let n be Nat; 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; 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); 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))); ( 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) ) }
; 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
A3:
X c= 2Set (Seg (n + 2))
by FINSUB_1:def 5;
let x be
object ;
( x in X implies (Part_sgn (ID,K)) . x = 1_ K )
assume
x in X
;
(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;
verum
end;
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
proof
let y be
object ;
TARSKI:def 3 ( 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 ) }
;
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;
verum
end;
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 ) }
proof
let y be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end;
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;