Metamath Proof Explorer

Theorem assamulgscmlem2

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

Ref Expression
Hypotheses assamulgscm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
assamulgscm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
assamulgscm.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
assamulgscm.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
assamulgscm.g ⊢ 𝐺 = ( mulGrp ‘ 𝐹 )
assamulgscm.p ⊢ ↑ = ( .g ‘ 𝐺 )
assamulgscm.h ⊢ 𝐻 = ( mulGrp ‘ 𝑊 )
assamulgscm.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
Assertion assamulgscmlem2 ( 𝑦 ∈ ℕ0 → ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 assamulgscm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 assamulgscm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 assamulgscm.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
4 assamulgscm.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 assamulgscm.g ⊢ 𝐺 = ( mulGrp ‘ 𝐹 )
6 assamulgscm.p ⊢ ↑ = ( .g ‘ 𝐺 )
7 assamulgscm.h ⊢ 𝐻 = ( mulGrp ‘ 𝑊 )
8 assamulgscm.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
9 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
10 7 ringmgp ⊢ ( 𝑊 ∈ Ring → 𝐻 ∈ Mnd )
11 9 10 syl ⊢ ( 𝑊 ∈ AssAlg → 𝐻 ∈ Mnd )
12 11 adantl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐻 ∈ Mnd )
13 12 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐻 ∈ Mnd )
14 13 adantr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → 𝐻 ∈ Mnd )
15 simpll ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → 𝑦 ∈ ℕ0 )
16 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
17 16 adantl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝑊 ∈ LMod )
18 simpll ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐴 ∈ 𝐵 )
19 simplr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝑋 ∈ 𝑉 )
20 1 2 4 3 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
21 17 18 19 20 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
22 21 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
23 22 adantr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
24 7 1 mgpbas ⊢ 𝑉 = ( Base ‘ 𝐻 )
25 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
26 7 25 mgpplusg ⊢ ( .r ‘ 𝑊 ) = ( +g ‘ 𝐻 )
27 24 8 26 mulgnn0p1 ⊢ ( ( 𝐻 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) )
28 14 15 23 27 syl3anc ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) )
29 oveq1 ⊢ ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) )
30 simprr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑊 ∈ AssAlg )
31 2 assasca ⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ CRing )
32 crngring ⊢ ( 𝐹 ∈ CRing → 𝐹 ∈ Ring )
33 5 ringmgp ⊢ ( 𝐹 ∈ Ring → 𝐺 ∈ Mnd )
34 31 32 33 3syl ⊢ ( 𝑊 ∈ AssAlg → 𝐺 ∈ Mnd )
35 34 adantl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐺 ∈ Mnd )
36 35 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐺 ∈ Mnd )
37 simpl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑦 ∈ ℕ0 )
38 3 a1i ⊢ ( 𝑊 ∈ AssAlg → 𝐵 = ( Base ‘ 𝐹 ) )
39 2 fveq2i ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
40 38 39 eqtrdi ⊢ ( 𝑊 ∈ AssAlg → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
41 40 eleq2d ⊢ ( 𝑊 ∈ AssAlg → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
42 41 biimpcd ⊢ ( 𝐴 ∈ 𝐵 → ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
43 42 adantr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
44 43 imp ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
45 44 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
46 2 eqcomi ⊢ ( Scalar ‘ 𝑊 ) = 𝐹
47 46 fveq2i ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ 𝐹 )
48 5 47 mgpbas ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ 𝐺 )
49 48 6 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
50 36 37 45 49 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
51 simprlr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑋 ∈ 𝑉 )
52 24 8 mulgnn0cl ⊢ ( ( 𝐻 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑦 𝐸 𝑋 ) ∈ 𝑉 )
53 13 37 51 52 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝑦 𝐸 𝑋 ) ∈ 𝑉 )
54 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
55 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
56 1 54 55 4 25 assaass ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑦 𝐸 𝑋 ) ∈ 𝑉 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ) ) → ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) )
57 30 50 53 22 56 syl13anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) )
58 1 54 55 4 25 assaassr ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑦 𝐸 𝑋 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) )
59 30 45 53 51 58 syl13anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) )
60 59 oveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) ) )
61 24 8 26 mulgnn0p1 ⊢ ( ( 𝐻 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑦 + 1 ) 𝐸 𝑋 ) = ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) )
62 13 37 51 61 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) 𝐸 𝑋 ) = ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) )
63 62 eqcomd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) = ( ( 𝑦 + 1 ) 𝐸 𝑋 ) )
64 63 oveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) = ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
65 64 oveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) )
66 17 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑊 ∈ LMod )
67 peano2nn0 ⊢ ( 𝑦 ∈ ℕ0 → ( 𝑦 + 1 ) ∈ ℕ0 )
68 67 adantr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝑦 + 1 ) ∈ ℕ0 )
69 24 8 mulgnn0cl ⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑦 + 1 ) ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ∈ 𝑉 )
70 13 68 51 69 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ∈ 𝑉 )
71 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
72 1 54 4 55 71 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ∈ 𝑉 ) ) → ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) )
73 72 eqcomd ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ∈ 𝑉 ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) = ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
74 66 50 45 70 73 syl13anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) = ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
75 60 65 74 3eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) = ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
76 simprll ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐴 ∈ 𝐵 )
77 5 3 mgpbas ⊢ 𝐵 = ( Base ‘ 𝐺 )
78 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
79 5 78 mgpplusg ⊢ ( .r ‘ 𝐹 ) = ( +g ‘ 𝐺 )
80 77 6 79 mulgnn0p1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) )
81 36 37 76 80 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) )
82 2 a1i ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐹 = ( Scalar ‘ 𝑊 ) )
83 82 fveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( .r ‘ 𝐹 ) = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
84 83 oveqd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) )
85 81 84 eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) )
86 85 eqcomd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) = ( ( 𝑦 + 1 ) ↑ 𝐴 ) )
87 86 oveq1d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
88 57 75 87 3eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
89 29 88 sylan9eqr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
90 28 89 eqtrd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
91 90 exp31 ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) ) )