Step | Hyp | Ref
| Expression |
1 | | rng2idl1cntr.j |
. . . . 5
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
2 | | eqid 2728 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | 1, 2 | ressbasss 17213 |
. . . 4
⊢
(Base‘𝐽)
⊆ (Base‘𝑅) |
4 | | rng2idl1cntr.u |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Ring) |
5 | | eqid 2728 |
. . . . . 6
⊢
(Base‘𝐽) =
(Base‘𝐽) |
6 | | rng2idl1cntr.1 |
. . . . . 6
⊢ 1 =
(1r‘𝐽) |
7 | 5, 6 | ringidcl 20196 |
. . . . 5
⊢ (𝐽 ∈ Ring → 1 ∈
(Base‘𝐽)) |
8 | 4, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 1 ∈ (Base‘𝐽)) |
9 | 3, 8 | sselid 3977 |
. . 3
⊢ (𝜑 → 1 ∈ (Base‘𝑅)) |
10 | | rng2idl1cntr.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Rng) |
11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Rng) |
12 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 1 ∈ (Base‘𝑅)) |
13 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
14 | | eqid 2728 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
15 | 2, 14 | rngass 20093 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ ( 1 ∈
(Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 1 ∈ (Base‘𝑅))) → (( 1 (.r‘𝑅)𝑥)(.r‘𝑅) 1 ) = ( 1 (.r‘𝑅)(𝑥(.r‘𝑅) 1 ))) |
16 | 11, 12, 13, 12, 15 | syl13anc 1370 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (( 1 (.r‘𝑅)𝑥)(.r‘𝑅) 1 ) = ( 1 (.r‘𝑅)(𝑥(.r‘𝑅) 1 ))) |
17 | | eqid 2728 |
. . . . . . 7
⊢
(.r‘𝐽) = (.r‘𝐽) |
18 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐽 ∈ Ring) |
19 | | rng2idl1cntr.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) |
20 | 10, 19, 1, 4, 2, 14,
6 | rngqiprngghmlem1 21171 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)𝑥) ∈ (Base‘𝐽)) |
21 | 5, 17, 6, 18, 20 | ringridmd 20203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (( 1 (.r‘𝑅)𝑥)(.r‘𝐽) 1 ) = ( 1 (.r‘𝑅)𝑥)) |
22 | 1, 14 | ressmulr 17282 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (2Ideal‘𝑅) →
(.r‘𝑅) =
(.r‘𝐽)) |
23 | 19, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (.r‘𝑅) = (.r‘𝐽)) |
24 | 23 | oveqd 7432 |
. . . . . . . 8
⊢ (𝜑 → (( 1 (.r‘𝑅)𝑥)(.r‘𝑅) 1 ) = (( 1 (.r‘𝑅)𝑥)(.r‘𝐽) 1 )) |
25 | 24 | eqeq1d 2730 |
. . . . . . 7
⊢ (𝜑 → ((( 1 (.r‘𝑅)𝑥)(.r‘𝑅) 1 ) = ( 1 (.r‘𝑅)𝑥) ↔ (( 1 (.r‘𝑅)𝑥)(.r‘𝐽) 1 ) = ( 1 (.r‘𝑅)𝑥))) |
26 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((( 1 (.r‘𝑅)𝑥)(.r‘𝑅) 1 ) = ( 1 (.r‘𝑅)𝑥) ↔ (( 1 (.r‘𝑅)𝑥)(.r‘𝐽) 1 ) = ( 1 (.r‘𝑅)𝑥))) |
27 | 21, 26 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (( 1 (.r‘𝑅)𝑥)(.r‘𝑅) 1 ) = ( 1 (.r‘𝑅)𝑥)) |
28 | 19 | 2idllidld 21142 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) |
29 | | eqid 2728 |
. . . . . . . . . . . 12
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
30 | 2, 29 | lidlss 21102 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (LIdeal‘𝑅) → 𝐼 ⊆ (Base‘𝑅)) |
31 | 1, 2 | ressbas2 17212 |
. . . . . . . . . . . 12
⊢ (𝐼 ⊆ (Base‘𝑅) → 𝐼 = (Base‘𝐽)) |
32 | 31 | eqcomd 2734 |
. . . . . . . . . . 11
⊢ (𝐼 ⊆ (Base‘𝑅) → (Base‘𝐽) = 𝐼) |
33 | 28, 30, 32 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝐽) = 𝐼) |
34 | 33, 28 | eqeltrd 2829 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝐽) ∈ (LIdeal‘𝑅)) |
35 | 19, 1, 5 | 2idlbas 21151 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝐽) = 𝐼) |
36 | | ringrng 20215 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ Ring → 𝐽 ∈ Rng) |
37 | 4, 36 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ Rng) |
38 | 1, 37 | eqeltrrid 2834 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng) |
39 | 10, 19, 38 | rng2idlsubrng 21153 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ (SubRng‘𝑅)) |
40 | 35, 39 | eqeltrd 2829 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝐽) ∈ (SubRng‘𝑅)) |
41 | | subrngsubg 20483 |
. . . . . . . . . 10
⊢
((Base‘𝐽)
∈ (SubRng‘𝑅)
→ (Base‘𝐽)
∈ (SubGrp‘𝑅)) |
42 | | eqid 2728 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
43 | 42 | subg0cl 19083 |
. . . . . . . . . 10
⊢
((Base‘𝐽)
∈ (SubGrp‘𝑅)
→ (0g‘𝑅) ∈ (Base‘𝐽)) |
44 | 40, 41, 43 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝐽)) |
45 | 10, 34, 44 | 3jca 1126 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 ∈ Rng ∧ (Base‘𝐽) ∈ (LIdeal‘𝑅) ∧
(0g‘𝑅)
∈ (Base‘𝐽))) |
46 | 8 | anim1ci 615 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥 ∈ (Base‘𝑅) ∧ 1 ∈ (Base‘𝐽))) |
47 | 42, 2, 14, 29 | rnglidlmcl 21106 |
. . . . . . . 8
⊢ (((𝑅 ∈ Rng ∧
(Base‘𝐽) ∈
(LIdeal‘𝑅) ∧
(0g‘𝑅)
∈ (Base‘𝐽))
∧ (𝑥 ∈
(Base‘𝑅) ∧ 1 ∈
(Base‘𝐽))) →
(𝑥(.r‘𝑅) 1 ) ∈ (Base‘𝐽)) |
48 | 45, 46, 47 | syl2an2r 684 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅) 1 ) ∈ (Base‘𝐽)) |
49 | 5, 17, 6, 18, 48 | ringlidmd 20202 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ( 1 (.r‘𝐽)(𝑥(.r‘𝑅) 1 )) = (𝑥(.r‘𝑅) 1 )) |
50 | 23 | oveqd 7432 |
. . . . . . . 8
⊢ (𝜑 → ( 1 (.r‘𝑅)(𝑥(.r‘𝑅) 1 )) = ( 1 (.r‘𝐽)(𝑥(.r‘𝑅) 1 ))) |
51 | 50 | eqeq1d 2730 |
. . . . . . 7
⊢ (𝜑 → (( 1 (.r‘𝑅)(𝑥(.r‘𝑅) 1 )) = (𝑥(.r‘𝑅) 1 ) ↔ ( 1
(.r‘𝐽)(𝑥(.r‘𝑅) 1 )) = (𝑥(.r‘𝑅) 1 ))) |
52 | 51 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (( 1 (.r‘𝑅)(𝑥(.r‘𝑅) 1 )) = (𝑥(.r‘𝑅) 1 ) ↔ ( 1
(.r‘𝐽)(𝑥(.r‘𝑅) 1 )) = (𝑥(.r‘𝑅) 1 ))) |
53 | 49, 52 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)(𝑥(.r‘𝑅) 1 )) = (𝑥(.r‘𝑅) 1 )) |
54 | 16, 27, 53 | 3eqtr3d 2776 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)𝑥) = (𝑥(.r‘𝑅) 1 )) |
55 | 54 | ralrimiva 3142 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)( 1 (.r‘𝑅)𝑥) = (𝑥(.r‘𝑅) 1 )) |
56 | | ssidd 4002 |
. . . 4
⊢ (𝜑 → (Base‘𝑅) ⊆ (Base‘𝑅)) |
57 | | rng2idl1cntr.m |
. . . . . 6
⊢ 𝑀 = (mulGrp‘𝑅) |
58 | 57, 2 | mgpbas 20074 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑀) |
59 | 57, 14 | mgpplusg 20072 |
. . . . 5
⊢
(.r‘𝑅) = (+g‘𝑀) |
60 | | eqid 2728 |
. . . . 5
⊢
(Cntz‘𝑀) =
(Cntz‘𝑀) |
61 | 58, 59, 60 | elcntz 19267 |
. . . 4
⊢
((Base‘𝑅)
⊆ (Base‘𝑅)
→ ( 1 ∈ ((Cntz‘𝑀)‘(Base‘𝑅)) ↔ ( 1 ∈ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)( 1 (.r‘𝑅)𝑥) = (𝑥(.r‘𝑅) 1 )))) |
62 | 56, 61 | syl 17 |
. . 3
⊢ (𝜑 → ( 1 ∈ ((Cntz‘𝑀)‘(Base‘𝑅)) ↔ ( 1 ∈ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)( 1 (.r‘𝑅)𝑥) = (𝑥(.r‘𝑅) 1 )))) |
63 | 9, 55, 62 | mpbir2and 712 |
. 2
⊢ (𝜑 → 1 ∈ ((Cntz‘𝑀)‘(Base‘𝑅))) |
64 | 58, 60 | cntrval 19264 |
. 2
⊢
((Cntz‘𝑀)‘(Base‘𝑅)) = (Cntr‘𝑀) |
65 | 63, 64 | eleqtrdi 2839 |
1
⊢ (𝜑 → 1 ∈ (Cntr‘𝑀)) |