Metamath Proof Explorer

Theorem assamulgscmlem2

Description: Lemma for assamulgscm (induction step). (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 assamulgscmlem2 
|- ( y e. NN0 -> ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) -> ( ( y + 1 ) E ( A .x. X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) 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 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
10 7 ringmgp 
 |-  ( W e. Ring -> H e. Mnd )
11 9 10 syl 
 |-  ( W e. AssAlg -> H e. Mnd )
12 11 adantl 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> H e. Mnd )
13 12 adantl 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> H e. Mnd )
14 13 adantr 
 |-  ( ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) /\ ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) ) -> H e. Mnd )
15 simpll 
 |-  ( ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) /\ ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) ) -> y e. NN0 )
16 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
17 16 adantl 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> W e. LMod )
18 simpll 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> A e. B )
19 simplr 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> X e. V )
20 1 2 4 3 lmodvscl 
 |-  ( ( W e. LMod /\ A e. B /\ X e. V ) -> ( A .x. X ) e. V )
21 17 18 19 20 syl3anc 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( A .x. X ) e. V )
22 21 adantl 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( A .x. X ) e. V )
23 22 adantr 
 |-  ( ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) /\ ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) ) -> ( A .x. X ) e. V )
24 7 1 mgpbas 
 |-  V = ( Base ` H )
25 eqid 
 |-  ( .r ` W ) = ( .r ` W )
26 7 25 mgpplusg 
 |-  ( .r ` W ) = ( +g ` H )
27 24 8 26 mulgnn0p1 
 |-  ( ( H e. Mnd /\ y e. NN0 /\ ( A .x. X ) e. V ) -> ( ( y + 1 ) E ( A .x. X ) ) = ( ( y E ( A .x. X ) ) ( .r ` W ) ( A .x. X ) ) )
28 14 15 23 27 syl3anc 
 |-  ( ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) /\ ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) ) -> ( ( y + 1 ) E ( A .x. X ) ) = ( ( y E ( A .x. X ) ) ( .r ` W ) ( A .x. X ) ) )
29 oveq1 
 |-  ( ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) -> ( ( y E ( A .x. X ) ) ( .r ` W ) ( A .x. X ) ) = ( ( ( y .^ A ) .x. ( y E X ) ) ( .r ` W ) ( A .x. X ) ) )
30 simprr 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> W e. AssAlg )
31 2 eqcomi 
 |-  ( Scalar ` W ) = F
32 31 fveq2i 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` F )
33 5 32 mgpbas 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` G )
34 2 assasca 
 |-  ( W e. AssAlg -> F e. Ring )
35 5 ringmgp 
 |-  ( F e. Ring -> G e. Mnd )
36 34 35 syl 
 |-  ( W e. AssAlg -> G e. Mnd )
37 36 adantl 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> G e. Mnd )
38 37 adantl 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> G e. Mnd )
39 simpl 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> y e. NN0 )
40 3 a1i 
 |-  ( W e. AssAlg -> B = ( Base ` F ) )
41 2 fveq2i 
 |-  ( Base ` F ) = ( Base ` ( Scalar ` W ) )
42 40 41 eqtrdi 
 |-  ( W e. AssAlg -> B = ( Base ` ( Scalar ` W ) ) )
43 42 eleq2d 
 |-  ( W e. AssAlg -> ( A e. B <-> A e. ( Base ` ( Scalar ` W ) ) ) )
44 43 biimpcd 
 |-  ( A e. B -> ( W e. AssAlg -> A e. ( Base ` ( Scalar ` W ) ) ) )
45 44 adantr 
 |-  ( ( A e. B /\ X e. V ) -> ( W e. AssAlg -> A e. ( Base ` ( Scalar ` W ) ) ) )
46 45 imp 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> A e. ( Base ` ( Scalar ` W ) ) )
47 46 adantl 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> A e. ( Base ` ( Scalar ` W ) ) )
48 33 6 38 39 47 mulgnn0cld 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( y .^ A ) e. ( Base ` ( Scalar ` W ) ) )
49 simprlr 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> X e. V )
50 24 8 13 39 49 mulgnn0cld 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( y E X ) e. V )
51 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
52 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
53 1 51 52 4 25 assaass 
 |-  ( ( W e. AssAlg /\ ( ( y .^ A ) e. ( Base ` ( Scalar ` W ) ) /\ ( y E X ) e. V /\ ( A .x. X ) e. V ) ) -> ( ( ( y .^ A ) .x. ( y E X ) ) ( .r ` W ) ( A .x. X ) ) = ( ( y .^ A ) .x. ( ( y E X ) ( .r ` W ) ( A .x. X ) ) ) )
54 30 48 50 22 53 syl13anc 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( ( y .^ A ) .x. ( y E X ) ) ( .r ` W ) ( A .x. X ) ) = ( ( y .^ A ) .x. ( ( y E X ) ( .r ` W ) ( A .x. X ) ) ) )
55 1 51 52 4 25 assaassr 
 |-  ( ( W e. AssAlg /\ ( A e. ( Base ` ( Scalar ` W ) ) /\ ( y E X ) e. V /\ X e. V ) ) -> ( ( y E X ) ( .r ` W ) ( A .x. X ) ) = ( A .x. ( ( y E X ) ( .r ` W ) X ) ) )
