Metamath Proof Explorer

Theorem gsummatr01

Description: Lemma 1 for smadiadetlem4 . (Contributed by AV, 8-Jan-2019)

Ref Expression
Hypotheses gsummatr01.p 
|- P = ( Base ` ( SymGrp ` N ) )
gsummatr01.r 
|- R = { r e. P | ( r ` K ) = L }
gsummatr01.0 
|- .0. = ( 0g ` G )
gsummatr01.s 
|- S = ( Base ` G )
Assertion gsummatr01 
|- ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) = ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) ( Q ` n ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummatr01.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 gsummatr01.r 
 |-  R = { r e. P | ( r ` K ) = L }
3 gsummatr01.0 
 |-  .0. = ( 0g ` G )
4 gsummatr01.s 
 |-  S = ( Base ` G )
5 difsnid 
 |-  ( K e. N -> ( ( N \ { K } ) u. { K } ) = N )
6 5 eqcomd 
 |-  ( K e. N -> N = ( ( N \ { K } ) u. { K } ) )
7 6 3ad2ant1 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> N = ( ( N \ { K } ) u. { K } ) )
8 7 3ad2ant3 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> N = ( ( N \ { K } ) u. { K } ) )
9 8 mpteq1d 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) = ( n e. ( ( N \ { K } ) u. { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) )
10 9 oveq2d 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) = ( G gsum ( n e. ( ( N \ { K } ) u. { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) )
11 1 2 3 4 gsummatr01lem3 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( G gsum ( n e. ( ( N \ { K } ) u. { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) = ( ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) ( +g ` G ) ( K ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` K ) ) ) )
12 eqidd 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) )
13 fveq1 
 |-  ( r = Q -> ( r ` K ) = ( Q ` K ) )
14 13 eqeq1d 
 |-  ( r = Q -> ( ( r ` K ) = L <-> ( Q ` K ) = L ) )
15 14 2 elrab2 
 |-  ( Q e. R <-> ( Q e. P /\ ( Q ` K ) = L ) )
16 eqeq2 
 |-  ( ( Q ` K ) = L -> ( j = ( Q ` K ) <-> j = L ) )
17 16 adantl 
 |-  ( ( Q e. P /\ ( Q ` K ) = L ) -> ( j = ( Q ` K ) <-> j = L ) )
18 17 anbi2d 
 |-  ( ( Q e. P /\ ( Q ` K ) = L ) -> ( ( i = K /\ j = ( Q ` K ) ) <-> ( i = K /\ j = L ) ) )
19 15 18 sylbi 
 |-  ( Q e. R -> ( ( i = K /\ j = ( Q ` K ) ) <-> ( i = K /\ j = L ) ) )
20 19 3ad2ant3 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> ( ( i = K /\ j = ( Q ` K ) ) <-> ( i = K /\ j = L ) ) )
21 iftrue 
 |-  ( i = K -> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) = if ( j = L , .0. , B ) )
22 iftrue 
 |-  ( j = L -> if ( j = L , .0. , B ) = .0. )
23 21 22 sylan9eq 
 |-  ( ( i = K /\ j = L ) -> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) = .0. )
24 20 23 syl6bi 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> ( ( i = K /\ j = ( Q ` K ) ) -> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) = .0. ) )
25 24 imp 
 |-  ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ ( i = K /\ j = ( Q ` K ) ) ) -> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) = .0. )
26 simp1 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> K e. N )
27 1 2 gsummatr01lem1 
 |-  ( ( Q e. R /\ K e. N ) -> ( Q ` K ) e. N )
28 27 ancoms 
 |-  ( ( K e. N /\ Q e. R ) -> ( Q ` K ) e. N )
29 28 3adant2 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> ( Q ` K ) e. N )
30 3 fvexi 
 |-  .0. e. _V
31 30 a1i 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> .0. e. _V )
32 12 25 26 29 31 ovmpod 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> ( K ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` K ) ) = .0. )
33 32 3ad2ant3 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( K ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` K ) ) = .0. )
34 33 oveq2d 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) ( +g ` G ) ( K ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` K ) ) ) = ( ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) ( +g ` G ) .0. ) )
35 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
36 35 adantr 
 |-  ( ( G e. CMnd /\ N e. Fin ) -> G e. Mnd )
37 36 3ad2ant1 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> G e. Mnd )
38 eqid 
 |-  ( Base ` G ) = ( Base ` G )
39 simp1l 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> G e. CMnd )
40 diffi 
 |-  ( N e. Fin -> ( N \ { K } ) e. Fin )
41 40 adantl 
 |-  ( ( G e. CMnd /\ N e. Fin ) -> ( N \ { K } ) e. Fin )
42 41 3ad2ant1 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( N \ { K } ) e. Fin )
43 eqidd 
 |-  ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ n e. ( N \ { K } ) ) -> ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) )
44 eqeq1 
 |-  ( i = n -> ( i = K <-> n = K ) )
45 44 adantr 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> ( i = K <-> n = K ) )
46 eqeq1 
 |-  ( j = ( Q ` n ) -> ( j = L <-> ( Q ` n ) = L ) )
47 46 ifbid 
 |-  ( j = ( Q ` n ) -> if ( j = L , .0. , B ) = if ( ( Q ` n ) = L , .0. , B ) )
