| Step | Hyp | Ref
| Expression |
| 1 | | coe1tm.k |
. . . 4
⊢ 𝐾 = (Base‘𝑅) |
| 2 | | coe1tm.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
| 3 | | coe1tm.x |
. . . 4
⊢ 𝑋 = (var1‘𝑅) |
| 4 | | coe1tm.m |
. . . 4
⊢ · = (
·𝑠 ‘𝑃) |
| 5 | | coe1tm.n |
. . . 4
⊢ 𝑁 = (mulGrp‘𝑃) |
| 6 | | coe1tm.e |
. . . 4
⊢ ↑ =
(.g‘𝑁) |
| 7 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 8 | 1, 2, 3, 4, 5, 6, 7 | ply1tmcl 22275 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) ∈ (Base‘𝑃)) |
| 9 | | eqid 2737 |
. . . 4
⊢
(coe1‘(𝐶 · (𝐷 ↑ 𝑋))) = (coe1‘(𝐶 · (𝐷 ↑ 𝑋))) |
| 10 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ ℕ0
↦ (1o × {𝑥})) = (𝑥 ∈ ℕ0 ↦
(1o × {𝑥})) |
| 11 | 9, 7, 2, 10 | coe1fval2 22212 |
. . 3
⊢ ((𝐶 · (𝐷 ↑ 𝑋)) ∈ (Base‘𝑃) → (coe1‘(𝐶 · (𝐷 ↑ 𝑋))) = ((𝐶 · (𝐷 ↑ 𝑋)) ∘ (𝑥 ∈ ℕ0 ↦
(1o × {𝑥})))) |
| 12 | 8, 11 | syl 17 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) →
(coe1‘(𝐶
·
(𝐷 ↑ 𝑋))) = ((𝐶 · (𝐷 ↑ 𝑋)) ∘ (𝑥 ∈ ℕ0 ↦
(1o × {𝑥})))) |
| 13 | | fconst6g 6797 |
. . . . 5
⊢ (𝑥 ∈ ℕ0
→ (1o × {𝑥}):1o⟶ℕ0) |
| 14 | | nn0ex 12532 |
. . . . . 6
⊢
ℕ0 ∈ V |
| 15 | | 1oex 8516 |
. . . . . 6
⊢
1o ∈ V |
| 16 | 14, 15 | elmap 8911 |
. . . . 5
⊢
((1o × {𝑥}) ∈ (ℕ0
↑m 1o) ↔ (1o × {𝑥}):1o⟶ℕ0) |
| 17 | 13, 16 | sylibr 234 |
. . . 4
⊢ (𝑥 ∈ ℕ0
→ (1o × {𝑥}) ∈ (ℕ0
↑m 1o)) |
| 18 | 17 | adantl 481 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (1o × {𝑥}) ∈ (ℕ0
↑m 1o)) |
| 19 | | eqidd 2738 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑥 ∈ ℕ0
↦ (1o × {𝑥})) = (𝑥 ∈ ℕ0 ↦
(1o × {𝑥}))) |
| 20 | | eqid 2737 |
. . . . . . . 8
⊢
(.g‘(mulGrp‘(1o mPoly 𝑅))) =
(.g‘(mulGrp‘(1o mPoly 𝑅))) |
| 21 | 5, 7 | mgpbas 20142 |
. . . . . . . . 9
⊢
(Base‘𝑃) =
(Base‘𝑁) |
| 22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘𝑃) =
(Base‘𝑁)) |
| 23 | | eqid 2737 |
. . . . . . . . . 10
⊢
(mulGrp‘(1o mPoly 𝑅)) = (mulGrp‘(1o mPoly
𝑅)) |
| 24 | 2, 7 | ply1bas 22196 |
. . . . . . . . . 10
⊢
(Base‘𝑃) =
(Base‘(1o mPoly 𝑅)) |
| 25 | 23, 24 | mgpbas 20142 |
. . . . . . . . 9
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘(1o mPoly 𝑅))) |
| 26 | 25 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘𝑃) =
(Base‘(mulGrp‘(1o mPoly 𝑅)))) |
| 27 | | ssv 4008 |
. . . . . . . . 9
⊢
(Base‘𝑃)
⊆ V |
| 28 | 27 | a1i 11 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘𝑃) ⊆
V) |
| 29 | | ovexd 7466 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (𝑥(+g‘𝑁)𝑦) ∈ V) |
| 30 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 31 | 5, 30 | mgpplusg 20141 |
. . . . . . . . . . 11
⊢
(.r‘𝑃) = (+g‘𝑁) |
| 32 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(1o mPoly 𝑅) = (1o mPoly 𝑅) |
| 33 | 2, 32, 30 | ply1mulr 22227 |
. . . . . . . . . . . 12
⊢
(.r‘𝑃) = (.r‘(1o
mPoly 𝑅)) |
| 34 | 23, 33 | mgpplusg 20141 |
. . . . . . . . . . 11
⊢
(.r‘𝑃) =
(+g‘(mulGrp‘(1o mPoly 𝑅))) |
| 35 | 31, 34 | eqtr3i 2767 |
. . . . . . . . . 10
⊢
(+g‘𝑁) =
(+g‘(mulGrp‘(1o mPoly 𝑅))) |
| 36 | 35 | a1i 11 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(+g‘𝑁) =
(+g‘(mulGrp‘(1o mPoly 𝑅)))) |
| 37 | 36 | oveqdr 7459 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (𝑥(+g‘𝑁)𝑦) = (𝑥(+g‘(mulGrp‘(1o
mPoly 𝑅)))𝑦)) |
| 38 | 6, 20, 22, 26, 28, 29, 37 | mulgpropd 19134 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → ↑ =
(.g‘(mulGrp‘(1o mPoly 𝑅)))) |
| 39 | 38 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → ↑ =
(.g‘(mulGrp‘(1o mPoly 𝑅)))) |
| 40 | | eqidd 2738 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝐷 = 𝐷) |
| 41 | 3 | vr1val 22193 |
. . . . . . 7
⊢ 𝑋 = ((1o mVar 𝑅)‘∅) |
| 42 | 41 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝑋 = ((1o mVar 𝑅)‘∅)) |
| 43 | 39, 40, 42 | oveq123d 7452 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐷 ↑ 𝑋) = (𝐷(.g‘(mulGrp‘(1o
mPoly 𝑅)))((1o mVar
𝑅)‘∅))) |
| 44 | 43 | oveq2d 7447 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) = (𝐶 · (𝐷(.g‘(mulGrp‘(1o
mPoly 𝑅)))((1o mVar
𝑅)‘∅)))) |
| 45 | | psr1baslem 22186 |
. . . . . 6
⊢
(ℕ0 ↑m 1o) = {𝑎 ∈ (ℕ0
↑m 1o) ∣ (◡𝑎 “ ℕ) ∈
Fin} |
| 46 | | coe1tm.z |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
| 47 | | eqid 2737 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 48 | | 1on 8518 |
. . . . . . 7
⊢
1o ∈ On |
| 49 | 48 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) →
1o ∈ On) |
| 50 | | eqid 2737 |
. . . . . 6
⊢
(1o mVar 𝑅) = (1o mVar 𝑅) |
| 51 | | simp1 1137 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝑅 ∈ Ring) |
| 52 | | 0lt1o 8542 |
. . . . . . 7
⊢ ∅
∈ 1o |
| 53 | 52 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → ∅
∈ 1o) |
| 54 | | simp3 1139 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝐷 ∈
ℕ0) |
| 55 | 32, 45, 46, 47, 49, 23, 20, 50, 51, 53, 54 | mplcoe3 22056 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑦 ∈ (ℕ0
↑m 1o) ↦ if(𝑦 = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)), (1r‘𝑅), 0 )) = (𝐷(.g‘(mulGrp‘(1o
mPoly 𝑅)))((1o mVar
𝑅)‘∅))) |
| 56 | 55 | oveq2d 7447 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝑦 ∈ (ℕ0
↑m 1o) ↦ if(𝑦 = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)), (1r‘𝑅), 0 ))) = (𝐶 · (𝐷(.g‘(mulGrp‘(1o
mPoly 𝑅)))((1o mVar
𝑅)‘∅)))) |
| 57 | 2, 32, 4 | ply1vsca 22226 |
. . . . 5
⊢ · = (
·𝑠 ‘(1o mPoly 𝑅)) |
| 58 | | elsni 4643 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ {∅} → 𝑏 = ∅) |
| 59 | | df1o2 8513 |
. . . . . . . . . . 11
⊢
1o = {∅} |
| 60 | 58, 59 | eleq2s 2859 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 1o →
𝑏 =
∅) |
| 61 | 60 | iftrued 4533 |
. . . . . . . . 9
⊢ (𝑏 ∈ 1o →
if(𝑏 = ∅, 𝐷, 0) = 𝐷) |
| 62 | 61 | adantl 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑏 ∈ 1o) →
if(𝑏 = ∅, 𝐷, 0) = 𝐷) |
| 63 | 62 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑏 ∈ 1o ↦
if(𝑏 = ∅, 𝐷, 0)) = (𝑏 ∈ 1o ↦ 𝐷)) |
| 64 | | fconstmpt 5747 |
. . . . . . 7
⊢
(1o × {𝐷}) = (𝑏 ∈ 1o ↦ 𝐷) |
| 65 | 63, 64 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑏 ∈ 1o ↦
if(𝑏 = ∅, 𝐷, 0)) = (1o ×
{𝐷})) |
| 66 | | fconst6g 6797 |
. . . . . . . 8
⊢ (𝐷 ∈ ℕ0
→ (1o × {𝐷}):1o⟶ℕ0) |
| 67 | 14, 15 | elmap 8911 |
. . . . . . . 8
⊢
((1o × {𝐷}) ∈ (ℕ0
↑m 1o) ↔ (1o × {𝐷}):1o⟶ℕ0) |
| 68 | 66, 67 | sylibr 234 |
. . . . . . 7
⊢ (𝐷 ∈ ℕ0
→ (1o × {𝐷}) ∈ (ℕ0
↑m 1o)) |
| 69 | 68 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) →
(1o × {𝐷})
∈ (ℕ0 ↑m 1o)) |
| 70 | 65, 69 | eqeltrd 2841 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑏 ∈ 1o ↦
if(𝑏 = ∅, 𝐷, 0)) ∈
(ℕ0 ↑m 1o)) |
| 71 | | simp2 1138 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → 𝐶 ∈ 𝐾) |
| 72 | 32, 57, 45, 47, 46, 1, 49, 51, 70, 71 | mplmon2 22085 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝑦 ∈ (ℕ0
↑m 1o) ↦ if(𝑦 = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)), (1r‘𝑅), 0 ))) = (𝑦 ∈ (ℕ0
↑m 1o) ↦ if(𝑦 = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ))) |
| 73 | 44, 56, 72 | 3eqtr2d 2783 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝐶 · (𝐷 ↑ 𝑋)) = (𝑦 ∈ (ℕ0
↑m 1o) ↦ if(𝑦 = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ))) |
| 74 | | eqeq1 2741 |
. . . 4
⊢ (𝑦 = (1o × {𝑥}) → (𝑦 = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)) ↔ (1o × {𝑥}) = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)))) |
| 75 | 74 | ifbid 4549 |
. . 3
⊢ (𝑦 = (1o × {𝑥}) → if(𝑦 = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ) = if((1o
× {𝑥}) = (𝑏 ∈ 1o ↦
if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 )) |
| 76 | 18, 19, 73, 75 | fmptco 7149 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → ((𝐶 · (𝐷 ↑ 𝑋)) ∘ (𝑥 ∈ ℕ0 ↦
(1o × {𝑥}))) = (𝑥 ∈ ℕ0 ↦
if((1o × {𝑥}) = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ))) |
| 77 | 65 | adantr 480 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (𝑏 ∈
1o ↦ if(𝑏
= ∅, 𝐷, 0)) =
(1o × {𝐷})) |
| 78 | 77 | eqeq2d 2748 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1o × {𝑥}) = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)) ↔ (1o × {𝑥}) = (1o ×
{𝐷}))) |
| 79 | | fveq1 6905 |
. . . . . . 7
⊢
((1o × {𝑥}) = (1o × {𝐷}) → ((1o
× {𝑥})‘∅)
= ((1o × {𝐷})‘∅)) |
| 80 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 81 | 80 | fvconst2 7224 |
. . . . . . . . 9
⊢ (∅
∈ 1o → ((1o × {𝑥})‘∅) = 𝑥) |
| 82 | 52, 81 | mp1i 13 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1o × {𝑥})‘∅) = 𝑥) |
| 83 | | simpl3 1194 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ 𝐷 ∈
ℕ0) |
| 84 | | fvconst2g 7222 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ℕ0
∧ ∅ ∈ 1o) → ((1o × {𝐷})‘∅) = 𝐷) |
| 85 | 83, 52, 84 | sylancl 586 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1o × {𝐷})‘∅) = 𝐷) |
| 86 | 82, 85 | eqeq12d 2753 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ (((1o × {𝑥})‘∅) = ((1o ×
{𝐷})‘∅) ↔
𝑥 = 𝐷)) |
| 87 | 79, 86 | imbitrid 244 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1o × {𝑥}) = (1o × {𝐷}) → 𝑥 = 𝐷)) |
| 88 | | sneq 4636 |
. . . . . . 7
⊢ (𝑥 = 𝐷 → {𝑥} = {𝐷}) |
| 89 | 88 | xpeq2d 5715 |
. . . . . 6
⊢ (𝑥 = 𝐷 → (1o × {𝑥}) = (1o ×
{𝐷})) |
| 90 | 87, 89 | impbid1 225 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1o × {𝑥}) = (1o × {𝐷}) ↔ 𝑥 = 𝐷)) |
| 91 | 78, 90 | bitrd 279 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ ((1o × {𝑥}) = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)) ↔ 𝑥 = 𝐷)) |
| 92 | 91 | ifbid 4549 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0)
→ if((1o × {𝑥}) = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 ) = if(𝑥 = 𝐷, 𝐶, 0 )) |
| 93 | 92 | mpteq2dva 5242 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) → (𝑥 ∈ ℕ0
↦ if((1o × {𝑥}) = (𝑏 ∈ 1o ↦ if(𝑏 = ∅, 𝐷, 0)), 𝐶, 0 )) = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 𝐷, 𝐶, 0 ))) |
| 94 | 12, 76, 93 | 3eqtrd 2781 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝐷 ∈ ℕ0) →
(coe1‘(𝐶
·
(𝐷 ↑ 𝑋))) = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 𝐷, 𝐶, 0 ))) |