56 30 47 50 49 55 syl13anc 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y E X ) ( .r ` W ) ( A .x. X ) ) = ( A .x. ( ( y E X ) ( .r ` W ) X ) ) )
57 56 oveq2d 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y .^ A ) .x. ( ( y E X ) ( .r ` W ) ( A .x. X ) ) ) = ( ( y .^ A ) .x. ( A .x. ( ( y E X ) ( .r ` W ) X ) ) ) )
58 24 8 26 mulgnn0p1 
 |-  ( ( H e. Mnd /\ y e. NN0 /\ X e. V ) -> ( ( y + 1 ) E X ) = ( ( y E X ) ( .r ` W ) X ) )
59 13 39 49 58 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y + 1 ) E X ) = ( ( y E X ) ( .r ` W ) X ) )
60 59 eqcomd 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y E X ) ( .r ` W ) X ) = ( ( y + 1 ) E X ) )
61 60 oveq2d 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( A .x. ( ( y E X ) ( .r ` W ) X ) ) = ( A .x. ( ( y + 1 ) E X ) ) )
62 61 oveq2d 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y .^ A ) .x. ( A .x. ( ( y E X ) ( .r ` W ) X ) ) ) = ( ( y .^ A ) .x. ( A .x. ( ( y + 1 ) E X ) ) ) )
63 17 adantl 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> W e. LMod )
64 peano2nn0 
 |-  ( y e. NN0 -> ( y + 1 ) e. NN0 )
65 64 adantr 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( y + 1 ) e. NN0 )
66 24 8 13 65 49 mulgnn0cld 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y + 1 ) E X ) e. V )
67 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
68 1 51 4 52 67 lmodvsass 
 |-  ( ( W e. LMod /\ ( ( y .^ A ) e. ( Base ` ( Scalar ` W ) ) /\ A e. ( Base ` ( Scalar ` W ) ) /\ ( ( y + 1 ) E X ) e. V ) ) -> ( ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) .x. ( ( y + 1 ) E X ) ) = ( ( y .^ A ) .x. ( A .x. ( ( y + 1 ) E X ) ) ) )
69 68 eqcomd 
 |-  ( ( W e. LMod /\ ( ( y .^ A ) e. ( Base ` ( Scalar ` W ) ) /\ A e. ( Base ` ( Scalar ` W ) ) /\ ( ( y + 1 ) E X ) e. V ) ) -> ( ( y .^ A ) .x. ( A .x. ( ( y + 1 ) E X ) ) ) = ( ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) .x. ( ( y + 1 ) E X ) ) )
70 63 48 47 66 69 syl13anc 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y .^ A ) .x. ( A .x. ( ( y + 1 ) E X ) ) ) = ( ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) .x. ( ( y + 1 ) E X ) ) )
71 57 62 70 3eqtrd 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y .^ A ) .x. ( ( y E X ) ( .r ` W ) ( A .x. X ) ) ) = ( ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) .x. ( ( y + 1 ) E X ) ) )
72 simprll 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> A e. B )
73 5 3 mgpbas 
 |-  B = ( Base ` G )
74 eqid 
 |-  ( .r ` F ) = ( .r ` F )
75 5 74 mgpplusg 
 |-  ( .r ` F ) = ( +g ` G )
76 73 6 75 mulgnn0p1 
 |-  ( ( G e. Mnd /\ y e. NN0 /\ A e. B ) -> ( ( y + 1 ) .^ A ) = ( ( y .^ A ) ( .r ` F ) A ) )
77 38 39 72 76 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y + 1 ) .^ A ) = ( ( y .^ A ) ( .r ` F ) A ) )
78 2 a1i 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> F = ( Scalar ` W ) )
79 78 fveq2d 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( .r ` F ) = ( .r ` ( Scalar ` W ) ) )
80 79 oveqd 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y .^ A ) ( .r ` F ) A ) = ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) )
81 77 80 eqtrd 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y + 1 ) .^ A ) = ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) )
82 81 eqcomd 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) = ( ( y + 1 ) .^ A ) )
83 82 oveq1d 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) .x. ( ( y + 1 ) E X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) )
84 54 71 83 3eqtrd 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( ( y .^ A ) .x. ( y E X ) ) ( .r ` W ) ( A .x. X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) )
85 29 84 sylan9eqr 
 |-  ( ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) /\ ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) ) -> ( ( y E ( A .x. X ) ) ( .r ` W ) ( A .x. X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) )
86 28 85 eqtrd 
 |-  ( ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) /\ ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) ) -> ( ( y + 1 ) E ( A .x. X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) )
87 86 exp31 
 |-  ( y e. NN0 -> ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) -> ( ( y + 1 ) E ( A .x. X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) ) ) )