let n be Nat; :: thesis: for K being Fanoian Field

for p2 being Element of Permutations (n + 2)

for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } holds

the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))

let K be Fanoian Field; :: thesis: for p2 being Element of Permutations (n + 2)

for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } holds

the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))

let p2 be Element of Permutations (n + 2); :: thesis: for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } holds

the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))

set n2 = n + 2;

let X, Y be Element of Fin (2Set (Seg (n + 2))); :: thesis: ( Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } implies the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y)) )

assume A1: Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } ; :: thesis: the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))

reconsider ID = id (Seg (n + 2)) as Element of Permutations (n + 2) by MATRIX_1:def 12;

set Y9 = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) } ;

A2: for x being object st x in X holds

(Part_sgn (ID,K)) . x = 1_ K

for p2 being Element of Permutations (n + 2)

for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } holds

the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))

let K be Fanoian Field; :: thesis: for p2 being Element of Permutations (n + 2)

for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } holds

the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))

let p2 be Element of Permutations (n + 2); :: thesis: for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } holds

the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))

set n2 = n + 2;

let X, Y be Element of Fin (2Set (Seg (n + 2))); :: thesis: ( Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } implies the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y)) )

assume A1: Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } ; :: thesis: the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))

reconsider ID = id (Seg (n + 2)) as Element of Permutations (n + 2) by MATRIX_1:def 12;

set Y9 = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) } ;

A2: for x being object st x in X holds

(Part_sgn (ID,K)) . x = 1_ K

proof

A9:
{ s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) } c= Y
A3:
X c= 2Set (Seg (n + 2))
by FINSUB_1:def 5;

let x be object ; :: thesis: ( x in X implies (Part_sgn (ID,K)) . x = 1_ K )

assume x in X ; :: thesis: (Part_sgn (ID,K)) . x = 1_ K

then consider i, j being Nat such that

A4: i in Seg (n + 2) and

A5: j in Seg (n + 2) and

A6: i < j and

A7: x = {i,j} by A3, MATRIX11:1;

A8: ID . j = j by A5, FUNCT_1:17;

ID . i = i by A4, FUNCT_1:17;

hence (Part_sgn (ID,K)) . x = 1_ K by A4, A5, A6, A7, A8, MATRIX11:def 1; :: thesis: verum

end;let x be object ; :: thesis: ( x in X implies (Part_sgn (ID,K)) . x = 1_ K )

assume x in X ; :: thesis: (Part_sgn (ID,K)) . x = 1_ K

then consider i, j being Nat such that

A4: i in Seg (n + 2) and

A5: j in Seg (n + 2) and

A6: i < j and

A7: x = {i,j} by A3, MATRIX11:1;

A8: ID . j = j by A5, FUNCT_1:17;

ID . i = i by A4, FUNCT_1:17;

hence (Part_sgn (ID,K)) . x = 1_ K by A4, A5, A6, A7, A8, MATRIX11:def 1; :: thesis: verum

proof

Y c= { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) }
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) } or y in Y )

assume y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) } ; :: thesis: y in Y

then consider s being Element of 2Set (Seg (n + 2)) such that

A10: y = s and

A11: s in X and

A12: (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ;

(Part_sgn (ID,K)) . s = 1_ K by A2, A11;

then (Part_sgn (p2,K)) . s = - (1_ K) by A12, MATRIX11:5;

hence y in Y by A1, A10, A11; :: thesis: verum

end;assume y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) } ; :: thesis: y in Y

then consider s being Element of 2Set (Seg (n + 2)) such that

A10: y = s and

A11: s in X and

A12: (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ;

(Part_sgn (ID,K)) . s = 1_ K by A2, A11;

then (Part_sgn (p2,K)) . s = - (1_ K) by A12, MATRIX11:5;

hence y in Y by A1, A10, A11; :: thesis: verum

proof

then A17:
Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) }
by A9, XBOOLE_0:def 10;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) } )

A13: 1_ K <> - (1_ K) by MATRIX11:22;

assume y in Y ; :: thesis: y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) }

then consider s being Element of 2Set (Seg (n + 2)) such that

A14: s = y and

A15: s in X and

A16: (Part_sgn (p2,K)) . s = - (1_ K) by A1;

(Part_sgn (ID,K)) . s = 1_ K by A2, A15;

hence y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) } by A14, A15, A16, A13; :: thesis: verum

end;A13: 1_ K <> - (1_ K) by MATRIX11:22;

assume y in Y ; :: thesis: y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) }

then consider s being Element of 2Set (Seg (n + 2)) such that

A14: s = y and

A15: s in X and

A16: (Part_sgn (p2,K)) . s = - (1_ K) by A1;

(Part_sgn (ID,K)) . s = 1_ K by A2, A15;

hence y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) } by A14, A15, A16, A13; :: thesis: verum

per cases
( (card Y) mod 2 = 0 or (card Y) mod 2 = 1 )
by NAT_D:12;

end;

suppose A18:
(card Y) mod 2 = 0
; :: thesis: the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))

then consider t being Nat such that

A19: card Y = (2 * t) + 0 and

0 < 2 by NAT_D:def 2;

t is Element of NAT by ORDINAL1:def 12;

hence (power K) . ((- (1_ K)),(card Y)) = 1_ K by A19, HURWITZ:4

.= the multF of K $$ (X,(Part_sgn (ID,K))) by A2, MATRIX11:4

.= the multF of K $$ (X,(Part_sgn (p2,K))) by A17, A18, MATRIX11:7 ;

:: thesis: verum

end;A19: card Y = (2 * t) + 0 and

0 < 2 by NAT_D:def 2;

t is Element of NAT by ORDINAL1:def 12;

hence (power K) . ((- (1_ K)),(card Y)) = 1_ K by A19, HURWITZ:4

.= the multF of K $$ (X,(Part_sgn (ID,K))) by A2, MATRIX11:4

.= the multF of K $$ (X,(Part_sgn (p2,K))) by A17, A18, MATRIX11:7 ;

:: thesis: verum

suppose A20:
(card Y) mod 2 = 1
; :: thesis: the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(card Y))

then consider t being Nat such that

A21: card Y = (2 * t) + 1 and

1 < 2 by NAT_D:def 2;

t is Element of NAT by ORDINAL1:def 12;

hence (power K) . ((- (1_ K)),(card Y)) = - (1_ K) by A21, HURWITZ:4

.= - ( the multF of K $$ (X,(Part_sgn (ID,K)))) by A2, MATRIX11:4

.= the multF of K $$ (X,(Part_sgn (p2,K))) by A17, A20, MATRIX11:7 ;

:: thesis: verum

end;A21: card Y = (2 * t) + 1 and

1 < 2 by NAT_D:def 2;

t is Element of NAT by ORDINAL1:def 12;

hence (power K) . ((- (1_ K)),(card Y)) = - (1_ K) by A21, HURWITZ:4

.= - ( the multF of K $$ (X,(Part_sgn (ID,K)))) by A2, MATRIX11:4

.= the multF of K $$ (X,(Part_sgn (p2,K))) by A17, A20, MATRIX11:7 ;

:: thesis: verum