This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqcomi ⊢ ( Scalar ‘ 𝑊 ) = 𝐹
32 31 fveq2i ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ 𝐹 )
33 5 32 mgpbas ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ 𝐺 )
34 2 assasca ⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ Ring )
35 5 ringmgp ⊢ ( 𝐹 ∈ Ring → 𝐺 ∈ Mnd )
36 34 35 syl ⊢ ( 𝑊 ∈ AssAlg → 𝐺 ∈ Mnd )
37 36 adantl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐺 ∈ Mnd )
38 37 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐺 ∈ Mnd )
39 simpl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑦 ∈ ℕ0 )
40 3 a1i ⊢ ( 𝑊 ∈ AssAlg → 𝐵 = ( Base ‘ 𝐹 ) )
41 2 fveq2i ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
42 40 41 eqtrdi ⊢ ( 𝑊 ∈ AssAlg → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
43 42 eleq2d ⊢ ( 𝑊 ∈ AssAlg → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
44 43 biimpcd ⊢ ( 𝐴 ∈ 𝐵 → ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
45 44 adantr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
46 45 imp ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
47 46 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
48 33 6 38 39 47 mulgnn0cld ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
49 simprlr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑋 ∈ 𝑉 )
50 24 8 13 39 49 mulgnn0cld ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝑦 𝐸 𝑋 ) ∈ 𝑉 )
51 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
52 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
53 1 51 52 4 25 assaass ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑦 𝐸 𝑋 ) ∈ 𝑉 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ) ) → ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) )
54 30 48 50 22 53 syl13anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) )
55 1 51 52 4 25 assaassr ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑦 𝐸 𝑋 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) )
56 30 47 50 49 55 syl13anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) )
57 56 oveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) ) )
58 24 8 26 mulgnn0p1 ⊢ ( ( 𝐻 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑦 + 1 ) 𝐸 𝑋 ) = ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) )
59 13 39 49 58 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) 𝐸 𝑋 ) = ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) )
60 59 eqcomd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) = ( ( 𝑦 + 1 ) 𝐸 𝑋 ) )
61 60 oveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) = ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
62 61 oveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) )
63 17 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑊 ∈ LMod )
64 peano2nn0 ⊢ ( 𝑦 ∈ ℕ0 → ( 𝑦 + 1 ) ∈ ℕ0 )
65 64 adantr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝑦 + 1 ) ∈ ℕ0 )
66 24 8 13 65 49 mulgnn0cld ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ∈ 𝑉 )
67 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
68 1 51 4 52 67 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ∈ 𝑉 ) ) → ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) )
69 68 eqcomd ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ∈ 𝑉 ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) = ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
70 63 48 47 66 69 syl13anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) = ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
71 57 62 70 3eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) = ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
72 simprll ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐴 ∈ 𝐵 )
73 5 3 mgpbas ⊢ 𝐵 = ( Base ‘ 𝐺 )
74 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
75 5 74 mgpplusg ⊢ ( .r ‘ 𝐹 ) = ( +g ‘ 𝐺 )
76 73 6 75 mulgnn0p1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) )
77 38 39 72 76 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) )
78 2 a1i ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐹 = ( Scalar ‘ 𝑊 ) )
79 78 fveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( .r ‘ 𝐹 ) = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
80 79 oveqd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) )
81 77 80 eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) )
82 81 eqcomd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) = ( ( 𝑦 + 1 ) ↑ 𝐴 ) )
83 82 oveq1d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
84 54 71 83 3eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
85 29 84 sylan9eqr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
86 28 85 eqtrd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
87 86 exp31 ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) ) )