Metamath Proof Explorer

Theorem assamulgscmlem1

Description: Lemma 1 for assamulgscm (induction base). (Contributed by AV, 26-Aug-2019)

Ref Expression
Hypotheses assamulgscm.v 
|- V = ( Base ` W )
assamulgscm.f 
|- F = ( Scalar ` W )
assamulgscm.b 
|- B = ( Base ` F )
assamulgscm.s 
|- .x. = ( .s ` W )
assamulgscm.g 
|- G = ( mulGrp ` F )
assamulgscm.p 
|- .^ = ( .g ` G )
assamulgscm.h 
|- H = ( mulGrp ` W )
assamulgscm.e 
|- E = ( .g ` H )
Assertion assamulgscmlem1 
|- ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( 0 E ( A .x. X ) ) = ( ( 0 .^ A ) .x. ( 0 E X ) ) )

Proof

Step Hyp Ref Expression
1 assamulgscm.v 
 |-  V = ( Base ` W )
2 assamulgscm.f 
 |-  F = ( Scalar ` W )
3 assamulgscm.b 
 |-  B = ( Base ` F )
4 assamulgscm.s 
 |-  .x. = ( .s ` W )
5 assamulgscm.g 
 |-  G = ( mulGrp ` F )
6 assamulgscm.p 
 |-  .^ = ( .g ` G )
7 assamulgscm.h 
 |-  H = ( mulGrp ` W )
8 assamulgscm.e 
 |-  E = ( .g ` H )
9 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
10 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
11 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
12 1 11 ringidcl 
 |-  ( W e. Ring -> ( 1r ` W ) e. V )
13 10 12 syl 
 |-  ( W e. AssAlg -> ( 1r ` W ) e. V )
14 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
15 1 2 4 14 lmodvs1 
 |-  ( ( W e. LMod /\ ( 1r ` W ) e. V ) -> ( ( 1r ` F ) .x. ( 1r ` W ) ) = ( 1r ` W ) )
16 15 eqcomd 
 |-  ( ( W e. LMod /\ ( 1r ` W ) e. V ) -> ( 1r ` W ) = ( ( 1r ` F ) .x. ( 1r ` W ) ) )
17 9 13 16 syl2anc 
 |-  ( W e. AssAlg -> ( 1r ` W ) = ( ( 1r ` F ) .x. ( 1r ` W ) ) )
18 17 adantl 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( 1r ` W ) = ( ( 1r ` F ) .x. ( 1r ` W ) ) )
19 9 adantl 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> W e. LMod )
20 simpll 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> A e. B )
21 simplr 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> X e. V )
22 1 2 4 3 lmodvscl 
 |-  ( ( W e. LMod /\ A e. B /\ X e. V ) -> ( A .x. X ) e. V )
23 19 20 21 22 syl3anc 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( A .x. X ) e. V )
24 7 1 mgpbas 
 |-  V = ( Base ` H )
25 7 11 ringidval 
 |-  ( 1r ` W ) = ( 0g ` H )
26 24 25 8 mulg0 
 |-  ( ( A .x. X ) e. V -> ( 0 E ( A .x. X ) ) = ( 1r ` W ) )
27 23 26 syl 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( 0 E ( A .x. X ) ) = ( 1r ` W ) )
28 5 3 mgpbas 
 |-  B = ( Base ` G )
29 5 14 ringidval 
 |-  ( 1r ` F ) = ( 0g ` G )
30 28 29 6 mulg0 
 |-  ( A e. B -> ( 0 .^ A ) = ( 1r ` F ) )
31 20 30 syl 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( 0 .^ A ) = ( 1r ` F ) )
32 24 25 8 mulg0 
 |-  ( X e. V -> ( 0 E X ) = ( 1r ` W ) )
33 21 32 syl 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( 0 E X ) = ( 1r ` W ) )
34 31 33 oveq12d 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( ( 0 .^ A ) .x. ( 0 E X ) ) = ( ( 1r ` F ) .x. ( 1r ` W ) ) )
35 18 27 34 3eqtr4d 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( 0 E ( A .x. X ) ) = ( ( 0 .^ A ) .x. ( 0 E X ) ) )