Metamath Proof Explorer

Theorem smadiadetlem3lem0

Description: Lemma 0 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 smadiadetlem3lem0 
|- ( ( ( M e. B /\ K e. N ) /\ Q e. W ) -> ( ( ( Y o. Z ) ` Q ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( Q ` n ) ) ) ) ) e. ( Base ` R ) )

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 difssd 
 |-  ( K e. N -> ( N \ { K } ) C_ N )
14 13 anim2i 
 |-  ( ( M e. B /\ K e. N ) -> ( M e. B /\ ( N \ { K } ) C_ N ) )
15 14 adantr 
 |-  ( ( ( M e. B /\ K e. N ) /\ Q e. W ) -> ( M e. B /\ ( N \ { K } ) C_ N ) )
16 1 2 submabas 
 |-  ( ( M e. B /\ ( N \ { K } ) C_ N ) -> ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) e. ( Base ` ( ( N \ { K } ) Mat R ) ) )
17 15 16 syl 
 |-  ( ( ( M e. B /\ K e. N ) /\ Q e. W ) -> ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) e. ( Base ` ( ( N \ { K } ) Mat R ) ) )
18 simpr 
 |-  ( ( ( M e. B /\ K e. N ) /\ Q e. W ) -> Q e. W )
19 eqid 
 |-  ( ( N \ { K } ) Mat R ) = ( ( N \ { K } ) Mat R )
20 eqid 
 |-  ( Base ` ( ( N \ { K } ) Mat R ) ) = ( Base ` ( ( N \ { K } ) Mat R ) )
21 11 12 8 19 20 7 madetsmelbas2 
 |-  ( ( R e. CRing /\ ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) e. ( Base ` ( ( N \ { K } ) Mat R ) ) /\ Q e. W ) -> ( ( ( Y o. Z ) ` Q ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( Q ` n ) ) ) ) ) e. ( Base ` R ) )
22 3 17 18 21 mp3an2i 
 |-  ( ( ( M e. B /\ K e. N ) /\ Q e. W ) -> ( ( ( Y o. Z ) ` Q ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( Q ` n ) ) ) ) ) e. ( Base ` R ) )