| Step | Hyp | Ref
| Expression |
| 1 | | pzriprng.r |
. . 3
⊢ 𝑅 = (ℤring
×s ℤring) |
| 2 | | pzriprng.i |
. . 3
⊢ 𝐼 = (ℤ ×
{0}) |
| 3 | 1, 2 | pzriprnglem4 21495 |
. 2
⊢ 𝐼 ∈ (SubGrp‘𝑅) |
| 4 | 1, 2 | pzriprnglem3 21494 |
. . . 4
⊢ (𝑥 ∈ 𝐼 ↔ ∃𝑎 ∈ ℤ 𝑥 = 〈𝑎, 0〉) |
| 5 | 1, 2 | pzriprnglem3 21494 |
. . . 4
⊢ (𝑦 ∈ 𝐼 ↔ ∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 0〉) |
| 6 | | zringbas 21464 |
. . . . . . . . . . . . 13
⊢ ℤ =
(Base‘ℤring) |
| 7 | | zringring 21460 |
. . . . . . . . . . . . . 14
⊢
ℤring ∈ Ring |
| 8 | 7 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
ℤring ∈ Ring) |
| 9 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑎 ∈
ℤ) |
| 10 | | 0zd 12625 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 0 ∈
ℤ) |
| 11 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℤ) |
| 12 | | zringmulr 21468 |
. . . . . . . . . . . . . . . 16
⊢ ·
= (.r‘ℤring) |
| 13 | 12 | eqcomi 2746 |
. . . . . . . . . . . . . . 15
⊢
(.r‘ℤring) = · |
| 14 | 13 | oveqi 7444 |
. . . . . . . . . . . . . 14
⊢ (𝑎(.r‘ℤring)𝑏) = (𝑎 · 𝑏) |
| 15 | | zmulcl 12666 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 · 𝑏) ∈ ℤ) |
| 16 | 14, 15 | eqeltrid 2845 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎(.r‘ℤring)𝑏) ∈ ℤ) |
| 17 | 13 | oveqi 7444 |
. . . . . . . . . . . . . . . 16
⊢
(0(.r‘ℤring)0) = (0 ·
0) |
| 18 | | 0cn 11253 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℂ |
| 19 | 18 | mul02i 11450 |
. . . . . . . . . . . . . . . 16
⊢ (0
· 0) = 0 |
| 20 | 17, 19 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢
(0(.r‘ℤring)0) = 0 |
| 21 | | 0z 12624 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ |
| 22 | 20, 21 | eqeltri 2837 |
. . . . . . . . . . . . . 14
⊢
(0(.r‘ℤring)0) ∈
ℤ |
| 23 | 22 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
(0(.r‘ℤring)0) ∈
ℤ) |
| 24 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(.r‘ℤring) =
(.r‘ℤring) |
| 25 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 26 | 1, 6, 6, 8, 8, 9, 10, 11, 10, 16, 23, 24, 24, 25 | xpsmul 17620 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
(〈𝑎,
0〉(.r‘𝑅)〈𝑏, 0〉) = 〈(𝑎(.r‘ℤring)𝑏),
(0(.r‘ℤring)0)〉) |
| 27 | | c0ex 11255 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
V |
| 28 | 27 | snid 4662 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
{0} |
| 29 | 28 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 0 ∈
{0}) |
| 30 | 20, 29 | eqeltrid 2845 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
(0(.r‘ℤring)0) ∈ {0}) |
| 31 | 16, 30 | opelxpd 5724 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
〈(𝑎(.r‘ℤring)𝑏),
(0(.r‘ℤring)0)〉 ∈ (ℤ ×
{0})) |
| 32 | 26, 31 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
(〈𝑎,
0〉(.r‘𝑅)〈𝑏, 0〉) ∈ (ℤ ×
{0})) |
| 33 | 32 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑦 = 〈𝑏, 0〉 ∧ 𝑥 = 〈𝑎, 0〉)) → (〈𝑎, 0〉(.r‘𝑅)〈𝑏, 0〉) ∈ (ℤ ×
{0})) |
| 34 | | oveq12 7440 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 〈𝑎, 0〉 ∧ 𝑦 = 〈𝑏, 0〉) → (𝑥(.r‘𝑅)𝑦) = (〈𝑎, 0〉(.r‘𝑅)〈𝑏, 0〉)) |
| 35 | 34 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑦 = 〈𝑏, 0〉 ∧ 𝑥 = 〈𝑎, 0〉) → (𝑥(.r‘𝑅)𝑦) = (〈𝑎, 0〉(.r‘𝑅)〈𝑏, 0〉)) |
| 36 | 35 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑦 = 〈𝑏, 0〉 ∧ 𝑥 = 〈𝑎, 0〉)) → (𝑥(.r‘𝑅)𝑦) = (〈𝑎, 0〉(.r‘𝑅)〈𝑏, 0〉)) |
| 37 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑦 = 〈𝑏, 0〉 ∧ 𝑥 = 〈𝑎, 0〉)) → 𝐼 = (ℤ × {0})) |
| 38 | 33, 36, 37 | 3eltr4d 2856 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (𝑦 = 〈𝑏, 0〉 ∧ 𝑥 = 〈𝑎, 0〉)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) |
| 39 | 38 | exp32 420 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑦 = 〈𝑏, 0〉 → (𝑥 = 〈𝑎, 0〉 → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼))) |
| 40 | 39 | rexlimdva 3155 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
(∃𝑏 ∈ ℤ
𝑦 = 〈𝑏, 0〉 → (𝑥 = 〈𝑎, 0〉 → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼))) |
| 41 | 40 | com23 86 |
. . . . . 6
⊢ (𝑎 ∈ ℤ → (𝑥 = 〈𝑎, 0〉 → (∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 0〉 → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼))) |
| 42 | 41 | rexlimiv 3148 |
. . . . 5
⊢
(∃𝑎 ∈
ℤ 𝑥 = 〈𝑎, 0〉 → (∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 0〉 → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼)) |
| 43 | 42 | imp 406 |
. . . 4
⊢
((∃𝑎 ∈
ℤ 𝑥 = 〈𝑎, 0〉 ∧ ∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 0〉) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) |
| 44 | 4, 5, 43 | syl2anb 598 |
. . 3
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐼) |
| 45 | 44 | rgen2 3199 |
. 2
⊢
∀𝑥 ∈
𝐼 ∀𝑦 ∈ 𝐼 (𝑥(.r‘𝑅)𝑦) ∈ 𝐼 |
| 46 | 1 | pzriprnglem1 21492 |
. . 3
⊢ 𝑅 ∈ Rng |
| 47 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 48 | 47, 25 | issubrng2 20558 |
. . 3
⊢ (𝑅 ∈ Rng → (𝐼 ∈ (SubRng‘𝑅) ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 (𝑥(.r‘𝑅)𝑦) ∈ 𝐼))) |
| 49 | 46, 48 | ax-mp 5 |
. 2
⊢ (𝐼 ∈ (SubRng‘𝑅) ↔ (𝐼 ∈ (SubGrp‘𝑅) ∧ ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 (𝑥(.r‘𝑅)𝑦) ∈ 𝐼)) |
| 50 | 3, 45, 49 | mpbir2an 711 |
1
⊢ 𝐼 ∈ (SubRng‘𝑅) |