48 47 adantl 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> if ( j = L , .0. , B ) = if ( ( Q ` n ) = L , .0. , B ) )
49 oveq12 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> ( i A j ) = ( n A ( Q ` n ) ) )
50 45 48 49 ifbieq12d 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) = if ( n = K , if ( ( Q ` n ) = L , .0. , B ) , ( n A ( Q ` n ) ) ) )
51 eldifsni 
 |-  ( n e. ( N \ { K } ) -> n =/= K )
52 51 neneqd 
 |-  ( n e. ( N \ { K } ) -> -. n = K )
53 52 iffalsed 
 |-  ( n e. ( N \ { K } ) -> if ( n = K , if ( ( Q ` n ) = L , .0. , B ) , ( n A ( Q ` n ) ) ) = ( n A ( Q ` n ) ) )
54 53 adantl 
 |-  ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ n e. ( N \ { K } ) ) -> if ( n = K , if ( ( Q ` n ) = L , .0. , B ) , ( n A ( Q ` n ) ) ) = ( n A ( Q ` n ) ) )
55 50 54 sylan9eqr 
 |-  ( ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ n e. ( N \ { K } ) ) /\ ( i = n /\ j = ( Q ` n ) ) ) -> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) = ( n A ( Q ` n ) ) )
56 eldifi 
 |-  ( n e. ( N \ { K } ) -> n e. N )
57 56 adantl 
 |-  ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ n e. ( N \ { K } ) ) -> n e. N )
58 simp3 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> Q e. R )
59 1 2 gsummatr01lem1 
 |-  ( ( Q e. R /\ n e. N ) -> ( Q ` n ) e. N )
60 58 56 59 syl2an 
 |-  ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ n e. ( N \ { K } ) ) -> ( Q ` n ) e. N )
61 ovexd 
 |-  ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ n e. ( N \ { K } ) ) -> ( n A ( Q ` n ) ) e. _V )
62 43 55 57 60 61 ovmpod 
 |-  ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ n e. ( N \ { K } ) ) -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) = ( n A ( Q ` n ) ) )
63 62 3ad2antl3 
 |-  ( ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) /\ n e. ( N \ { K } ) ) -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) = ( n A ( Q ` n ) ) )
64 4 eleq2i 
 |-  ( ( i A j ) e. S <-> ( i A j ) e. ( Base ` G ) )
65 64 2ralbii 
 |-  ( A. i e. N A. j e. N ( i A j ) e. S <-> A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) )
66 1 2 gsummatr01lem2 
 |-  ( ( Q e. R /\ n e. N ) -> ( A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) )
67 65 66 syl5bi 
 |-  ( ( Q e. R /\ n e. N ) -> ( A. i e. N A. j e. N ( i A j ) e. S -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) )
68 58 56 67 syl2anr 
 |-  ( ( n e. ( N \ { K } ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( A. i e. N A. j e. N ( i A j ) e. S -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) )
69 68 ex 
 |-  ( n e. ( N \ { K } ) -> ( ( K e. N /\ L e. N /\ Q e. R ) -> ( A. i e. N A. j e. N ( i A j ) e. S -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) ) )
70 69 com13 
 |-  ( A. i e. N A. j e. N ( i A j ) e. S -> ( ( K e. N /\ L e. N /\ Q e. R ) -> ( n e. ( N \ { K } ) -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) ) )
71 70 adantr 
 |-  ( ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) -> ( ( K e. N /\ L e. N /\ Q e. R ) -> ( n e. ( N \ { K } ) -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) ) )
72 71 imp 
 |-  ( ( ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( n e. ( N \ { K } ) -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) )
73 72 3adant1 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( n e. ( N \ { K } ) -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) )
74 73 imp 
 |-  ( ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) /\ n e. ( N \ { K } ) ) -> ( n A ( Q ` n ) ) e. ( Base ` G ) )
75 63 74 eqeltrd 
 |-  ( ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) /\ n e. ( N \ { K } ) ) -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) e. ( Base ` G ) )
76 75 ralrimiva 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> A. n e. ( N \ { K } ) ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) e. ( Base ` G ) )
77 38 39 42 76 gsummptcl 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) e. ( Base ` G ) )
78 eqid 
 |-  ( +g ` G ) = ( +g ` G )
79 38 78 3 mndrid 
 |-  ( ( G e. Mnd /\ ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) e. ( Base ` G ) ) -> ( ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) ( +g ` G ) .0. ) = ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) )
80 37 77 79 syl2anc 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) ( +g ` G ) .0. ) = ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) )
81 1 2 3 4 gsummatr01lem4 
 |-  ( ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) /\ n e. ( N \ { K } ) ) -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) = ( n ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) ( Q ` n ) ) )
82 81 mpteq2dva 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) = ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) ( Q ` n ) ) ) )
83 82 oveq2d 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) = ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) ( Q ` n ) ) ) ) )
84 34 80 83 3eqtrd 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) ( +g ` G ) ( K ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` K ) ) ) = ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) ( Q ` n ) ) ) ) )
85 10 11 84 3eqtrd 
 |-  ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( G gsum ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) = ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) ( Q ` n ) ) ) ) )