Metamath Proof Explorer

Theorem smadiadetlem3

Description: Lemma 3 for smadiadet . (Contributed by AV, 31-Jan-2019)

Ref Expression
Hypotheses marep01ma.a 
|- A = ( N Mat R )
marep01ma.b 
|- B = ( Base ` A )
marep01ma.r 
|- R e. CRing
marep01ma.0 
|- .0. = ( 0g ` R )
marep01ma.1 
|- .1. = ( 1r ` R )
smadiadetlem.p 
|- P = ( Base ` ( SymGrp ` N ) )
smadiadetlem.g 
|- G = ( mulGrp ` R )
madetminlem.y 
|- Y = ( ZRHom ` R )
madetminlem.s 
|- S = ( pmSgn ` N )
madetminlem.t 
|- .x. = ( .r ` R )
smadiadetlem.w 
|- W = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
smadiadetlem.z 
|- Z = ( pmSgn ` ( N \ { K } ) )
Assertion smadiadetlem3 
|- ( ( M e. B /\ K e. N ) -> ( R gsum ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) = ( R gsum ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 marep01ma.a 
 |-  A = ( N Mat R )
2 marep01ma.b 
 |-  B = ( Base ` A )
3 marep01ma.r 
 |-  R e. CRing
4 marep01ma.0 
 |-  .0. = ( 0g ` R )
5 marep01ma.1 
 |-  .1. = ( 1r ` R )
6 smadiadetlem.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
7 smadiadetlem.g 
 |-  G = ( mulGrp ` R )
8 madetminlem.y 
 |-  Y = ( ZRHom ` R )
9 madetminlem.s 
 |-  S = ( pmSgn ` N )
10 madetminlem.t 
 |-  .x. = ( .r ` R )
11 smadiadetlem.w 
 |-  W = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
12 smadiadetlem.z 
 |-  Z = ( pmSgn ` ( N \ { K } ) )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 eqid 
 |-  ( Cntz ` R ) = ( Cntz ` R )
15 crngring 
 |-  ( R e. CRing -> R e. Ring )
16 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
17 3 15 16 mp2b 
 |-  R e. Mnd
18 17 a1i 
 |-  ( ( M e. B /\ K e. N ) -> R e. Mnd )
19 fvexd 
 |-  ( ( M e. B /\ K e. N ) -> ( Base ` ( SymGrp ` ( N \ { K } ) ) ) e. _V )
20 11 19 eqeltrid 
 |-  ( ( M e. B /\ K e. N ) -> W e. _V )
21 1 2 3 4 5 6 7 8 9 10 11 12 smadiadetlem3lem1 
 |-  ( ( M e. B /\ K e. N ) -> ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) : W --> ( Base ` R ) )
22 1 2 3 4 5 6 7 8 9 10 11 12 smadiadetlem3lem2 
 |-  ( ( M e. B /\ K e. N ) -> ran ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) C_ ( ( Cntz ` R ) ` ran ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) )
23 eqid 
 |-  ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) = ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) )
24 1 2 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
25 24 simpld 
 |-  ( M e. B -> N e. Fin )
26 25 adantr 
 |-  ( ( M e. B /\ K e. N ) -> N e. Fin )
27 diffi 
 |-  ( N e. Fin -> ( N \ { K } ) e. Fin )
28 eqid 
 |-  ( SymGrp ` ( N \ { K } ) ) = ( SymGrp ` ( N \ { K } ) )
29 eqid 
 |-  ( Base ` ( SymGrp ` ( N \ { K } ) ) ) = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
30 28 29 symgbasfi 
 |-  ( ( N \ { K } ) e. Fin -> ( Base ` ( SymGrp ` ( N \ { K } ) ) ) e. Fin )
31 26 27 30 3syl 
 |-  ( ( M e. B /\ K e. N ) -> ( Base ` ( SymGrp ` ( N \ { K } ) ) ) e. Fin )
32 11 31 eqeltrid 
 |-  ( ( M e. B /\ K e. N ) -> W e. Fin )
33 ovexd 
 |-  ( ( ( M e. B /\ K e. N ) /\ p e. W ) -> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) e. _V )
34 4 fvexi 
 |-  .0. e. _V
35 34 a1i 
 |-  ( ( M e. B /\ K e. N ) -> .0. e. _V )
36 23 32 33 35 fsuppmptdm 
 |-  ( ( M e. B /\ K e. N ) -> ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) finSupp .0. )
37 fveq1 
 |-  ( q = p -> ( q ` K ) = ( p ` K ) )
38 37 eqeq1d 
 |-  ( q = p -> ( ( q ` K ) = K <-> ( p ` K ) = K ) )
39 38 cbvrabv 
 |-  { q e. P | ( q ` K ) = K } = { p e. P | ( p ` K ) = K }
40 eqid 
 |-  ( p e. { q e. P | ( q ` K ) = K } |-> ( p |` ( N \ { K } ) ) ) = ( p e. { q e. P | ( q ` K ) = K } |-> ( p |` ( N \ { K } ) ) )
41 6 39 11 40 symgfixf1o 
 |-  ( ( N e. Fin /\ K e. N ) -> ( p e. { q e. P | ( q ` K ) = K } |-> ( p |` ( N \ { K } ) ) ) : { q e. P | ( q ` K ) = K } -1-1-onto-> W )
