Metamath Proof Explorer

Theorem gsummatr01lem4

Description: Lemma 2 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 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 ) ) )

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 eqidd 
 |-  ( ( 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 ) ) ) )
6 eqeq1 
 |-  ( i = n -> ( i = K <-> n = K ) )
7 6 adantr 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> ( i = K <-> n = K ) )
8 eqeq1 
 |-  ( j = ( Q ` n ) -> ( j = L <-> ( Q ` n ) = L ) )
9 8 adantl 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> ( j = L <-> ( Q ` n ) = L ) )
10 9 ifbid 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> if ( j = L , .0. , B ) = if ( ( Q ` n ) = L , .0. , B ) )
11 oveq12 
 |-  ( ( i = n /\ j = ( Q ` n ) ) -> ( i A j ) = ( n A ( Q ` n ) ) )
12 7 10 11 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 ) ) ) )
13 eldifsni 
 |-  ( n e. ( N \ { K } ) -> n =/= K )
14 13 neneqd 
 |-  ( n e. ( N \ { K } ) -> -. n = K )
15 14 iffalsed 
 |-  ( n e. ( N \ { K } ) -> if ( n = K , if ( ( Q ` n ) = L , .0. , B ) , ( n A ( Q ` n ) ) ) = ( n A ( Q ` n ) ) )
16 15 adantl 
 |-  ( ( Q e. R /\ n e. ( N \ { K } ) ) -> if ( n = K , if ( ( Q ` n ) = L , .0. , B ) , ( n A ( Q ` n ) ) ) = ( n A ( Q ` n ) ) )
17 12 16 sylan9eqr 
 |-  ( ( ( 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 ) ) )
18 eldifi 
 |-  ( n e. ( N \ { K } ) -> n e. N )
19 18 adantl 
 |-  ( ( Q e. R /\ n e. ( N \ { K } ) ) -> n e. N )
20 1 2 gsummatr01lem1 
 |-  ( ( Q e. R /\ n e. N ) -> ( Q ` n ) e. N )
21 18 20 sylan2 
 |-  ( ( Q e. R /\ n e. ( N \ { K } ) ) -> ( Q ` n ) e. N )
22 ovexd 
 |-  ( ( Q e. R /\ n e. ( N \ { K } ) ) -> ( n A ( Q ` n ) ) e. _V )
23 5 17 19 21 22 ovmpod 
 |-  ( ( 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 ) ) )
24 23 ex 
 |-  ( 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 ) ) ) )
25 24 3ad2ant3 
 |-  ( ( 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 ) ) ) )
26 25 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 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 ) ) ) )
27 26 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 ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) = ( n A ( Q ` n ) ) )
28 eqidd 
 |-  ( ( ( ( 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 } ) ) -> ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) = ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) )
29 11 adantl 
 |-  ( ( ( ( ( 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 } ) ) /\ ( i = n /\ j = ( Q ` n ) ) ) -> ( i A j ) = ( n A ( Q ` n ) ) )
30 eqidd 
 |-  ( ( ( ( ( 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 } ) ) /\ i = n ) -> ( N \ { L } ) = ( N \ { L } ) )
31 simpr 
 |-  ( ( ( ( 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 e. ( N \ { K } ) )
32 fveq1 
 |-  ( r = Q -> ( r ` K ) = ( Q ` K ) )
33 32 eqeq1d 
 |-  ( r = Q -> ( ( r ` K ) = L <-> ( Q ` K ) = L ) )
34 33 2 elrab2 
 |-  ( Q e. R <-> ( Q e. P /\ ( Q ` K ) = L ) )
35 simpll 
 |-  ( ( ( Q e. P /\ ( Q ` K ) = L ) /\ ( L e. N /\ K e. N ) ) -> Q e. P )
36 eqid 
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
37 36 1 symgfv 
 |-  ( ( Q e. P /\ n e. N ) -> ( Q ` n ) e. N )
38 35 18 37 syl2an 
 |-  ( ( ( ( Q e. P /\ ( Q ` K ) = L ) /\ ( L e. N /\ K e. N ) ) /\ n e. ( N \ { K } ) ) -> ( Q ` n ) e. N )
39 35 adantr 
 |-  ( ( ( ( Q e. P /\ ( Q ` K ) = L ) /\ ( L e. N /\ K e. N ) ) /\ n e. ( N \ { K } ) ) -> Q e. P )
40 simplrr 
 |-  ( ( ( ( Q e. P /\ ( Q ` K ) = L ) /\ ( L e. N /\ K e. N ) ) /\ n e. ( N \ { K } ) ) -> K e. N )
41 18 adantl 
 |-  ( ( ( ( Q e. P /\ ( Q ` K ) = L ) /\ ( L e. N /\ K e. N ) ) /\ n e. ( N \ { K } ) ) -> n e. N )
