Step | Hyp | Ref
| Expression |
1 | | ply1domn.p |
. . 3
⊢ 𝑃 = (Poly1‘𝑅) |
2 | 1 | ply1nz 23685 |
. 2
⊢ (𝑅 ∈ NzRing → 𝑃 ∈ NzRing) |
3 | | simpl 472 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) → 𝑅 ∈ Ring) |
4 | | eqid 2610 |
. . . . . . 7
⊢
(1r‘𝑃) = (1r‘𝑃) |
5 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑃) = (0g‘𝑃) |
6 | 4, 5 | nzrnz 19081 |
. . . . . 6
⊢ (𝑃 ∈ NzRing →
(1r‘𝑃)
≠ (0g‘𝑃)) |
7 | 6 | adantl 481 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) →
(1r‘𝑃)
≠ (0g‘𝑃)) |
8 | | ifeq1 4040 |
. . . . . . . . 9
⊢
((1r‘𝑅) = (0g‘𝑅) → if(𝑦 = (1𝑜 × {0}),
(1r‘𝑅),
(0g‘𝑅)) =
if(𝑦 =
(1𝑜 × {0}), (0g‘𝑅), (0g‘𝑅))) |
9 | | ifid 4075 |
. . . . . . . . 9
⊢ if(𝑦 = (1𝑜
× {0}), (0g‘𝑅), (0g‘𝑅)) = (0g‘𝑅) |
10 | 8, 9 | syl6eq 2660 |
. . . . . . . 8
⊢
((1r‘𝑅) = (0g‘𝑅) → if(𝑦 = (1𝑜 × {0}),
(1r‘𝑅),
(0g‘𝑅)) =
(0g‘𝑅)) |
11 | 10 | ralrimivw 2950 |
. . . . . . 7
⊢
((1r‘𝑅) = (0g‘𝑅) → ∀𝑦 ∈ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin}if(𝑦 = (1𝑜
× {0}), (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) |
12 | | eqid 2610 |
. . . . . . . . . 10
⊢
(1𝑜 mPoly 𝑅) = (1𝑜 mPoly 𝑅) |
13 | | eqid 2610 |
. . . . . . . . . 10
⊢ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} = {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈
Fin} |
14 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) |
15 | | eqid 2610 |
. . . . . . . . . 10
⊢
(1r‘𝑅) = (1r‘𝑅) |
16 | 12, 1, 4 | ply1mpl1 19448 |
. . . . . . . . . 10
⊢
(1r‘𝑃) =
(1r‘(1𝑜 mPoly 𝑅)) |
17 | | 1on 7454 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ On |
18 | 17 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) →
1𝑜 ∈ On) |
19 | 12, 13, 14, 15, 16, 18, 3 | mpl1 19265 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) →
(1r‘𝑃) =
(𝑦 ∈ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} ↦
if(𝑦 =
(1𝑜 × {0}), (1r‘𝑅), (0g‘𝑅)))) |
20 | 12, 1, 5 | ply1mpl0 19446 |
. . . . . . . . . . 11
⊢
(0g‘𝑃) =
(0g‘(1𝑜 mPoly 𝑅)) |
21 | | ringgrp 18375 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
22 | 3, 21 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) → 𝑅 ∈ Grp) |
23 | 12, 13, 14, 20, 18, 22 | mpl0 19262 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) →
(0g‘𝑃) =
({𝑥 ∈
(ℕ0 ↑𝑚 1𝑜) ∣
(◡𝑥 “ ℕ) ∈ Fin} ×
{(0g‘𝑅)})) |
24 | | fconstmpt 5085 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} ×
{(0g‘𝑅)})
= (𝑦 ∈ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} ↦
(0g‘𝑅)) |
25 | 23, 24 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) →
(0g‘𝑃) =
(𝑦 ∈ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} ↦
(0g‘𝑅))) |
26 | 19, 25 | eqeq12d 2625 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) →
((1r‘𝑃) =
(0g‘𝑃)
↔ (𝑦 ∈ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} ↦
if(𝑦 =
(1𝑜 × {0}), (1r‘𝑅), (0g‘𝑅))) = (𝑦 ∈ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} ↦
(0g‘𝑅)))) |
27 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) ∈ V |
28 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) ∈ V |
29 | 27, 28 | ifex 4106 |
. . . . . . . . . 10
⊢ if(𝑦 = (1𝑜
× {0}), (1r‘𝑅), (0g‘𝑅)) ∈ V |
30 | 29 | rgenw 2908 |
. . . . . . . . 9
⊢
∀𝑦 ∈
{𝑥 ∈
(ℕ0 ↑𝑚 1𝑜) ∣
(◡𝑥 “ ℕ) ∈ Fin}if(𝑦 = (1𝑜
× {0}), (1r‘𝑅), (0g‘𝑅)) ∈ V |
31 | | mpteqb 6207 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
{𝑥 ∈
(ℕ0 ↑𝑚 1𝑜) ∣
(◡𝑥 “ ℕ) ∈ Fin}if(𝑦 = (1𝑜
× {0}), (1r‘𝑅), (0g‘𝑅)) ∈ V → ((𝑦 ∈ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} ↦
if(𝑦 =
(1𝑜 × {0}), (1r‘𝑅), (0g‘𝑅))) = (𝑦 ∈ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} ↦
(0g‘𝑅))
↔ ∀𝑦 ∈
{𝑥 ∈
(ℕ0 ↑𝑚 1𝑜) ∣
(◡𝑥 “ ℕ) ∈ Fin}if(𝑦 = (1𝑜
× {0}), (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅))) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑦 ∈ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} ↦
if(𝑦 =
(1𝑜 × {0}), (1r‘𝑅), (0g‘𝑅))) = (𝑦 ∈ {𝑥 ∈ (ℕ0
↑𝑚 1𝑜) ∣ (◡𝑥 “ ℕ) ∈ Fin} ↦
(0g‘𝑅))
↔ ∀𝑦 ∈
{𝑥 ∈
(ℕ0 ↑𝑚 1𝑜) ∣
(◡𝑥 “ ℕ) ∈ Fin}if(𝑦 = (1𝑜
× {0}), (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) |
33 | 26, 32 | syl6bb 275 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) →
((1r‘𝑃) =
(0g‘𝑃)
↔ ∀𝑦 ∈
{𝑥 ∈
(ℕ0 ↑𝑚 1𝑜) ∣
(◡𝑥 “ ℕ) ∈ Fin}if(𝑦 = (1𝑜
× {0}), (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅))) |
34 | 11, 33 | syl5ibr 235 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) →
((1r‘𝑅) =
(0g‘𝑅)
→ (1r‘𝑃) = (0g‘𝑃))) |
35 | 34 | necon3d 2803 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) →
((1r‘𝑃)
≠ (0g‘𝑃) → (1r‘𝑅) ≠
(0g‘𝑅))) |
36 | 7, 35 | mpd 15 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) →
(1r‘𝑅)
≠ (0g‘𝑅)) |
37 | 15, 14 | isnzr 19080 |
. . . 4
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ (0g‘𝑅))) |
38 | 3, 36, 37 | sylanbrc 695 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing) → 𝑅 ∈ NzRing) |
39 | 38 | ex 449 |
. 2
⊢ (𝑅 ∈ Ring → (𝑃 ∈ NzRing → 𝑅 ∈
NzRing)) |
40 | 2, 39 | impbid2 215 |
1
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ 𝑃 ∈
NzRing)) |