42 25 41 sylan 
 |-  ( ( M e. B /\ K e. N ) -> ( p e. { q e. P | ( q ` K ) = K } |-> ( p |` ( N \ { K } ) ) ) : { q e. P | ( q ` K ) = K } -1-1-onto-> W )
43 13 4 14 18 20 21 22 36 42 gsumzf1o 
 |-  ( ( M e. B /\ K e. N ) -> ( R gsum ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) = ( R gsum ( ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) o. ( p e. { q e. P | ( q ` K ) = K } |-> ( p |` ( N \ { K } ) ) ) ) ) )
44 eqid 
 |-  { q e. P | ( q ` K ) = K } = { q e. P | ( q ` K ) = K }
45 eqid 
 |-  ( N \ { K } ) = ( N \ { K } )
46 6 44 11 45 symgfixelsi 
 |-  ( ( K e. N /\ p e. { q e. P | ( q ` K ) = K } ) -> ( p |` ( N \ { K } ) ) e. W )
47 46 adantll 
 |-  ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> ( p |` ( N \ { K } ) ) e. W )
48 eqidd 
 |-  ( ( M e. B /\ K e. N ) -> ( p e. { q e. P | ( q ` K ) = K } |-> ( p |` ( N \ { K } ) ) ) = ( p e. { q e. P | ( q ` K ) = K } |-> ( p |` ( N \ { K } ) ) ) )
49 fveq2 
 |-  ( p = y -> ( ( Y o. Z ) ` p ) = ( ( Y o. Z ) ` y ) )
50 fveq1 
 |-  ( p = y -> ( p ` n ) = ( y ` n ) )
51 50 oveq2d 
 |-  ( p = y -> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) = ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( y ` n ) ) )
52 51 mpteq2dv 
 |-  ( p = y -> ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) = ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( y ` n ) ) ) )
53 52 oveq2d 
 |-  ( p = y -> ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) = ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( y ` n ) ) ) ) )
54 49 53 oveq12d 
 |-  ( p = y -> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) = ( ( ( Y o. Z ) ` y ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( y ` n ) ) ) ) ) )
55 54 cbvmptv 
 |-  ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) = ( y e. W |-> ( ( ( Y o. Z ) ` y ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( y ` n ) ) ) ) ) )
56 55 a1i 
 |-  ( ( M e. B /\ K e. N ) -> ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) = ( y e. W |-> ( ( ( Y o. Z ) ` y ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( y ` n ) ) ) ) ) ) )
57 fveq2 
 |-  ( y = ( p |` ( N \ { K } ) ) -> ( ( Y o. Z ) ` y ) = ( ( Y o. Z ) ` ( p |` ( N \ { K } ) ) ) )
58 fveq1 
 |-  ( y = ( p |` ( N \ { K } ) ) -> ( y ` n ) = ( ( p |` ( N \ { K } ) ) ` n ) )
59 fvres 
 |-  ( n e. ( N \ { K } ) -> ( ( p |` ( N \ { K } ) ) ` n ) = ( p ` n ) )
60 58 59 sylan9eq 
 |-  ( ( y = ( p |` ( N \ { K } ) ) /\ n e. ( N \ { K } ) ) -> ( y ` n ) = ( p ` n ) )
61 60 oveq2d 
 |-  ( ( y = ( p |` ( N \ { K } ) ) /\ n e. ( N \ { K } ) ) -> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( y ` n ) ) = ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) )
62 61 mpteq2dva 
 |-  ( y = ( p |` ( N \ { K } ) ) -> ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( y ` n ) ) ) = ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) )
63 62 oveq2d 
 |-  ( y = ( p |` ( N \ { K } ) ) -> ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( y ` n ) ) ) ) = ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) )
64 57 63 oveq12d 
 |-  ( y = ( p |` ( N \ { K } ) ) -> ( ( ( Y o. Z ) ` y ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( y ` n ) ) ) ) ) = ( ( ( Y o. Z ) ` ( p |` ( N \ { K } ) ) ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) )
65 47 48 56 64 fmptco 
 |-  ( ( M e. B /\ K e. N ) -> ( ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) o. ( p e. { q e. P | ( q ` K ) = K } |-> ( p |` ( N \ { K } ) ) ) ) = ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. Z ) ` ( p |` ( N \ { K } ) ) ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) )
66 6 9 12 copsgndif 
 |-  ( ( N e. Fin /\ K e. N ) -> ( p e. { q e. P | ( q ` K ) = K } -> ( ( Y o. Z ) ` ( p |` ( N \ { K } ) ) ) = ( ( Y o. S ) ` p ) ) )
67 25 66 sylan 
 |-  ( ( M e. B /\ K e. N ) -> ( p e. { q e. P | ( q ` K ) = K } -> ( ( Y o. Z ) ` ( p |` ( N \ { K } ) ) ) = ( ( Y o. S ) ` p ) ) )
68 67 imp 
 |-  ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> ( ( Y o. Z ) ` ( p |` ( N \ { K } ) ) ) = ( ( Y o. S ) ` p ) )
69 68 oveq1d 
 |-  ( ( ( M e. B /\ K e. N ) /\ p e. { q e. P | ( q ` K ) = K } ) -> ( ( ( Y o. Z ) ` ( p |` ( N \ { K } ) ) ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) = ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) )
70 69 mpteq2dva 
 |-  ( ( M e. B /\ K e. N ) -> ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. Z ) ` ( p |` ( N \ { K } ) ) ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) = ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) )
71 65 70 eqtrd 
 |-  ( ( M e. B /\ K e. N ) -> ( ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) o. ( p e. { q e. P | ( q ` K ) = K } |-> ( p |` ( N \ { K } ) ) ) ) = ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) )
72 71 oveq2d 
 |-  ( ( M e. B /\ K e. N ) -> ( R gsum ( ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) o. ( p e. { q e. P | ( q ` K ) = K } |-> ( p |` ( N \ { K } ) ) ) ) ) = ( R gsum ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) )
73 43 72 eqtr2d 
 |-  ( ( M e. B /\ K e. N ) -> ( R gsum ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) = ( R gsum ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) )