| Step | Hyp | Ref
| Expression |
| 1 | | rng2idlring.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Rng) |
| 2 | | rng2idlring.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) |
| 3 | | rng2idlring.j |
. . . . . . . . . . . 12
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
| 4 | | rng2idlring.u |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ Ring) |
| 5 | | ringrng 20282 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ Ring → 𝐽 ∈ Rng) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ Rng) |
| 7 | 3, 6 | eqeltrrid 2846 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng) |
| 8 | 1, 2, 7 | rng2idlnsg 21276 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) |
| 9 | | nsgsubg 19176 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) → 𝐼 ∈ (SubGrp‘𝑅)) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅)) |
| 11 | | rngqiprngim.q |
. . . . . . . . . . 11
⊢ 𝑄 = (𝑅 /s ∼ ) |
| 12 | | rngqiprngim.g |
. . . . . . . . . . . 12
⊢ ∼ =
(𝑅 ~QG
𝐼) |
| 13 | 12 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ (𝑅 /s ∼ ) =
(𝑅 /s
(𝑅 ~QG
𝐼)) |
| 14 | 11, 13 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) |
| 15 | | eqid 2737 |
. . . . . . . . . 10
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) |
| 16 | 14, 15 | qus2idrng 21283 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Rng ∧ 𝐼 ∈ (2Ideal‘𝑅) ∧ 𝐼 ∈ (SubGrp‘𝑅)) → 𝑄 ∈ Rng) |
| 17 | 1, 2, 10, 16 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ Rng) |
| 18 | | rnggrp 20155 |
. . . . . . . . 9
⊢ (𝑄 ∈ Rng → 𝑄 ∈ Grp) |
| 19 | 18 | grpmndd 18964 |
. . . . . . . 8
⊢ (𝑄 ∈ Rng → 𝑄 ∈ Mnd) |
| 20 | 17, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ Mnd) |
| 21 | | ringmnd 20240 |
. . . . . . . 8
⊢ (𝐽 ∈ Ring → 𝐽 ∈ Mnd) |
| 22 | 4, 21 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Mnd) |
| 23 | | rngqiprngim.p |
. . . . . . . 8
⊢ 𝑃 = (𝑄 ×s 𝐽) |
| 24 | 23 | xpsmnd0 18791 |
. . . . . . 7
⊢ ((𝑄 ∈ Mnd ∧ 𝐽 ∈ Mnd) →
(0g‘𝑃) =
〈(0g‘𝑄), (0g‘𝐽)〉) |
| 25 | 20, 22, 24 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑃) =
〈(0g‘𝑄), (0g‘𝐽)〉) |
| 26 | 25 | sneqd 4638 |
. . . . 5
⊢ (𝜑 →
{(0g‘𝑃)} =
{〈(0g‘𝑄), (0g‘𝐽)〉}) |
| 27 | 26 | imaeq2d 6078 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ {(0g‘𝑃)}) = (◡𝐹 “ {〈(0g‘𝑄), (0g‘𝐽)〉})) |
| 28 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
| 29 | | opex 5469 |
. . . . . . 7
⊢
〈[𝑥] ∼ , (
1 · 𝑥)〉 ∈
V |
| 30 | 29 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 〈[𝑥] ∼ , ( 1 · 𝑥)〉 ∈
V) |
| 31 | | rngqiprngim.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ 〈[𝑥] ∼ , ( 1 · 𝑥)〉) |
| 32 | 28, 30, 31 | fnmptd 6709 |
. . . . 5
⊢ (𝜑 → 𝐹 Fn 𝐵) |
| 33 | | fncnvima2 7081 |
. . . . 5
⊢ (𝐹 Fn 𝐵 → (◡𝐹 “ {〈(0g‘𝑄), (0g‘𝐽)〉}) = {𝑎 ∈ 𝐵 ∣ (𝐹‘𝑎) ∈ {〈(0g‘𝑄), (0g‘𝐽)〉}}) |
| 34 | 32, 33 | syl 17 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ {〈(0g‘𝑄), (0g‘𝐽)〉}) = {𝑎 ∈ 𝐵 ∣ (𝐹‘𝑎) ∈ {〈(0g‘𝑄), (0g‘𝐽)〉}}) |
| 35 | | rng2idlring.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
| 36 | | rng2idlring.t |
. . . . . . . 8
⊢ · =
(.r‘𝑅) |
| 37 | | rng2idlring.1 |
. . . . . . . 8
⊢ 1 =
(1r‘𝐽) |
| 38 | | rngqiprngim.c |
. . . . . . . 8
⊢ 𝐶 = (Base‘𝑄) |
| 39 | 1, 2, 3, 4, 35, 36, 37, 12, 11, 38, 23, 31 | rngqiprngimfv 21308 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) = 〈[𝑎] ∼ , ( 1 · 𝑎)〉) |
| 40 | 39 | eleq1d 2826 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝐹‘𝑎) ∈ {〈(0g‘𝑄), (0g‘𝐽)〉} ↔ 〈[𝑎] ∼ , ( 1 · 𝑎)〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉})) |
| 41 | 40 | rabbidva 3443 |
. . . . 5
⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ (𝐹‘𝑎) ∈ {〈(0g‘𝑄), (0g‘𝐽)〉}} = {𝑎 ∈ 𝐵 ∣ 〈[𝑎] ∼ , ( 1 · 𝑎)〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉}}) |
| 42 | | eceq1 8784 |
. . . . . . . 8
⊢ (𝑎 = (0g‘𝑅) → [𝑎] ∼ =
[(0g‘𝑅)]
∼
) |
| 43 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑎 = (0g‘𝑅) → ( 1 · 𝑎) = ( 1 ·
(0g‘𝑅))) |
| 44 | 42, 43 | opeq12d 4881 |
. . . . . . 7
⊢ (𝑎 = (0g‘𝑅) → 〈[𝑎] ∼ , ( 1 · 𝑎)〉 =
〈[(0g‘𝑅)] ∼ , ( 1 ·
(0g‘𝑅))〉) |
| 45 | 44 | eleq1d 2826 |
. . . . . 6
⊢ (𝑎 = (0g‘𝑅) → (〈[𝑎] ∼ , ( 1 · 𝑎)〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉} ↔
〈[(0g‘𝑅)] ∼ , ( 1 ·
(0g‘𝑅))〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉})) |
| 46 | | rnggrp 20155 |
. . . . . . . . 9
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) |
| 47 | 1, 46 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 48 | 47 | grpmndd 18964 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Mnd) |
| 49 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 50 | 35, 49 | mndidcl 18762 |
. . . . . . 7
⊢ (𝑅 ∈ Mnd →
(0g‘𝑅)
∈ 𝐵) |
| 51 | 48, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑅) ∈ 𝐵) |
| 52 | 12 | eceq2i 8787 |
. . . . . . . . 9
⊢
[(0g‘𝑅)] ∼ =
[(0g‘𝑅)](𝑅 ~QG 𝐼) |
| 53 | 14, 49 | qus0 19207 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
| 54 | 8, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
| 55 | 52, 54 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝜑 →
[(0g‘𝑅)]
∼
= (0g‘𝑄)) |
| 56 | 1, 2, 7 | rng2idl0 21277 |
. . . . . . . . . . 11
⊢ (𝜑 → (0g‘𝑅) ∈ 𝐼) |
| 57 | 35, 15 | 2idlss 21272 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ (2Ideal‘𝑅) → 𝐼 ⊆ 𝐵) |
| 58 | 2, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ⊆ 𝐵) |
| 59 | 3, 35, 49 | ress0g 18775 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Mnd ∧
(0g‘𝑅)
∈ 𝐼 ∧ 𝐼 ⊆ 𝐵) → (0g‘𝑅) = (0g‘𝐽)) |
| 60 | 48, 56, 58, 59 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑅) = (0g‘𝐽)) |
| 61 | 60 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → ( 1 ·
(0g‘𝑅)) =
( 1 ·
(0g‘𝐽))) |
| 62 | 3, 36 | ressmulr 17351 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (2Ideal‘𝑅) → · =
(.r‘𝐽)) |
| 63 | 2, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → · =
(.r‘𝐽)) |
| 64 | 63 | oveqd 7448 |
. . . . . . . . 9
⊢ (𝜑 → ( 1 ·
(0g‘𝐽)) =
( 1
(.r‘𝐽)(0g‘𝐽))) |
| 65 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐽) =
(Base‘𝐽) |
| 66 | 65, 37 | ringidcl 20262 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Ring → 1 ∈
(Base‘𝐽)) |
| 67 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(.r‘𝐽) = (.r‘𝐽) |
| 68 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝐽) = (0g‘𝐽) |
| 69 | 65, 67, 68 | ringrz 20291 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Ring ∧ 1 ∈
(Base‘𝐽)) → (
1
(.r‘𝐽)(0g‘𝐽)) = (0g‘𝐽)) |
| 70 | 4, 66, 69 | syl2anc2 585 |
. . . . . . . . 9
⊢ (𝜑 → ( 1 (.r‘𝐽)(0g‘𝐽)) = (0g‘𝐽)) |
| 71 | 61, 64, 70 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 → ( 1 ·
(0g‘𝑅)) =
(0g‘𝐽)) |
| 72 | 55, 71 | opeq12d 4881 |
. . . . . . 7
⊢ (𝜑 →
〈[(0g‘𝑅)] ∼ , ( 1 ·
(0g‘𝑅))〉 = 〈(0g‘𝑄), (0g‘𝐽)〉) |
| 73 | | opex 5469 |
. . . . . . . 8
⊢
〈[(0g‘𝑅)] ∼ , ( 1 ·
(0g‘𝑅))〉 ∈ V |
| 74 | 73 | elsn 4641 |
. . . . . . 7
⊢
(〈[(0g‘𝑅)] ∼ , ( 1 ·
(0g‘𝑅))〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉} ↔
〈[(0g‘𝑅)] ∼ , ( 1 ·
(0g‘𝑅))〉 = 〈(0g‘𝑄), (0g‘𝐽)〉) |
| 75 | 72, 74 | sylibr 234 |
. . . . . 6
⊢ (𝜑 →
〈[(0g‘𝑅)] ∼ , ( 1 ·
(0g‘𝑅))〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉}) |
| 76 | | opex 5469 |
. . . . . . . . . 10
⊢
〈[𝑎] ∼ , (
1 · 𝑎)〉 ∈
V |
| 77 | 76 | elsn 4641 |
. . . . . . . . 9
⊢
(〈[𝑎] ∼ , (
1 · 𝑎)〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉} ↔ 〈[𝑎] ∼ , ( 1 · 𝑎)〉 =
〈(0g‘𝑄), (0g‘𝐽)〉) |
| 78 | 12 | ovexi 7465 |
. . . . . . . . . . 11
⊢ ∼ ∈
V |
| 79 | | ecexg 8749 |
. . . . . . . . . . 11
⊢ ( ∼ ∈
V → [𝑎] ∼ ∈
V) |
| 80 | 78, 79 | ax-mp 5 |
. . . . . . . . . 10
⊢ [𝑎] ∼ ∈
V |
| 81 | | ovex 7464 |
. . . . . . . . . 10
⊢ ( 1 · 𝑎) ∈ V |
| 82 | 80, 81 | opth 5481 |
. . . . . . . . 9
⊢
(〈[𝑎] ∼ , (
1 · 𝑎)〉 =
〈(0g‘𝑄), (0g‘𝐽)〉 ↔ ([𝑎] ∼ =
(0g‘𝑄)
∧ ( 1
·
𝑎) =
(0g‘𝐽))) |
| 83 | 77, 82 | bitri 275 |
. . . . . . . 8
⊢
(〈[𝑎] ∼ , (
1 · 𝑎)〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉} ↔ ([𝑎] ∼ =
(0g‘𝑄)
∧ ( 1
·
𝑎) =
(0g‘𝐽))) |
| 84 | 1, 2, 3, 4, 35, 36, 37, 12, 11 | rngqiprngimf1lem 21304 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (([𝑎] ∼ =
(0g‘𝑄)
∧ ( 1
·
𝑎) =
(0g‘𝐽))
→ 𝑎 =
(0g‘𝑅))) |
| 85 | 83, 84 | biimtrid 242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (〈[𝑎] ∼ , ( 1 · 𝑎)〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉} → 𝑎 = (0g‘𝑅))) |
| 86 | 85 | imp 406 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 〈[𝑎] ∼ , ( 1 · 𝑎)〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉}) → 𝑎 = (0g‘𝑅)) |
| 87 | 45, 51, 75, 86 | rabeqsnd 4669 |
. . . . 5
⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ 〈[𝑎] ∼ , ( 1 · 𝑎)〉 ∈
{〈(0g‘𝑄), (0g‘𝐽)〉}} = {(0g‘𝑅)}) |
| 88 | 41, 87 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ (𝐹‘𝑎) ∈ {〈(0g‘𝑄), (0g‘𝐽)〉}} =
{(0g‘𝑅)}) |
| 89 | 27, 34, 88 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (◡𝐹 “ {(0g‘𝑃)}) =
{(0g‘𝑅)}) |
| 90 | 1, 2, 3, 4, 35, 36, 37, 12, 11, 38, 23, 31 | rngqiprngghm 21309 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑃)) |
| 91 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 92 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝑃) = (0g‘𝑃) |
| 93 | 35, 91, 49, 92 | kerf1ghm 19265 |
. . . 4
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑃) → (𝐹:𝐵–1-1→(Base‘𝑃) ↔ (◡𝐹 “ {(0g‘𝑃)}) =
{(0g‘𝑅)})) |
| 94 | 90, 93 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹:𝐵–1-1→(Base‘𝑃) ↔ (◡𝐹 “ {(0g‘𝑃)}) =
{(0g‘𝑅)})) |
| 95 | 89, 94 | mpbird 257 |
. 2
⊢ (𝜑 → 𝐹:𝐵–1-1→(Base‘𝑃)) |
| 96 | | eqidd 2738 |
. . 3
⊢ (𝜑 → 𝐹 = 𝐹) |
| 97 | | eqidd 2738 |
. . 3
⊢ (𝜑 → 𝐵 = 𝐵) |
| 98 | 1, 2, 3, 4, 35, 36, 37, 12, 11, 38, 23 | rngqipbas 21305 |
. . 3
⊢ (𝜑 → (Base‘𝑃) = (𝐶 × 𝐼)) |
| 99 | 96, 97, 98 | f1eq123d 6840 |
. 2
⊢ (𝜑 → (𝐹:𝐵–1-1→(Base‘𝑃) ↔ 𝐹:𝐵–1-1→(𝐶 × 𝐼))) |
| 100 | 95, 99 | mpbid 232 |
1
⊢ (𝜑 → 𝐹:𝐵–1-1→(𝐶 × 𝐼)) |