42 39 40 41 3jca 
 |-  ( ( ( ( Q e. P /\ ( Q ` K ) = L ) /\ ( L e. N /\ K e. N ) ) /\ n e. ( N \ { K } ) ) -> ( Q e. P /\ K e. N /\ n e. N ) )
43 simpllr 
 |-  ( ( ( ( Q e. P /\ ( Q ` K ) = L ) /\ ( L e. N /\ K e. N ) ) /\ n e. ( N \ { K } ) ) -> ( Q ` K ) = L )
44 13 adantl 
 |-  ( ( ( ( Q e. P /\ ( Q ` K ) = L ) /\ ( L e. N /\ K e. N ) ) /\ n e. ( N \ { K } ) ) -> n =/= K )
45 36 1 symgfvne 
 |-  ( ( Q e. P /\ K e. N /\ n e. N ) -> ( ( Q ` K ) = L -> ( n =/= K -> ( Q ` n ) =/= L ) ) )
46 42 43 44 45 syl3c 
 |-  ( ( ( ( Q e. P /\ ( Q ` K ) = L ) /\ ( L e. N /\ K e. N ) ) /\ n e. ( N \ { K } ) ) -> ( Q ` n ) =/= L )
47 38 46 jca 
 |-  ( ( ( ( Q e. P /\ ( Q ` K ) = L ) /\ ( L e. N /\ K e. N ) ) /\ n e. ( N \ { K } ) ) -> ( ( Q ` n ) e. N /\ ( Q ` n ) =/= L ) )
48 47 exp42 
 |-  ( ( Q e. P /\ ( Q ` K ) = L ) -> ( L e. N -> ( K e. N -> ( n e. ( N \ { K } ) -> ( ( Q ` n ) e. N /\ ( Q ` n ) =/= L ) ) ) ) )
49 34 48 sylbi 
 |-  ( Q e. R -> ( L e. N -> ( K e. N -> ( n e. ( N \ { K } ) -> ( ( Q ` n ) e. N /\ ( Q ` n ) =/= L ) ) ) ) )
50 49 3imp31 
 |-  ( ( K e. N /\ L e. N /\ Q e. R ) -> ( n e. ( N \ { K } ) -> ( ( Q ` n ) e. N /\ ( Q ` n ) =/= L ) ) )
51 50 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 e. ( N \ { K } ) -> ( ( Q ` n ) e. N /\ ( Q ` n ) =/= L ) ) )
52 51 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 } ) ) -> ( ( Q ` n ) e. N /\ ( Q ` n ) =/= L ) )
53 eldifsn 
 |-  ( ( Q ` n ) e. ( N \ { L } ) <-> ( ( Q ` n ) e. N /\ ( Q ` n ) =/= L ) )
54 52 53 sylibr 
 |-  ( ( ( ( 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 } ) ) -> ( Q ` n ) e. ( N \ { L } ) )
55 ovexd 
 |-  ( ( ( ( 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. _V )
56 nfv 
 |-  F/ i ( G e. CMnd /\ N e. Fin )
57 nfra1 
 |-  F/ i A. i e. N A. j e. N ( i A j ) e. S
58 nfcv 
 |-  F/_ i S
59 58 nfel2 
 |-  F/ i B e. S
60 57 59 nfan 
 |-  F/ i ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S )
61 nfv 
 |-  F/ i ( K e. N /\ L e. N /\ Q e. R )
62 56 60 61 nf3an 
 |-  F/ i ( ( 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 ) )
63 nfcv 
 |-  F/_ i ( N \ { K } )
64 63 nfel2 
 |-  F/ i n e. ( N \ { K } )
65 62 64 nfan 
 |-  F/ i ( ( ( 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 } ) )
66 nfv 
 |-  F/ j ( G e. CMnd /\ N e. Fin )
67 nfra2w 
 |-  F/ j A. i e. N A. j e. N ( i A j ) e. S
68 nfcv 
 |-  F/_ j S
69 68 nfel2 
 |-  F/ j B e. S
70 67 69 nfan 
 |-  F/ j ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S )
71 nfv 
 |-  F/ j ( K e. N /\ L e. N /\ Q e. R )
72 66 70 71 nf3an 
 |-  F/ j ( ( 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 ) )
73 nfcv 
 |-  F/_ j ( N \ { K } )
74 73 nfel2 
 |-  F/ j n e. ( N \ { K } )
75 72 74 nfan 
 |-  F/ j ( ( ( 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 } ) )
76 nfcv 
 |-  F/_ j n
77 nfcv 
 |-  F/_ i ( Q ` n )
78 nfcv 
 |-  F/_ i ( n A ( Q ` n ) )
79 nfcv 
 |-  F/_ j ( n A ( Q ` n ) )
80 28 29 30 31 54 55 65 75 76 77 78 79 ovmpodxf 
 |-  ( ( ( ( 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 \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) ( Q ` n ) ) = ( n A ( Q ` n ) ) )
81 27 80 eqtr4d 
 |-  ( ( ( ( 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 ) ) )