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 assasca 
 |-  ( W e. AssAlg -> F e. CRing )
32 crngring 
 |-  ( F e. CRing -> F e. Ring )
33 5 ringmgp 
 |-  ( F e. Ring -> G e. Mnd )
34 31 32 33 3syl 
 |-  ( W e. AssAlg -> G e. Mnd )
35 34 adantl 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> G e. Mnd )
36 35 adantl 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> G e. Mnd )
37 simpl 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> y e. NN0 )
38 3 a1i 
 |-  ( W e. AssAlg -> B = ( Base ` F ) )
39 2 fveq2i 
 |-  ( Base ` F ) = ( Base ` ( Scalar ` W ) )
40 38 39 eqtrdi 
 |-  ( W e. AssAlg -> B = ( Base ` ( Scalar ` W ) ) )
41 40 eleq2d 
 |-  ( W e. AssAlg -> ( A e. B <-> A e. ( Base ` ( Scalar ` W ) ) ) )
42 41 biimpcd 
 |-  ( A e. B -> ( W e. AssAlg -> A e. ( Base ` ( Scalar ` W ) ) ) )
43 42 adantr 
 |-  ( ( A e. B /\ X e. V ) -> ( W e. AssAlg -> A e. ( Base ` ( Scalar ` W ) ) ) )
44 43 imp 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> A e. ( Base ` ( Scalar ` W ) ) )
45 44 adantl 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> A e. ( Base ` ( Scalar ` W ) ) )
46 2 eqcomi 
 |-  ( Scalar ` W ) = F
47 46 fveq2i 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` F )
48 5 47 mgpbas 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` G )
49 48 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ y e. NN0 /\ A e. ( Base ` ( Scalar ` W ) ) ) -> ( y .^ A ) e. ( Base ` ( Scalar ` W ) ) )
50 36 37 45 49 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( y .^ A ) e. ( Base ` ( Scalar ` W ) ) )
51 simprlr 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> X e. V )
52 24 8 mulgnn0cl 
 |-  ( ( H e. Mnd /\ y e. NN0 /\ X e. V ) -> ( y E X ) e. V )
53 13 37 51 52 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( y E X ) e. V )
54 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
55 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
56 1 54 55 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 ) ) ) )
57 30 50 53 22 56 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 ) ) ) )
58 1 54 55 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 ) ) )
59 30 45 53 51 58 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 ) ) )
60 59 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 ) ) ) )
61 24 8 26 mulgnn0p1 
 |-  ( ( H e. Mnd /\ y e. NN0 /\ X e. V ) -> ( ( y + 1 ) E X ) = ( ( y E X ) ( .r ` W ) X ) )
62 13 37 51 61 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y + 1 ) E X ) = ( ( y E X ) ( .r ` W ) X ) )
63 62 eqcomd 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y E X ) ( .r ` W ) X ) = ( ( y + 1 ) E X ) )
64 63 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 ) ) )
65 64 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 ) ) ) )
66 17 adantl 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> W e. LMod )
67 peano2nn0 
 |-  ( y e. NN0 -> ( y + 1 ) e. NN0 )
68 67 adantr 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( y + 1 ) e. NN0 )
69 24 8 mulgnn0cl 
 |-  ( ( H e. Mnd /\ ( y + 1 ) e. NN0 /\ X e. V ) -> ( ( y + 1 ) E X ) e. V )
70 13 68 51 69 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y + 1 ) E X ) e. V )
71 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
72 1 54 4 55 71 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 ) ) ) )
73 72 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 ) ) )
74 66 50 45 70 73 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 ) ) )
75 60 65 74 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 ) ) )
76 simprll 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> A e. B )
77 5 3 mgpbas 
 |-  B = ( Base ` G )
78 eqid 
 |-  ( .r ` F ) = ( .r ` F )
79 5 78 mgpplusg 
 |-  ( .r ` F ) = ( +g ` G )
80 77 6 79 mulgnn0p1 
 |-  ( ( G e. Mnd /\ y e. NN0 /\ A e. B ) -> ( ( y + 1 ) .^ A ) = ( ( y .^ A ) ( .r ` F ) A ) )
81 36 37 76 80 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y + 1 ) .^ A ) = ( ( y .^ A ) ( .r ` F ) A ) )
82 2 a1i 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> F = ( Scalar ` W ) )
83 82 fveq2d 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( .r ` F ) = ( .r ` ( Scalar ` W ) ) )
84 83 oveqd 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y .^ A ) ( .r ` F ) A ) = ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) )
85 81 84 eqtrd 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y + 1 ) .^ A ) = ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) )
86 85 eqcomd 
 |-  ( ( y e. NN0 /\ ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) ) -> ( ( y .^ A ) ( .r ` ( Scalar ` W ) ) A ) = ( ( y + 1 ) .^ A ) )
87 86 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 ) ) )
88 57 75 87 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 ) ) )
89 29 88 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 ) ) )
90 28 89 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 ) ) )
91 90 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 ) ) ) ) )