Proof of Theorem rngqiprngimfolem
Step | Hyp | Ref
| Expression |
1 | | rng2idlring.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Rng) |
2 | 1 | 3ad2ant1 1132 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → 𝑅 ∈ Rng) |
3 | | rng2idlring.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) |
4 | | rng2idlring.j |
. . . . 5
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
5 | | rng2idlring.u |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Ring) |
6 | | rng2idlring.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
7 | | rng2idlring.t |
. . . . 5
⊢ · =
(.r‘𝑅) |
8 | | rng2idlring.1 |
. . . . 5
⊢ 1 =
(1r‘𝐽) |
9 | 1, 3, 4, 5, 6, 7, 8 | rngqiprng1elbas 21049 |
. . . 4
⊢ (𝜑 → 1 ∈ 𝐵) |
10 | 9 | 3ad2ant1 1132 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → 1 ∈ 𝐵) |
11 | | rnggrp 20056 |
. . . . . 6
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) |
12 | 1, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Grp) |
13 | 12 | 3ad2ant1 1132 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → 𝑅 ∈ Grp) |
14 | | simp3 1137 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵) |
15 | 6, 7 | rngcl 20062 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵) → ( 1 · 𝐶) ∈ 𝐵) |
16 | 2, 10, 14, 15 | syl3anc 1370 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · 𝐶) ∈ 𝐵) |
17 | | eqid 2731 |
. . . . 5
⊢
(-g‘𝑅) = (-g‘𝑅) |
18 | 6, 17 | grpsubcl 18943 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝐶 ∈ 𝐵 ∧ ( 1 · 𝐶) ∈ 𝐵) → (𝐶(-g‘𝑅)( 1 · 𝐶)) ∈ 𝐵) |
19 | 13, 14, 16, 18 | syl3anc 1370 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → (𝐶(-g‘𝑅)( 1 · 𝐶)) ∈ 𝐵) |
20 | | eqid 2731 |
. . . . . . 7
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) |
21 | 6, 20 | 2idlss 21021 |
. . . . . 6
⊢ (𝐼 ∈ (2Ideal‘𝑅) → 𝐼 ⊆ 𝐵) |
22 | 3, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐼 ⊆ 𝐵) |
23 | 22 | sselda 3982 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ 𝐵) |
24 | 23 | 3adant3 1131 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → 𝐴 ∈ 𝐵) |
25 | | eqid 2731 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
26 | 6, 25, 7 | rngdi 20058 |
. . 3
⊢ ((𝑅 ∈ Rng ∧ ( 1 ∈ 𝐵 ∧ (𝐶(-g‘𝑅)( 1 · 𝐶)) ∈ 𝐵 ∧ 𝐴 ∈ 𝐵)) → ( 1 · ((𝐶(-g‘𝑅)( 1 · 𝐶))(+g‘𝑅)𝐴)) = (( 1 · (𝐶(-g‘𝑅)( 1 · 𝐶)))(+g‘𝑅)( 1 · 𝐴))) |
27 | 2, 10, 19, 24, 26 | syl13anc 1371 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · ((𝐶(-g‘𝑅)( 1 · 𝐶))(+g‘𝑅)𝐴)) = (( 1 · (𝐶(-g‘𝑅)( 1 · 𝐶)))(+g‘𝑅)( 1 · 𝐴))) |
28 | 6, 7, 17, 2, 10, 14, 16 | rngsubdi 20069 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · (𝐶(-g‘𝑅)( 1 · 𝐶))) = (( 1 · 𝐶)(-g‘𝑅)( 1 · ( 1 · 𝐶)))) |
29 | 4, 7 | ressmulr 17259 |
. . . . . . . . 9
⊢ (𝐼 ∈ (2Ideal‘𝑅) → · =
(.r‘𝐽)) |
30 | 3, 29 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → · =
(.r‘𝐽)) |
31 | 30 | oveqd 7429 |
. . . . . . 7
⊢ (𝜑 → ( 1 · ( 1 · 𝐶)) = ( 1 (.r‘𝐽)( 1 · 𝐶))) |
32 | 31 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · ( 1 · 𝐶)) = ( 1 (.r‘𝐽)( 1 · 𝐶))) |
33 | | eqid 2731 |
. . . . . . 7
⊢
(Base‘𝐽) =
(Base‘𝐽) |
34 | | eqid 2731 |
. . . . . . 7
⊢
(.r‘𝐽) = (.r‘𝐽) |
35 | 5 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → 𝐽 ∈ Ring) |
36 | 1, 3, 4, 5, 6, 7, 8 | rngqiprngghmlem1 21050 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ 𝐵) → ( 1 · 𝐶) ∈ (Base‘𝐽)) |
37 | 36 | 3adant2 1130 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · 𝐶) ∈ (Base‘𝐽)) |
38 | 33, 34, 8, 35, 37 | ringlidmd 20164 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 (.r‘𝐽)( 1 · 𝐶)) = ( 1 · 𝐶)) |
39 | 32, 38 | eqtrd 2771 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · ( 1 · 𝐶)) = ( 1 · 𝐶)) |
40 | 39 | oveq2d 7428 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → (( 1 · 𝐶)(-g‘𝑅)( 1 · ( 1 · 𝐶))) = (( 1 · 𝐶)(-g‘𝑅)( 1 · 𝐶))) |
41 | | eqid 2731 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
42 | 6, 41, 17 | grpsubid 18947 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ ( 1 · 𝐶) ∈ 𝐵) → (( 1 · 𝐶)(-g‘𝑅)( 1 · 𝐶)) = (0g‘𝑅)) |
43 | 13, 16, 42 | syl2anc 583 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → (( 1 · 𝐶)(-g‘𝑅)( 1 · 𝐶)) = (0g‘𝑅)) |
44 | 28, 40, 43 | 3eqtrd 2775 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · (𝐶(-g‘𝑅)( 1 · 𝐶))) = (0g‘𝑅)) |
45 | 44 | oveq1d 7427 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → (( 1 · (𝐶(-g‘𝑅)( 1 · 𝐶)))(+g‘𝑅)( 1 · 𝐴)) = ((0g‘𝑅)(+g‘𝑅)( 1 · 𝐴))) |
46 | 6, 7 | rngcl 20062 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵) → ( 1 · 𝐴) ∈ 𝐵) |
47 | 2, 10, 24, 46 | syl3anc 1370 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · 𝐴) ∈ 𝐵) |
48 | 6, 25, 41, 13, 47 | grplidd 18894 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ((0g‘𝑅)(+g‘𝑅)( 1 · 𝐴)) = ( 1 · 𝐴)) |
49 | 30 | oveqd 7429 |
. . . 4
⊢ (𝜑 → ( 1 · 𝐴) = ( 1 (.r‘𝐽)𝐴)) |
50 | 49 | 3ad2ant1 1132 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · 𝐴) = ( 1 (.r‘𝐽)𝐴)) |
51 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼) → 𝐽 ∈ Ring) |
52 | 3, 4, 33 | 2idlbas 21022 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐽) = 𝐼) |
53 | 52 | eqcomd 2737 |
. . . . . . 7
⊢ (𝜑 → 𝐼 = (Base‘𝐽)) |
54 | 53 | eleq2d 2818 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ (Base‘𝐽))) |
55 | 54 | biimpa 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ (Base‘𝐽)) |
56 | 33, 34, 8, 51, 55 | ringlidmd 20164 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼) → ( 1 (.r‘𝐽)𝐴) = 𝐴) |
57 | 56 | 3adant3 1131 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 (.r‘𝐽)𝐴) = 𝐴) |
58 | 48, 50, 57 | 3eqtrd 2775 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ((0g‘𝑅)(+g‘𝑅)( 1 · 𝐴)) = 𝐴) |
59 | 27, 45, 58 | 3eqtrd 2775 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐼 ∧ 𝐶 ∈ 𝐵) → ( 1 · ((𝐶(-g‘𝑅)( 1 · 𝐶))(+g‘𝑅)𝐴)) = 𝐴) |