Metamath Proof Explorer

Theorem smadiadetlem3lem2

Description: Lemma 2 for smadiadetlem3 . (Contributed by AV, 12-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 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 ) ) ) ) ) ) ) )

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 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
15 3 13 14 mp2b 
 |-  R e. CMnd
16 1 2 3 4 5 6 7 8 9 10 11 12 smadiadetlem3lem0 
 |-  ( ( ( 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. ( Base ` R ) )
17 16 ralrimiva 
 |-  ( ( M e. B /\ K e. N ) -> A. 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. ( Base ` R ) )
18 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 ) ) ) ) ) )
19 18 rnmptss 
 |-  ( A. 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. ( Base ` 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 ) ) ) ) ) ) C_ ( Base ` R ) )
20 17 19 syl 
 |-  ( ( 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_ ( Base ` R ) )
21 eqid 
 |-  ( Base ` R ) = ( Base ` R )
22 eqid 
 |-  ( Cntz ` R ) = ( Cntz ` R )
23 21 22 cntzcmnss 
 |-  ( ( R e. CMnd /\ 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_ ( Base ` 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 ) ) ) ) ) ) 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 ) ) ) ) ) ) ) )
24 15 20 23 sylancr 
 |-  ( ( 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 ) ) ) ) ) ) ) )