Metamath Proof Explorer

Theorem gsummatr01lem3

Description: Lemma 1 for gsummatr01 . (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 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 ) ) ) )

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 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 simpl 
 |-  ( ( G e. CMnd /\ N e. Fin ) -> G e. CMnd )
8 7 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. CMnd )
9 diffi 
 |-  ( N e. Fin -> ( N \ { K } ) e. Fin )
10 9 adantl 
 |-  ( ( G e. CMnd /\ N e. Fin ) -> ( N \ { K } ) e. Fin )
11 10 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 )
12 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 ) ) ) )
13 eqeq1 
 |-  ( i = n -> ( i = K <-> n = K ) )
14 13 adantr 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> ( i = K <-> n = K ) )
15 eqeq1 
 |-  ( j = ( Q ` n ) -> ( j = L <-> ( Q ` n ) = L ) )
16 15 ifbid 
 |-  ( j = ( Q ` n ) -> if ( j = L , .0. , B ) = if ( ( Q ` n ) = L , .0. , B ) )
17 16 adantl 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> if ( j = L , .0. , B ) = if ( ( Q ` n ) = L , .0. , B ) )
18 oveq12 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> ( i A j ) = ( n A ( Q ` n ) ) )
19 14 17 18 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 ) ) ) )
20 eldifsni 
 |-  ( n e. ( N \ { K } ) -> n =/= K )
21 20 neneqd 
 |-  ( n e. ( N \ { K } ) -> -. n = K )
22 21 iffalsed 
 |-  ( n e. ( N \ { K } ) -> if ( n = K , if ( ( Q ` n ) = L , .0. , B ) , ( n A ( Q ` n ) ) ) = ( n A ( Q ` n ) ) )
23 22 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 ) ) )
24 19 23 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 ) ) )
25 eldifi 
 |-  ( n e. ( N \ { K } ) -> n e. N )
26 25 adantl 
 |-  ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ n e. ( N \ { K } ) ) -> n e. N )
27 1 2 gsummatr01lem1 
 |-  ( ( Q e. R /\ n e. N ) -> ( Q ` n ) e. N )
28 27 expcom 
 |-  ( n e. N -> ( Q e. R -> ( Q ` n ) e. N ) )
29 28 25 syl11 
 |-  ( Q e. R -> ( n e. ( N \ { K } ) -> ( Q ` n ) e. N ) )
30 29 3ad2ant3 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> ( n e. ( N \ { K } ) -> ( Q ` n ) e. N ) )
31 30 imp 
 |-  ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ n e. ( N \ { K } ) ) -> ( Q ` n ) e. N )
32 ovexd 
 |-  ( ( ( K e. N /\ L e. N /\ Q e. R ) /\ n e. ( N \ { K } ) ) -> ( n A ( Q ` n ) ) e. _V )
33 12 24 26 31 32 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 ) ) )
34 33 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 ) ) )
35 4 eleq2i 
 |-  ( ( i A j ) e. S <-> ( i A j ) e. ( Base ` G ) )
36 35 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 ) )
37 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 ) ) )
38 25 37 sylan2 
 |-  ( ( Q e. R /\ n e. ( N \ { K } ) ) -> ( A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) )
39 38 ex 
 |-  ( Q e. R -> ( n e. ( N \ { K } ) -> ( A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) ) )
40 39 3ad2ant3 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> ( n e. ( N \ { K } ) -> ( A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) ) )
41 40 com3r 
 |-  ( A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) -> ( ( K e. N /\ L e. N /\ Q e. R ) -> ( n e. ( N \ { K } ) -> ( n A ( Q ` n ) ) e. ( Base ` G ) ) ) )
42 36 41 sylbi 
 |-  ( 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 ) ) ) )
43 42 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 ) ) ) )
44 43 imp31 
 |-  ( ( ( ( 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 ) )
45 44 3adantl1 
 |-  ( ( ( ( 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 ) )
46 34 45 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 ) )
47 simp31 
 |-  ( ( ( 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 e. N )
48 neldifsnd 
 |-  ( ( ( 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 e. ( N \ { K } ) )
49 eqidd 
 |-  ( ( B e. S /\ ( 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 ) ) ) )
50 iftrue 
 |-  ( i = K -> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) = if ( j = L , .0. , B ) )
51 eqeq1 
 |-  ( j = ( Q ` K ) -> ( j = L <-> ( Q ` K ) = L ) )
52 51 ifbid 
 |-  ( j = ( Q ` K ) -> if ( j = L , .0. , B ) = if ( ( Q ` K ) = L , .0. , B ) )
53 50 52 sylan9eq 
 |-  ( ( i = K /\ j = ( Q ` K ) ) -> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) = if ( ( Q ` K ) = L , .0. , B ) )
54 53 adantl 
 |-  ( ( ( B e. S /\ ( 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 ) ) = if ( ( Q ` K ) = L , .0. , B ) )
55 simpr1 
 |-  ( ( B e. S /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> K e. N )
56 1 2 gsummatr01lem1 
 |-  ( ( Q e. R /\ K e. N ) -> ( Q ` K ) e. N )
57 56 ancoms 
 |-  ( ( K e. N /\ Q e. R ) -> ( Q ` K ) e. N )
58 57 3adant2 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> ( Q ` K ) e. N )
59 58 adantl 
 |-  ( ( B e. S /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( Q ` K ) e. N )
60 3 fvexi 
 |-  .0. e. _V
61 simpl 
 |-  ( ( B e. S /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> B e. S )
62 ifexg 
 |-  ( ( .0. e. _V /\ B e. S ) -> if ( ( Q ` K ) = L , .0. , B ) e. _V )
63 60 61 62 sylancr 
 |-  ( ( B e. S /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> if ( ( Q ` K ) = L , .0. , B ) e. _V )
64 49 54 55 59 63 ovmpod 
 |-  ( ( 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 ) ) = if ( ( Q ` K ) = L , .0. , B ) )
65 64 adantll 
 |-  ( ( ( 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 ) ) = if ( ( Q ` K ) = L , .0. , B ) )
66 65 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 ) ) -> ( K ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` K ) ) = if ( ( Q ` K ) = L , .0. , B ) )
67 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
68 5 3 mndidcl 
 |-  ( G e. Mnd -> .0. e. ( Base ` G ) )
69 67 68 syl 
 |-  ( G e. CMnd -> .0. e. ( Base ` G ) )
70 69 adantr 
 |-  ( ( G e. CMnd /\ N e. Fin ) -> .0. e. ( Base ` G ) )
71 70 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 ) ) -> .0. e. ( Base ` G ) )
72 4 eleq2i 
 |-  ( B e. S <-> B e. ( Base ` G ) )
73 72 biimpi 
 |-  ( B e. S -> B e. ( Base ` G ) )
74 73 adantl 
 |-  ( ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) -> B e. ( Base ` G ) )
75 74 3ad2ant2 
 |-  ( ( ( 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 ) ) -> B e. ( Base ` G ) )
76 71 75 ifcld 
 |-  ( ( ( 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 ) ) -> if ( ( Q ` K ) = L , .0. , B ) e. ( Base ` G ) )
77 66 76 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 ) ) -> ( K ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` K ) ) e. ( Base ` G ) )
78 id 
 |-  ( n = K -> n = K )
79 fveq2 
 |-  ( n = K -> ( Q ` n ) = ( Q ` K ) )
80 78 79 oveq12d 
 |-  ( n = K -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) = ( K ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` K ) ) )
81 5 6 8 11 46 47 48 77 80 gsumunsn 
 |-  ( ( ( 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 ) ) ) )