| Step | Hyp | Ref
| Expression |
| 1 | | rng2idl1cntr.j |
. . . . 5
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
| 2 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 3 | 1, 2 | ressbasss 17284 |
. . . 4
⊢
(Base‘𝐽)
⊆ (Base‘𝑅) |
| 4 | | rng2idl1cntr.u |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Ring) |
| 5 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐽) =
(Base‘𝐽) |
| 6 | | rng2idl1cntr.1 |
. . . . . 6
⊢ 1 =
(1r‘𝐽) |
| 7 | 5, 6 | ringidcl 20262 |
. . . . 5
⊢ (𝐽 ∈ Ring → 1 ∈
(Base‘𝐽)) |
| 8 | 4, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 1 ∈ (Base‘𝐽)) |
| 9 | 3, 8 | sselid 3981 |
. . 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 2737 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 15 | 2, 14 | rngass 20156 |
. . . . . 6
⊢ ((𝑅 ∈ Rng ∧ ( 1 ∈
(Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 1 ∈ (Base‘𝑅))) → (( 1 (.r‘𝑅)𝑥)(.r‘𝑅) 1 ) = ( 1 (.r‘𝑅)(𝑥(.r‘𝑅) 1 ))) |
| 16 | 11, 12, 13, 12, 15 | syl13anc 1374 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (( 1 (.r‘𝑅)𝑥)(.r‘𝑅) 1 ) = ( 1 (.r‘𝑅)(𝑥(.r‘𝑅) 1 ))) |
| 17 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝐽) = (.r‘𝐽) |
| 18 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐽 ∈ Ring) |
| 19 | | rng2idl1cntr.i |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) |
| 20 | 10, 19, 1, 4, 2, 14,
6 | rngqiprngghmlem1 21297 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)𝑥) ∈ (Base‘𝐽)) |
| 21 | 5, 17, 6, 18, 20 | ringridmd 20270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (( 1 (.r‘𝑅)𝑥)(.r‘𝐽) 1 ) = ( 1 (.r‘𝑅)𝑥)) |
| 22 | 1, 14 | ressmulr 17351 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (2Ideal‘𝑅) →
(.r‘𝑅) =
(.r‘𝐽)) |
| 23 | 19, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (.r‘𝑅) = (.r‘𝐽)) |
| 24 | 23 | oveqd 7448 |
. . . . . . . 8
⊢ (𝜑 → (( 1 (.r‘𝑅)𝑥)(.r‘𝑅) 1 ) = (( 1 (.r‘𝑅)𝑥)(.r‘𝐽) 1 )) |
| 25 | 24 | eqeq1d 2739 |
. . . . . . 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 21264 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) |
| 29 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
| 30 | 2, 29 | lidlss 21222 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (LIdeal‘𝑅) → 𝐼 ⊆ (Base‘𝑅)) |
| 31 | 1, 2 | ressbas2 17283 |
. . . . . . . . . . . 12
⊢ (𝐼 ⊆ (Base‘𝑅) → 𝐼 = (Base‘𝐽)) |
| 32 | 31 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝐼 ⊆ (Base‘𝑅) → (Base‘𝐽) = 𝐼) |
| 33 | 28, 30, 32 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝐽) = 𝐼) |
| 34 | 33, 28 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝐽) ∈ (LIdeal‘𝑅)) |
| 35 | 19, 1, 5 | 2idlbas 21273 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝐽) = 𝐼) |
| 36 | | ringrng 20282 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ Ring → 𝐽 ∈ Rng) |
| 37 | 4, 36 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ Rng) |
| 38 | 1, 37 | eqeltrrid 2846 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅 ↾s 𝐼) ∈ Rng) |
| 39 | 10, 19, 38 | rng2idlsubrng 21275 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ (SubRng‘𝑅)) |
| 40 | 35, 39 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝐽) ∈ (SubRng‘𝑅)) |
| 41 | | subrngsubg 20552 |
. . . . . . . . . 10
⊢
((Base‘𝐽)
∈ (SubRng‘𝑅)
→ (Base‘𝐽)
∈ (SubGrp‘𝑅)) |
| 42 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 43 | 42 | subg0cl 19152 |
. . . . . . . . . 10
⊢
((Base‘𝐽)
∈ (SubGrp‘𝑅)
→ (0g‘𝑅) ∈ (Base‘𝐽)) |
| 44 | 40, 41, 43 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝐽)) |
| 45 | 10, 34, 44 | 3jca 1129 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 ∈ Rng ∧ (Base‘𝐽) ∈ (LIdeal‘𝑅) ∧
(0g‘𝑅)
∈ (Base‘𝐽))) |
| 46 | 8 | anim1ci 616 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥 ∈ (Base‘𝑅) ∧ 1 ∈ (Base‘𝐽))) |
| 47 | 42, 2, 14, 29 | rnglidlmcl 21226 |
. . . . . . . 8
⊢ (((𝑅 ∈ Rng ∧
(Base‘𝐽) ∈
(LIdeal‘𝑅) ∧
(0g‘𝑅)
∈ (Base‘𝐽))
∧ (𝑥 ∈
(Base‘𝑅) ∧ 1 ∈
(Base‘𝐽))) →
(𝑥(.r‘𝑅) 1 ) ∈ (Base‘𝐽)) |
| 48 | 45, 46, 47 | syl2an2r 685 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅) 1 ) ∈ (Base‘𝐽)) |
| 49 | 5, 17, 6, 18, 48 | ringlidmd 20269 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ( 1 (.r‘𝐽)(𝑥(.r‘𝑅) 1 )) = (𝑥(.r‘𝑅) 1 )) |
| 50 | 23 | oveqd 7448 |
. . . . . . . 8
⊢ (𝜑 → ( 1 (.r‘𝑅)(𝑥(.r‘𝑅) 1 )) = ( 1 (.r‘𝐽)(𝑥(.r‘𝑅) 1 ))) |
| 51 | 50 | eqeq1d 2739 |
. . . . . . 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 2785 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)𝑥) = (𝑥(.r‘𝑅) 1 )) |
| 55 | 54 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)( 1 (.r‘𝑅)𝑥) = (𝑥(.r‘𝑅) 1 )) |
| 56 | | ssidd 4007 |
. . . 4
⊢ (𝜑 → (Base‘𝑅) ⊆ (Base‘𝑅)) |
| 57 | | rng2idl1cntr.m |
. . . . . 6
⊢ 𝑀 = (mulGrp‘𝑅) |
| 58 | 57, 2 | mgpbas 20142 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑀) |
| 59 | 57, 14 | mgpplusg 20141 |
. . . . 5
⊢
(.r‘𝑅) = (+g‘𝑀) |
| 60 | | eqid 2737 |
. . . . 5
⊢
(Cntz‘𝑀) =
(Cntz‘𝑀) |
| 61 | 58, 59, 60 | elcntz 19340 |
. . . 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 713 |
. 2
⊢ (𝜑 → 1 ∈ ((Cntz‘𝑀)‘(Base‘𝑅))) |
| 64 | 58, 60 | cntrval 19337 |
. 2
⊢
((Cntz‘𝑀)‘(Base‘𝑅)) = (Cntr‘𝑀) |
| 65 | 63, 64 | eleqtrdi 2851 |
1
⊢ (𝜑 → 1 ∈ (Cntr‘𝑀)) |