| Step | Hyp | Ref
| Expression |
| 1 | | 0z 12624 |
. . . . 5
⊢ 0 ∈
ℤ |
| 2 | | c0ex 11255 |
. . . . . 6
⊢ 0 ∈
V |
| 3 | 2 | snss 4785 |
. . . . 5
⊢ (0 ∈
ℤ ↔ {0} ⊆ ℤ) |
| 4 | 1, 3 | mpbi 230 |
. . . 4
⊢ {0}
⊆ ℤ |
| 5 | | xpss2 5705 |
. . . 4
⊢ ({0}
⊆ ℤ → (ℤ × {0}) ⊆ (ℤ ×
ℤ)) |
| 6 | 4, 5 | ax-mp 5 |
. . 3
⊢ (ℤ
× {0}) ⊆ (ℤ × ℤ) |
| 7 | | pzriprng.i |
. . 3
⊢ 𝐼 = (ℤ ×
{0}) |
| 8 | | pzriprng.r |
. . . 4
⊢ 𝑅 = (ℤring
×s ℤring) |
| 9 | 8 | pzriprnglem2 21493 |
. . 3
⊢
(Base‘𝑅) =
(ℤ × ℤ) |
| 10 | 6, 7, 9 | 3sstr4i 4035 |
. 2
⊢ 𝐼 ⊆ (Base‘𝑅) |
| 11 | 1 | ne0ii 4344 |
. . . . 5
⊢ ℤ
≠ ∅ |
| 12 | 2 | snnz 4776 |
. . . . 5
⊢ {0} ≠
∅ |
| 13 | 11, 12 | pm3.2i 470 |
. . . 4
⊢ (ℤ
≠ ∅ ∧ {0} ≠ ∅) |
| 14 | | xpnz 6179 |
. . . 4
⊢ ((ℤ
≠ ∅ ∧ {0} ≠ ∅) ↔ (ℤ × {0}) ≠
∅) |
| 15 | 13, 14 | mpbi 230 |
. . 3
⊢ (ℤ
× {0}) ≠ ∅ |
| 16 | 7, 15 | eqnetri 3011 |
. 2
⊢ 𝐼 ≠ ∅ |
| 17 | 8, 7 | pzriprnglem3 21494 |
. . . 4
⊢ (𝑥 ∈ 𝐼 ↔ ∃𝑎 ∈ ℤ 𝑥 = 〈𝑎, 0〉) |
| 18 | 8, 7 | pzriprnglem3 21494 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐼 ↔ ∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 0〉) |
| 19 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) → 𝑥 = 〈𝑎, 0〉) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) ∧ 𝑏 ∈ ℤ) → 𝑥 = 〈𝑎, 0〉) |
| 21 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = 〈𝑏, 0〉 → 𝑦 = 〈𝑏, 0〉) |
| 22 | 20, 21 | oveqan12d 7450 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = 〈𝑏, 0〉) → (𝑥(+g‘𝑅)𝑦) = (〈𝑎, 0〉(+g‘𝑅)〈𝑏, 0〉)) |
| 23 | | zringbas 21464 |
. . . . . . . . . . . . 13
⊢ ℤ =
(Base‘ℤring) |
| 24 | | zringring 21460 |
. . . . . . . . . . . . . 14
⊢
ℤring ∈ Ring |
| 25 | 24 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
ℤring ∈ Ring) |
| 26 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑎 ∈
ℤ) |
| 27 | 1 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 0 ∈
ℤ) |
| 28 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℤ) |
| 29 | | zaddcl 12657 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ) |
| 30 | | 00id 11436 |
. . . . . . . . . . . . . . 15
⊢ (0 + 0) =
0 |
| 31 | 30, 1 | eqeltri 2837 |
. . . . . . . . . . . . . 14
⊢ (0 + 0)
∈ ℤ |
| 32 | 31 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (0 + 0)
∈ ℤ) |
| 33 | | zringplusg 21465 |
. . . . . . . . . . . . 13
⊢ + =
(+g‘ℤring) |
| 34 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 35 | 8, 23, 23, 25, 25, 26, 27, 28, 27, 29, 32, 33, 33, 34 | xpsadd 17619 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
(〈𝑎,
0〉(+g‘𝑅)〈𝑏, 0〉) = 〈(𝑎 + 𝑏), (0 + 0)〉) |
| 36 | 2 | snid 4662 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
{0} |
| 37 | 30, 36 | eqeltri 2837 |
. . . . . . . . . . . . 13
⊢ (0 + 0)
∈ {0} |
| 38 | 7 | eleq2i 2833 |
. . . . . . . . . . . . . 14
⊢
(〈(𝑎 + 𝑏), (0 + 0)〉 ∈ 𝐼 ↔ 〈(𝑎 + 𝑏), (0 + 0)〉 ∈ (ℤ ×
{0})) |
| 39 | | opelxp 5721 |
. . . . . . . . . . . . . 14
⊢
(〈(𝑎 + 𝑏), (0 + 0)〉 ∈ (ℤ
× {0}) ↔ ((𝑎 +
𝑏) ∈ ℤ ∧ (0
+ 0) ∈ {0})) |
| 40 | 38, 39 | bitri 275 |
. . . . . . . . . . . . 13
⊢
(〈(𝑎 + 𝑏), (0 + 0)〉 ∈ 𝐼 ↔ ((𝑎 + 𝑏) ∈ ℤ ∧ (0 + 0) ∈
{0})) |
| 41 | 29, 37, 40 | sylanblrc 590 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
〈(𝑎 + 𝑏), (0 + 0)〉 ∈ 𝐼) |
| 42 | 35, 41 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) →
(〈𝑎,
0〉(+g‘𝑅)〈𝑏, 0〉) ∈ 𝐼) |
| 43 | 42 | ad4ant13 751 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = 〈𝑏, 0〉) → (〈𝑎, 0〉(+g‘𝑅)〈𝑏, 0〉) ∈ 𝐼) |
| 44 | 22, 43 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = 〈𝑏, 0〉) → (𝑥(+g‘𝑅)𝑦) ∈ 𝐼) |
| 45 | 44 | rexlimdva2 3157 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) → (∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 0〉 → (𝑥(+g‘𝑅)𝑦) ∈ 𝐼)) |
| 46 | 18, 45 | biimtrid 242 |
. . . . . . 7
⊢ ((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) → (𝑦 ∈ 𝐼 → (𝑥(+g‘𝑅)𝑦) ∈ 𝐼)) |
| 47 | 46 | ralrimiv 3145 |
. . . . . 6
⊢ ((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) → ∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼) |
| 48 | | zringgrp 21463 |
. . . . . . . . . . 11
⊢
ℤring ∈ Grp |
| 49 | 48 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℤ →
ℤring ∈ Grp) |
| 50 | | id 22 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℤ) |
| 51 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℤ → 0 ∈
ℤ) |
| 52 | | eqid 2737 |
. . . . . . . . . 10
⊢
(invg‘ℤring) =
(invg‘ℤring) |
| 53 | | eqid 2737 |
. . . . . . . . . 10
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 54 | 8, 23, 23, 49, 49, 50, 51, 52, 52, 53 | xpsinv 19078 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℤ →
((invg‘𝑅)‘〈𝑎, 0〉) =
〈((invg‘ℤring)‘𝑎),
((invg‘ℤring)‘0)〉) |
| 55 | | zringinvg 21476 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℤ → -𝑎 =
((invg‘ℤring)‘𝑎)) |
| 56 | | znegcl 12652 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℤ → -𝑎 ∈
ℤ) |
| 57 | 55, 56 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℤ →
((invg‘ℤring)‘𝑎) ∈ ℤ) |
| 58 | | neg0 11555 |
. . . . . . . . . . . 12
⊢ -0 =
0 |
| 59 | 58, 36 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ -0 ∈
{0} |
| 60 | | zringinvg 21476 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ → -0 =
((invg‘ℤring)‘0)) |
| 61 | 60 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℤ → (-0 ∈ {0} ↔
((invg‘ℤring)‘0) ∈
{0})) |
| 62 | 1, 61 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℤ → (-0
∈ {0} ↔ ((invg‘ℤring)‘0)
∈ {0})) |
| 63 | 59, 62 | mpbii 233 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℤ →
((invg‘ℤring)‘0) ∈
{0}) |
| 64 | 57, 63 | opelxpd 5724 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℤ →
〈((invg‘ℤring)‘𝑎),
((invg‘ℤring)‘0)〉 ∈ (ℤ
× {0})) |
| 65 | 54, 64 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ →
((invg‘𝑅)‘〈𝑎, 0〉) ∈ (ℤ ×
{0})) |
| 66 | 65 | adantr 480 |
. . . . . . 7
⊢ ((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) →
((invg‘𝑅)‘〈𝑎, 0〉) ∈ (ℤ ×
{0})) |
| 67 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑎, 0〉 →
((invg‘𝑅)‘𝑥) = ((invg‘𝑅)‘〈𝑎, 0〉)) |
| 68 | 67 | adantl 481 |
. . . . . . 7
⊢ ((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) →
((invg‘𝑅)‘𝑥) = ((invg‘𝑅)‘〈𝑎, 0〉)) |
| 69 | 7 | a1i 11 |
. . . . . . 7
⊢ ((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) → 𝐼 = (ℤ × {0})) |
| 70 | 66, 68, 69 | 3eltr4d 2856 |
. . . . . 6
⊢ ((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) →
((invg‘𝑅)‘𝑥) ∈ 𝐼) |
| 71 | 47, 70 | jca 511 |
. . . . 5
⊢ ((𝑎 ∈ ℤ ∧ 𝑥 = 〈𝑎, 0〉) → (∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐼)) |
| 72 | 71 | rexlimiva 3147 |
. . . 4
⊢
(∃𝑎 ∈
ℤ 𝑥 = 〈𝑎, 0〉 → (∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐼)) |
| 73 | 17, 72 | sylbi 217 |
. . 3
⊢ (𝑥 ∈ 𝐼 → (∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐼)) |
| 74 | 73 | rgen 3063 |
. 2
⊢
∀𝑥 ∈
𝐼 (∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐼) |
| 75 | 8 | pzriprnglem1 21492 |
. . . 4
⊢ 𝑅 ∈ Rng |
| 76 | | rnggrp 20155 |
. . . 4
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) |
| 77 | 75, 76 | ax-mp 5 |
. . 3
⊢ 𝑅 ∈ Grp |
| 78 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 79 | 78, 34, 53 | issubg2 19159 |
. . 3
⊢ (𝑅 ∈ Grp → (𝐼 ∈ (SubGrp‘𝑅) ↔ (𝐼 ⊆ (Base‘𝑅) ∧ 𝐼 ≠ ∅ ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐼)))) |
| 80 | 77, 79 | ax-mp 5 |
. 2
⊢ (𝐼 ∈ (SubGrp‘𝑅) ↔ (𝐼 ⊆ (Base‘𝑅) ∧ 𝐼 ≠ ∅ ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥(+g‘𝑅)𝑦) ∈ 𝐼 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝐼))) |
| 81 | 10, 16, 74, 80 | mpbir3an 1342 |
1
⊢ 𝐼 ∈ (SubGrp‘𝑅) |