Proof of Theorem assamulgscmlem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | assaring 21881 | . . . . . . . 8
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) | 
| 2 |  | assamulgscm.h | . . . . . . . . 9
⊢ 𝐻 = (mulGrp‘𝑊) | 
| 3 | 2 | ringmgp 20236 | . . . . . . . 8
⊢ (𝑊 ∈ Ring → 𝐻 ∈ Mnd) | 
| 4 | 1, 3 | syl 17 | . . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝐻 ∈ Mnd) | 
| 5 | 4 | adantl 481 | . . . . . 6
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝐻 ∈ Mnd) | 
| 6 | 5 | adantl 481 | . . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝐻 ∈ Mnd) | 
| 7 | 6 | adantr 480 | . . . 4
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → 𝐻 ∈ Mnd) | 
| 8 |  | simpll 767 | . . . 4
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → 𝑦 ∈ ℕ0) | 
| 9 |  | assalmod 21880 | . . . . . . . 8
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) | 
| 10 | 9 | adantl 481 | . . . . . . 7
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝑊 ∈ LMod) | 
| 11 |  | simpll 767 | . . . . . . 7
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝐴 ∈ 𝐵) | 
| 12 |  | simplr 769 | . . . . . . 7
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝑋 ∈ 𝑉) | 
| 13 |  | assamulgscm.v | . . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) | 
| 14 |  | assamulgscm.f | . . . . . . . 8
⊢ 𝐹 = (Scalar‘𝑊) | 
| 15 |  | assamulgscm.s | . . . . . . . 8
⊢  · = (
·𝑠 ‘𝑊) | 
| 16 |  | assamulgscm.b | . . . . . . . 8
⊢ 𝐵 = (Base‘𝐹) | 
| 17 | 13, 14, 15, 16 | lmodvscl 20876 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐴 · 𝑋) ∈ 𝑉) | 
| 18 | 10, 11, 12, 17 | syl3anc 1373 | . . . . . 6
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (𝐴 · 𝑋) ∈ 𝑉) | 
| 19 | 18 | adantl 481 | . . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (𝐴 · 𝑋) ∈ 𝑉) | 
| 20 | 19 | adantr 480 | . . . 4
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → (𝐴 · 𝑋) ∈ 𝑉) | 
| 21 | 2, 13 | mgpbas 20142 | . . . . 5
⊢ 𝑉 = (Base‘𝐻) | 
| 22 |  | assamulgscm.e | . . . . 5
⊢ 𝐸 = (.g‘𝐻) | 
| 23 |  | eqid 2737 | . . . . . 6
⊢
(.r‘𝑊) = (.r‘𝑊) | 
| 24 | 2, 23 | mgpplusg 20141 | . . . . 5
⊢
(.r‘𝑊) = (+g‘𝐻) | 
| 25 | 21, 22, 24 | mulgnn0p1 19103 | . . . 4
⊢ ((𝐻 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ (𝐴 · 𝑋) ∈ 𝑉) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = ((𝑦𝐸(𝐴 · 𝑋))(.r‘𝑊)(𝐴 · 𝑋))) | 
| 26 | 7, 8, 20, 25 | syl3anc 1373 | . . 3
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = ((𝑦𝐸(𝐴 · 𝑋))(.r‘𝑊)(𝐴 · 𝑋))) | 
| 27 |  | oveq1 7438 | . . . 4
⊢ ((𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋)) → ((𝑦𝐸(𝐴 · 𝑋))(.r‘𝑊)(𝐴 · 𝑋)) = (((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))(.r‘𝑊)(𝐴 · 𝑋))) | 
| 28 |  | simprr 773 | . . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝑊 ∈ AssAlg) | 
| 29 |  | assamulgscm.g | . . . . . . . 8
⊢ 𝐺 = (mulGrp‘𝐹) | 
| 30 | 14 | eqcomi 2746 | . . . . . . . . 9
⊢
(Scalar‘𝑊) =
𝐹 | 
| 31 | 30 | fveq2i 6909 | . . . . . . . 8
⊢
(Base‘(Scalar‘𝑊)) = (Base‘𝐹) | 
| 32 | 29, 31 | mgpbas 20142 | . . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘𝐺) | 
| 33 |  | assamulgscm.p | . . . . . . 7
⊢  ↑ =
(.g‘𝐺) | 
| 34 | 14 | assasca 21882 | . . . . . . . . . 10
⊢ (𝑊 ∈ AssAlg → 𝐹 ∈ Ring) | 
| 35 | 29 | ringmgp 20236 | . . . . . . . . . 10
⊢ (𝐹 ∈ Ring → 𝐺 ∈ Mnd) | 
| 36 | 34, 35 | syl 17 | . . . . . . . . 9
⊢ (𝑊 ∈ AssAlg → 𝐺 ∈ Mnd) | 
| 37 | 36 | adantl 481 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝐺 ∈ Mnd) | 
| 38 | 37 | adantl 481 | . . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝐺 ∈ Mnd) | 
| 39 |  | simpl 482 | . . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝑦 ∈ ℕ0) | 
| 40 | 16 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑊 ∈ AssAlg → 𝐵 = (Base‘𝐹)) | 
| 41 | 14 | fveq2i 6909 | . . . . . . . . . . . . 13
⊢
(Base‘𝐹) =
(Base‘(Scalar‘𝑊)) | 
| 42 | 40, 41 | eqtrdi 2793 | . . . . . . . . . . . 12
⊢ (𝑊 ∈ AssAlg → 𝐵 =
(Base‘(Scalar‘𝑊))) | 
| 43 | 42 | eleq2d 2827 | . . . . . . . . . . 11
⊢ (𝑊 ∈ AssAlg → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ (Base‘(Scalar‘𝑊)))) | 
| 44 | 43 | biimpcd 249 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝐵 → (𝑊 ∈ AssAlg → 𝐴 ∈ (Base‘(Scalar‘𝑊)))) | 
| 45 | 44 | adantr 480 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝑊 ∈ AssAlg → 𝐴 ∈ (Base‘(Scalar‘𝑊)))) | 
| 46 | 45 | imp 406 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝐴 ∈ (Base‘(Scalar‘𝑊))) | 
| 47 | 46 | adantl 481 | . . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝐴 ∈ (Base‘(Scalar‘𝑊))) | 
| 48 | 32, 33, 38, 39, 47 | mulgnn0cld 19113 | . . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (𝑦 ↑ 𝐴) ∈ (Base‘(Scalar‘𝑊))) | 
| 49 |  | simprlr 780 | . . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝑋 ∈ 𝑉) | 
| 50 | 21, 22, 6, 39, 49 | mulgnn0cld 19113 | . . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (𝑦𝐸𝑋) ∈ 𝑉) | 
| 51 |  | eqid 2737 | . . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 52 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 53 | 13, 51, 52, 15, 23 | assaass 21878 | . . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ ((𝑦 ↑ 𝐴) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑦𝐸𝑋) ∈ 𝑉 ∧ (𝐴 · 𝑋) ∈ 𝑉)) → (((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))(.r‘𝑊)(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋)))) | 
| 54 | 28, 48, 50, 19, 53 | syl13anc 1374 | . . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))(.r‘𝑊)(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋)))) | 
| 55 | 13, 51, 52, 15, 23 | assaassr 21879 | . . . . . . . 8
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈
(Base‘(Scalar‘𝑊)) ∧ (𝑦𝐸𝑋) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋)) = (𝐴 · ((𝑦𝐸𝑋)(.r‘𝑊)𝑋))) | 
| 56 | 28, 47, 50, 49, 55 | syl13anc 1374 | . . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋)) = (𝐴 · ((𝑦𝐸𝑋)(.r‘𝑊)𝑋))) | 
| 57 | 56 | oveq2d 7447 | . . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴) · ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋))) = ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦𝐸𝑋)(.r‘𝑊)𝑋)))) | 
| 58 | 21, 22, 24 | mulgnn0p1 19103 | . . . . . . . . . 10
⊢ ((𝐻 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝑉) → ((𝑦 + 1)𝐸𝑋) = ((𝑦𝐸𝑋)(.r‘𝑊)𝑋)) | 
| 59 | 6, 39, 49, 58 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 + 1)𝐸𝑋) = ((𝑦𝐸𝑋)(.r‘𝑊)𝑋)) | 
| 60 | 59 | eqcomd 2743 | . . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦𝐸𝑋)(.r‘𝑊)𝑋) = ((𝑦 + 1)𝐸𝑋)) | 
| 61 | 60 | oveq2d 7447 | . . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (𝐴 · ((𝑦𝐸𝑋)(.r‘𝑊)𝑋)) = (𝐴 · ((𝑦 + 1)𝐸𝑋))) | 
| 62 | 61 | oveq2d 7447 | . . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦𝐸𝑋)(.r‘𝑊)𝑋))) = ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦 + 1)𝐸𝑋)))) | 
| 63 | 10 | adantl 481 | . . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝑊 ∈ LMod) | 
| 64 |  | peano2nn0 12566 | . . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ0) | 
| 65 | 64 | adantr 480 | . . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (𝑦 + 1) ∈
ℕ0) | 
| 66 | 21, 22, 6, 65, 49 | mulgnn0cld 19113 | . . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 + 1)𝐸𝑋) ∈ 𝑉) | 
| 67 |  | eqid 2737 | . . . . . . . . 9
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) | 
| 68 | 13, 51, 15, 52, 67 | lmodvsass 20885 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ ((𝑦 ↑ 𝐴) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝐴 ∈ (Base‘(Scalar‘𝑊)) ∧ ((𝑦 + 1)𝐸𝑋) ∈ 𝑉)) → (((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) · ((𝑦 + 1)𝐸𝑋)) = ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦 + 1)𝐸𝑋)))) | 
| 69 | 68 | eqcomd 2743 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ ((𝑦 ↑ 𝐴) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝐴 ∈ (Base‘(Scalar‘𝑊)) ∧ ((𝑦 + 1)𝐸𝑋) ∈ 𝑉)) → ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦 + 1)𝐸𝑋))) = (((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) · ((𝑦 + 1)𝐸𝑋))) | 
| 70 | 63, 48, 47, 66, 69 | syl13anc 1374 | . . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦 + 1)𝐸𝑋))) = (((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) · ((𝑦 + 1)𝐸𝑋))) | 
| 71 | 57, 62, 70 | 3eqtrd 2781 | . . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴) · ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋))) = (((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) · ((𝑦 + 1)𝐸𝑋))) | 
| 72 |  | simprll 779 | . . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝐴 ∈ 𝐵) | 
| 73 | 29, 16 | mgpbas 20142 | . . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) | 
| 74 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(.r‘𝐹) = (.r‘𝐹) | 
| 75 | 29, 74 | mgpplusg 20141 | . . . . . . . . . 10
⊢
(.r‘𝐹) = (+g‘𝐺) | 
| 76 | 73, 33, 75 | mulgnn0p1 19103 | . . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝐴 ∈ 𝐵) → ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(.r‘𝐹)𝐴)) | 
| 77 | 38, 39, 72, 76 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(.r‘𝐹)𝐴)) | 
| 78 | 14 | a1i 11 | . . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝐹 = (Scalar‘𝑊)) | 
| 79 | 78 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) →
(.r‘𝐹) =
(.r‘(Scalar‘𝑊))) | 
| 80 | 79 | oveqd 7448 | . . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴)(.r‘𝐹)𝐴) = ((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴)) | 
| 81 | 77, 80 | eqtrd 2777 | . . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴)) | 
| 82 | 81 | eqcomd 2743 | . . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) = ((𝑦 + 1) ↑ 𝐴)) | 
| 83 | 82 | oveq1d 7446 | . . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) · ((𝑦 + 1)𝐸𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))) | 
| 84 | 54, 71, 83 | 3eqtrd 2781 | . . . 4
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))(.r‘𝑊)(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))) | 
| 85 | 27, 84 | sylan9eqr 2799 | . . 3
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → ((𝑦𝐸(𝐴 · 𝑋))(.r‘𝑊)(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))) | 
| 86 | 26, 85 | eqtrd 2777 | . 2
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))) | 
| 87 | 86 | exp31 419 | 1
⊢ (𝑦 ∈ ℕ0
→ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → ((𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋)) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))))) |