Proof of Theorem assamulgscmlem2
Step | Hyp | Ref
| Expression |
1 | | assaring 21267 |
. . . . . . . 8
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
2 | | assamulgscm.h |
. . . . . . . . 9
⊢ 𝐻 = (mulGrp‘𝑊) |
3 | 2 | ringmgp 19970 |
. . . . . . . 8
⊢ (𝑊 ∈ Ring → 𝐻 ∈ Mnd) |
4 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝐻 ∈ Mnd) |
5 | 4 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝐻 ∈ Mnd) |
6 | 5 | adantl 482 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝐻 ∈ Mnd) |
7 | 6 | adantr 481 |
. . . 4
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → 𝐻 ∈ Mnd) |
8 | | simpll 765 |
. . . 4
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → 𝑦 ∈ ℕ0) |
9 | | assalmod 21266 |
. . . . . . . 8
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
10 | 9 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝑊 ∈ LMod) |
11 | | simpll 765 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝐴 ∈ 𝐵) |
12 | | simplr 767 |
. . . . . . 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 20339 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐴 · 𝑋) ∈ 𝑉) |
18 | 10, 11, 12, 17 | syl3anc 1371 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → (𝐴 · 𝑋) ∈ 𝑉) |
19 | 18 | adantl 482 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (𝐴 · 𝑋) ∈ 𝑉) |
20 | 19 | adantr 481 |
. . . 4
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → (𝐴 · 𝑋) ∈ 𝑉) |
21 | 2, 13 | mgpbas 19902 |
. . . . 5
⊢ 𝑉 = (Base‘𝐻) |
22 | | assamulgscm.e |
. . . . 5
⊢ 𝐸 = (.g‘𝐻) |
23 | | eqid 2736 |
. . . . . 6
⊢
(.r‘𝑊) = (.r‘𝑊) |
24 | 2, 23 | mgpplusg 19900 |
. . . . 5
⊢
(.r‘𝑊) = (+g‘𝐻) |
25 | 21, 22, 24 | mulgnn0p1 18887 |
. . . 4
⊢ ((𝐻 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ (𝐴 · 𝑋) ∈ 𝑉) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = ((𝑦𝐸(𝐴 · 𝑋))(.r‘𝑊)(𝐴 · 𝑋))) |
26 | 7, 8, 20, 25 | syl3anc 1371 |
. . 3
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = ((𝑦𝐸(𝐴 · 𝑋))(.r‘𝑊)(𝐴 · 𝑋))) |
27 | | oveq1 7364 |
. . . 4
⊢ ((𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋)) → ((𝑦𝐸(𝐴 · 𝑋))(.r‘𝑊)(𝐴 · 𝑋)) = (((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))(.r‘𝑊)(𝐴 · 𝑋))) |
28 | | simprr 771 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝑊 ∈ AssAlg) |
29 | | assamulgscm.g |
. . . . . . . 8
⊢ 𝐺 = (mulGrp‘𝐹) |
30 | 14 | eqcomi 2745 |
. . . . . . . . 9
⊢
(Scalar‘𝑊) =
𝐹 |
31 | 30 | fveq2i 6845 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑊)) = (Base‘𝐹) |
32 | 29, 31 | mgpbas 19902 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘𝐺) |
33 | | assamulgscm.p |
. . . . . . 7
⊢ ↑ =
(.g‘𝐺) |
34 | 14 | assasca 21268 |
. . . . . . . . . 10
⊢ (𝑊 ∈ AssAlg → 𝐹 ∈ CRing) |
35 | | crngring 19976 |
. . . . . . . . . 10
⊢ (𝐹 ∈ CRing → 𝐹 ∈ Ring) |
36 | 29 | ringmgp 19970 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Ring → 𝐺 ∈ Mnd) |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑊 ∈ AssAlg → 𝐺 ∈ Mnd) |
38 | 37 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝐺 ∈ Mnd) |
39 | 38 | adantl 482 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝐺 ∈ Mnd) |
40 | | simpl 483 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝑦 ∈ ℕ0) |
41 | 16 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ AssAlg → 𝐵 = (Base‘𝐹)) |
42 | 14 | fveq2i 6845 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐹) =
(Base‘(Scalar‘𝑊)) |
43 | 41, 42 | eqtrdi 2792 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ AssAlg → 𝐵 =
(Base‘(Scalar‘𝑊))) |
44 | 43 | eleq2d 2823 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ AssAlg → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ (Base‘(Scalar‘𝑊)))) |
45 | 44 | biimpcd 248 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐵 → (𝑊 ∈ AssAlg → 𝐴 ∈ (Base‘(Scalar‘𝑊)))) |
46 | 45 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝑊 ∈ AssAlg → 𝐴 ∈ (Base‘(Scalar‘𝑊)))) |
47 | 46 | imp 407 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → 𝐴 ∈ (Base‘(Scalar‘𝑊))) |
48 | 47 | adantl 482 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝐴 ∈ (Base‘(Scalar‘𝑊))) |
49 | 32, 33, 39, 40, 48 | mulgnn0cld 18897 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (𝑦 ↑ 𝐴) ∈ (Base‘(Scalar‘𝑊))) |
50 | | simprlr 778 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝑋 ∈ 𝑉) |
51 | 21, 22, 6, 40, 50 | mulgnn0cld 18897 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (𝑦𝐸𝑋) ∈ 𝑉) |
52 | | eqid 2736 |
. . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
53 | | eqid 2736 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
54 | 13, 52, 53, 15, 23 | assaass 21264 |
. . . . . 6
⊢ ((𝑊 ∈ AssAlg ∧ ((𝑦 ↑ 𝐴) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑦𝐸𝑋) ∈ 𝑉 ∧ (𝐴 · 𝑋) ∈ 𝑉)) → (((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))(.r‘𝑊)(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋)))) |
55 | 28, 49, 51, 19, 54 | syl13anc 1372 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))(.r‘𝑊)(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋)))) |
56 | 13, 52, 53, 15, 23 | assaassr 21265 |
. . . . . . . 8
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴 ∈
(Base‘(Scalar‘𝑊)) ∧ (𝑦𝐸𝑋) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋)) = (𝐴 · ((𝑦𝐸𝑋)(.r‘𝑊)𝑋))) |
57 | 28, 48, 51, 50, 56 | syl13anc 1372 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋)) = (𝐴 · ((𝑦𝐸𝑋)(.r‘𝑊)𝑋))) |
58 | 57 | oveq2d 7373 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴) · ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋))) = ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦𝐸𝑋)(.r‘𝑊)𝑋)))) |
59 | 21, 22, 24 | mulgnn0p1 18887 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝑉) → ((𝑦 + 1)𝐸𝑋) = ((𝑦𝐸𝑋)(.r‘𝑊)𝑋)) |
60 | 6, 40, 50, 59 | syl3anc 1371 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 + 1)𝐸𝑋) = ((𝑦𝐸𝑋)(.r‘𝑊)𝑋)) |
61 | 60 | eqcomd 2742 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦𝐸𝑋)(.r‘𝑊)𝑋) = ((𝑦 + 1)𝐸𝑋)) |
62 | 61 | oveq2d 7373 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (𝐴 · ((𝑦𝐸𝑋)(.r‘𝑊)𝑋)) = (𝐴 · ((𝑦 + 1)𝐸𝑋))) |
63 | 62 | oveq2d 7373 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦𝐸𝑋)(.r‘𝑊)𝑋))) = ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦 + 1)𝐸𝑋)))) |
64 | 10 | adantl 482 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝑊 ∈ LMod) |
65 | | peano2nn0 12453 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ0) |
66 | 65 | adantr 481 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (𝑦 + 1) ∈
ℕ0) |
67 | 21, 22, 6, 66, 50 | mulgnn0cld 18897 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 + 1)𝐸𝑋) ∈ 𝑉) |
68 | | eqid 2736 |
. . . . . . . . 9
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
69 | 13, 52, 15, 53, 68 | lmodvsass 20347 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ ((𝑦 ↑ 𝐴) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝐴 ∈ (Base‘(Scalar‘𝑊)) ∧ ((𝑦 + 1)𝐸𝑋) ∈ 𝑉)) → (((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) · ((𝑦 + 1)𝐸𝑋)) = ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦 + 1)𝐸𝑋)))) |
70 | 69 | eqcomd 2742 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ ((𝑦 ↑ 𝐴) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝐴 ∈ (Base‘(Scalar‘𝑊)) ∧ ((𝑦 + 1)𝐸𝑋) ∈ 𝑉)) → ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦 + 1)𝐸𝑋))) = (((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) · ((𝑦 + 1)𝐸𝑋))) |
71 | 64, 49, 48, 67, 70 | syl13anc 1372 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴) · (𝐴 · ((𝑦 + 1)𝐸𝑋))) = (((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) · ((𝑦 + 1)𝐸𝑋))) |
72 | 58, 63, 71 | 3eqtrd 2780 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴) · ((𝑦𝐸𝑋)(.r‘𝑊)(𝐴 · 𝑋))) = (((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) · ((𝑦 + 1)𝐸𝑋))) |
73 | | simprll 777 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝐴 ∈ 𝐵) |
74 | 29, 16 | mgpbas 19902 |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
75 | | eqid 2736 |
. . . . . . . . . . 11
⊢
(.r‘𝐹) = (.r‘𝐹) |
76 | 29, 75 | mgpplusg 19900 |
. . . . . . . . . 10
⊢
(.r‘𝐹) = (+g‘𝐺) |
77 | 74, 33, 76 | mulgnn0p1 18887 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝐴 ∈ 𝐵) → ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(.r‘𝐹)𝐴)) |
78 | 39, 40, 73, 77 | syl3anc 1371 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(.r‘𝐹)𝐴)) |
79 | 14 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → 𝐹 = (Scalar‘𝑊)) |
80 | 79 | fveq2d 6846 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) →
(.r‘𝐹) =
(.r‘(Scalar‘𝑊))) |
81 | 80 | oveqd 7374 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴)(.r‘𝐹)𝐴) = ((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴)) |
82 | 78, 81 | eqtrd 2776 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴)) |
83 | 82 | eqcomd 2742 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → ((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) = ((𝑦 + 1) ↑ 𝐴)) |
84 | 83 | oveq1d 7372 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (((𝑦 ↑ 𝐴)(.r‘(Scalar‘𝑊))𝐴) · ((𝑦 + 1)𝐸𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))) |
85 | 55, 72, 84 | 3eqtrd 2780 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) → (((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))(.r‘𝑊)(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))) |
86 | 27, 85 | sylan9eqr 2798 |
. . 3
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → ((𝑦𝐸(𝐴 · 𝑋))(.r‘𝑊)(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))) |
87 | 26, 86 | eqtrd 2776 |
. 2
⊢ (((𝑦 ∈ ℕ0
∧ ((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋))) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))) |
88 | 87 | exp31 420 |
1
⊢ (𝑦 ∈ ℕ0
→ (((𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ AssAlg) → ((𝑦𝐸(𝐴 · 𝑋)) = ((𝑦 ↑ 𝐴) · (𝑦𝐸𝑋)) → ((𝑦 + 1)𝐸(𝐴 · 𝑋)) = (((𝑦 + 1) ↑ 𝐴) · ((𝑦 + 1)𝐸𝑋))))) |