Proof of Theorem rngqiprngimf1lem
Step | Hyp | Ref
| Expression |
1 | | rng2idlring.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Rng) |
2 | | rng2idlring.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) |
3 | | rng2idlring.j |
. . . . . . . . . 10
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
4 | | rng2idlring.u |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ Ring) |
5 | | ringrng 20203 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ Ring → 𝐽 ∈ Rng) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ Rng) |
7 | 3, 6 | eqeltrrid 2833 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng) |
8 | 1, 2, 7 | rng2idlnsg 21142 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → 𝐼 ∈ (NrmSGrp‘𝑅)) |
10 | | rngqiprngim.q |
. . . . . . . . 9
⊢ 𝑄 = (𝑅 /s ∼ ) |
11 | | rngqiprngim.g |
. . . . . . . . . 10
⊢ ∼ =
(𝑅 ~QG
𝐼) |
12 | 11 | oveq2i 7425 |
. . . . . . . . 9
⊢ (𝑅 /s ∼ ) =
(𝑅 /s
(𝑅 ~QG
𝐼)) |
13 | 10, 12 | eqtri 2755 |
. . . . . . . 8
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) |
14 | | eqid 2727 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
15 | 13, 14 | qus0 19128 |
. . . . . . 7
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) →
[(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
16 | 9, 15 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → [(0g‘𝑅)](𝑅 ~QG 𝐼) = (0g‘𝑄)) |
17 | 16 | eqcomd 2733 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → (0g‘𝑄) = [(0g‘𝑅)](𝑅 ~QG 𝐼)) |
18 | 17 | eqeq2d 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ([𝐴] ∼ =
(0g‘𝑄)
↔ [𝐴] ∼ =
[(0g‘𝑅)](𝑅 ~QG 𝐼))) |
19 | 11 | eqcomi 2736 |
. . . . . . 7
⊢ (𝑅 ~QG 𝐼) = ∼ |
20 | 19 | eceq2i 8757 |
. . . . . 6
⊢
[(0g‘𝑅)](𝑅 ~QG 𝐼) = [(0g‘𝑅)] ∼ |
21 | 20 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → [(0g‘𝑅)](𝑅 ~QG 𝐼) = [(0g‘𝑅)] ∼ ) |
22 | 21 | eqeq2d 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ([𝐴] ∼ =
[(0g‘𝑅)](𝑅 ~QG 𝐼) ↔ [𝐴] ∼ =
[(0g‘𝑅)]
∼
)) |
23 | | eqcom 2734 |
. . . . 5
⊢ ([𝐴] ∼ =
[(0g‘𝑅)]
∼
↔ [(0g‘𝑅)] ∼ = [𝐴] ∼ ) |
24 | | rngabl 20079 |
. . . . . . . 8
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel) |
25 | 1, 24 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Abel) |
26 | | nsgsubg 19097 |
. . . . . . . 8
⊢ (𝐼 ∈ (NrmSGrp‘𝑅) → 𝐼 ∈ (SubGrp‘𝑅)) |
27 | 8, 26 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ (SubGrp‘𝑅)) |
28 | 25, 27 | jca 511 |
. . . . . 6
⊢ (𝜑 → (𝑅 ∈ Abel ∧ 𝐼 ∈ (SubGrp‘𝑅))) |
29 | | rng2idlring.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
30 | 29, 14 | rng0cl 20087 |
. . . . . . . 8
⊢ (𝑅 ∈ Rng →
(0g‘𝑅)
∈ 𝐵) |
31 | 1, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝑅) ∈ 𝐵) |
32 | 31 | anim1i 614 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ((0g‘𝑅) ∈ 𝐵 ∧ 𝐴 ∈ 𝐵)) |
33 | | eqid 2727 |
. . . . . . 7
⊢
(-g‘𝑅) = (-g‘𝑅) |
34 | 29, 33, 11 | qusecsub 19774 |
. . . . . 6
⊢ (((𝑅 ∈ Abel ∧ 𝐼 ∈ (SubGrp‘𝑅)) ∧
((0g‘𝑅)
∈ 𝐵 ∧ 𝐴 ∈ 𝐵)) → ([(0g‘𝑅)] ∼ = [𝐴] ∼ ↔ (𝐴(-g‘𝑅)(0g‘𝑅)) ∈ 𝐼)) |
35 | 28, 32, 34 | syl2an2r 684 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ([(0g‘𝑅)] ∼ = [𝐴] ∼ ↔ (𝐴(-g‘𝑅)(0g‘𝑅)) ∈ 𝐼)) |
36 | 23, 35 | bitrid 283 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ([𝐴] ∼ =
[(0g‘𝑅)]
∼
↔ (𝐴(-g‘𝑅)(0g‘𝑅)) ∈ 𝐼)) |
37 | 18, 22, 36 | 3bitrd 305 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ([𝐴] ∼ =
(0g‘𝑄)
↔ (𝐴(-g‘𝑅)(0g‘𝑅)) ∈ 𝐼)) |
38 | | rnggrp 20082 |
. . . . . . 7
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) |
39 | 1, 38 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Grp) |
40 | 29, 14, 33 | grpsubid1 18965 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝐴 ∈ 𝐵) → (𝐴(-g‘𝑅)(0g‘𝑅)) = 𝐴) |
41 | 39, 40 | sylan 579 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → (𝐴(-g‘𝑅)(0g‘𝑅)) = 𝐴) |
42 | 41 | eleq1d 2813 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ((𝐴(-g‘𝑅)(0g‘𝑅)) ∈ 𝐼 ↔ 𝐴 ∈ 𝐼)) |
43 | | eqid 2727 |
. . . . . . . . 9
⊢
(Base‘𝐽) =
(Base‘𝐽) |
44 | | eqid 2727 |
. . . . . . . . 9
⊢
(0g‘𝐽) = (0g‘𝐽) |
45 | | eqid 2727 |
. . . . . . . . 9
⊢
(.r‘𝐽) = (.r‘𝐽) |
46 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ (Base‘𝐽)) → 𝐽 ∈ Ring) |
47 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ (Base‘𝐽)) → 𝐴 ∈ (Base‘𝐽)) |
48 | | eqid 2727 |
. . . . . . . . 9
⊢
(1r‘𝐽) = (1r‘𝐽) |
49 | 43, 44, 45, 46, 47, 48 | ring1nzdiv 20320 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ (Base‘𝐽)) → (((1r‘𝐽)(.r‘𝐽)𝐴) = (0g‘𝐽) ↔ 𝐴 = (0g‘𝐽))) |
50 | 49 | biimpd 228 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ (Base‘𝐽)) → (((1r‘𝐽)(.r‘𝐽)𝐴) = (0g‘𝐽) → 𝐴 = (0g‘𝐽))) |
51 | 50 | ex 412 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ (Base‘𝐽) → (((1r‘𝐽)(.r‘𝐽)𝐴) = (0g‘𝐽) → 𝐴 = (0g‘𝐽)))) |
52 | 2, 3, 43 | 2idlbas 21139 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐽) = 𝐼) |
53 | 52 | eqcomd 2733 |
. . . . . . 7
⊢ (𝜑 → 𝐼 = (Base‘𝐽)) |
54 | 53 | eleq2d 2814 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ (Base‘𝐽))) |
55 | | rng2idlring.t |
. . . . . . . . . . 11
⊢ · =
(.r‘𝑅) |
56 | 3, 55 | ressmulr 17273 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (2Ideal‘𝑅) → · =
(.r‘𝐽)) |
57 | 2, 56 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → · =
(.r‘𝐽)) |
58 | | rng2idlring.1 |
. . . . . . . . . 10
⊢ 1 =
(1r‘𝐽) |
59 | 58 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 =
(1r‘𝐽)) |
60 | | eqidd 2728 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = 𝐴) |
61 | 57, 59, 60 | oveq123d 7435 |
. . . . . . . 8
⊢ (𝜑 → ( 1 · 𝐴) = ((1r‘𝐽)(.r‘𝐽)𝐴)) |
62 | 61 | eqeq1d 2729 |
. . . . . . 7
⊢ (𝜑 → (( 1 · 𝐴) = (0g‘𝐽) ↔ ((1r‘𝐽)(.r‘𝐽)𝐴) = (0g‘𝐽))) |
63 | 3, 14 | subg0 19071 |
. . . . . . . . 9
⊢ (𝐼 ∈ (SubGrp‘𝑅) →
(0g‘𝑅) =
(0g‘𝐽)) |
64 | 27, 63 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) = (0g‘𝐽)) |
65 | 64 | eqeq2d 2738 |
. . . . . . 7
⊢ (𝜑 → (𝐴 = (0g‘𝑅) ↔ 𝐴 = (0g‘𝐽))) |
66 | 62, 65 | imbi12d 344 |
. . . . . 6
⊢ (𝜑 → ((( 1 · 𝐴) = (0g‘𝐽) → 𝐴 = (0g‘𝑅)) ↔ (((1r‘𝐽)(.r‘𝐽)𝐴) = (0g‘𝐽) → 𝐴 = (0g‘𝐽)))) |
67 | 51, 54, 66 | 3imtr4d 294 |
. . . . 5
⊢ (𝜑 → (𝐴 ∈ 𝐼 → (( 1 · 𝐴) = (0g‘𝐽) → 𝐴 = (0g‘𝑅)))) |
68 | 67 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ 𝐼 → (( 1 · 𝐴) = (0g‘𝐽) → 𝐴 = (0g‘𝑅)))) |
69 | 42, 68 | sylbid 239 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ((𝐴(-g‘𝑅)(0g‘𝑅)) ∈ 𝐼 → (( 1 · 𝐴) = (0g‘𝐽) → 𝐴 = (0g‘𝑅)))) |
70 | 37, 69 | sylbid 239 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → ([𝐴] ∼ =
(0g‘𝑄)
→ (( 1 · 𝐴) = (0g‘𝐽) → 𝐴 = (0g‘𝑅)))) |
71 | 70 | impd 410 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → (([𝐴] ∼ =
(0g‘𝑄)
∧ ( 1
·
𝐴) =
(0g‘𝐽))
→ 𝐴 =
(0g‘𝑅))) |