| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | uznzr.1 | . . . 4
⊢ 𝐺 = (1st ‘𝑅) | 
| 2 |  | uznzr.5 | . . . 4
⊢ 𝑋 = ran 𝐺 | 
| 3 |  | uznzr.3 | . . . 4
⊢ 𝑍 = (GId‘𝐺) | 
| 4 | 1, 2, 3 | rngo0cl 37927 | . . 3
⊢ (𝑅 ∈ RingOps → 𝑍 ∈ 𝑋) | 
| 5 |  | en1eqsn 9309 | . . . . . 6
⊢ ((𝑍 ∈ 𝑋 ∧ 𝑋 ≈ 1o) → 𝑋 = {𝑍}) | 
| 6 | 1 | rneqi 5947 | . . . . . . . 8
⊢ ran 𝐺 = ran (1st
‘𝑅) | 
| 7 |  | uznzr.2 | . . . . . . . 8
⊢ 𝐻 = (2nd ‘𝑅) | 
| 8 |  | uznzr.4 | . . . . . . . 8
⊢ 𝑈 = (GId‘𝐻) | 
| 9 | 6, 7, 8 | rngo1cl 37947 | . . . . . . 7
⊢ (𝑅 ∈ RingOps → 𝑈 ∈ ran 𝐺) | 
| 10 |  | eleq2 2829 | . . . . . . . . . 10
⊢ (𝑋 = {𝑍} → (𝑈 ∈ 𝑋 ↔ 𝑈 ∈ {𝑍})) | 
| 11 | 10 | biimpd 229 | . . . . . . . . 9
⊢ (𝑋 = {𝑍} → (𝑈 ∈ 𝑋 → 𝑈 ∈ {𝑍})) | 
| 12 |  | elsni 4642 | . . . . . . . . 9
⊢ (𝑈 ∈ {𝑍} → 𝑈 = 𝑍) | 
| 13 | 11, 12 | syl6com 37 | . . . . . . . 8
⊢ (𝑈 ∈ 𝑋 → (𝑋 = {𝑍} → 𝑈 = 𝑍)) | 
| 14 | 2 | eqcomi 2745 | . . . . . . . 8
⊢ ran 𝐺 = 𝑋 | 
| 15 | 13, 14 | eleq2s 2858 | . . . . . . 7
⊢ (𝑈 ∈ ran 𝐺 → (𝑋 = {𝑍} → 𝑈 = 𝑍)) | 
| 16 | 9, 15 | syl 17 | . . . . . 6
⊢ (𝑅 ∈ RingOps → (𝑋 = {𝑍} → 𝑈 = 𝑍)) | 
| 17 | 5, 16 | syl5com 31 | . . . . 5
⊢ ((𝑍 ∈ 𝑋 ∧ 𝑋 ≈ 1o) → (𝑅 ∈ RingOps → 𝑈 = 𝑍)) | 
| 18 | 17 | ex 412 | . . . 4
⊢ (𝑍 ∈ 𝑋 → (𝑋 ≈ 1o → (𝑅 ∈ RingOps → 𝑈 = 𝑍))) | 
| 19 | 18 | com23 86 | . . 3
⊢ (𝑍 ∈ 𝑋 → (𝑅 ∈ RingOps → (𝑋 ≈ 1o → 𝑈 = 𝑍))) | 
| 20 | 4, 19 | mpcom 38 | . 2
⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o →
𝑈 = 𝑍)) | 
| 21 | 1, 2 | rngone0 37919 | . . 3
⊢ (𝑅 ∈ RingOps → 𝑋 ≠ ∅) | 
| 22 |  | oveq2 7440 | . . . . . 6
⊢ (𝑈 = 𝑍 → (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) | 
| 23 | 22 | ralrimivw 3149 | . . . . 5
⊢ (𝑈 = 𝑍 → ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) | 
| 24 | 3, 2, 1, 7 | rngorz 37931 | . . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → (𝑥𝐻𝑍) = 𝑍) | 
| 25 | 24 | ralrimiva 3145 | . . . . . 6
⊢ (𝑅 ∈ RingOps →
∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍) | 
| 26 | 2, 6 | eqtri 2764 | . . . . . . . . 9
⊢ 𝑋 = ran (1st
‘𝑅) | 
| 27 | 7, 26, 8 | rngoridm 37946 | . . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → (𝑥𝐻𝑈) = 𝑥) | 
| 28 | 27 | ralrimiva 3145 | . . . . . . 7
⊢ (𝑅 ∈ RingOps →
∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = 𝑥) | 
| 29 |  | r19.26 3110 | . . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ↔ (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = 𝑥 ∧ ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍))) | 
| 30 |  | r19.26 3110 | . . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑋 (((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) ↔ (∀𝑥 ∈ 𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍)) | 
| 31 |  | eqtr 2759 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = (𝑥𝐻𝑈) ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → 𝑥 = (𝑥𝐻𝑍)) | 
| 32 |  | eqtr 2759 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = (𝑥𝐻𝑍) ∧ (𝑥𝐻𝑍) = 𝑍) → 𝑥 = 𝑍) | 
| 33 | 32 | ex 412 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑥𝐻𝑍) → ((𝑥𝐻𝑍) = 𝑍 → 𝑥 = 𝑍)) | 
| 34 | 31, 33 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = (𝑥𝐻𝑈) ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → ((𝑥𝐻𝑍) = 𝑍 → 𝑥 = 𝑍)) | 
| 35 | 34 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑥𝐻𝑈) → ((𝑥𝐻𝑈) = (𝑥𝐻𝑍) → ((𝑥𝐻𝑍) = 𝑍 → 𝑥 = 𝑍))) | 
| 36 | 35 | eqcoms 2744 | . . . . . . . . . . . . . . 15
⊢ ((𝑥𝐻𝑈) = 𝑥 → ((𝑥𝐻𝑈) = (𝑥𝐻𝑍) → ((𝑥𝐻𝑍) = 𝑍 → 𝑥 = 𝑍))) | 
| 37 | 36 | imp31 417 | . . . . . . . . . . . . . 14
⊢ ((((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) → 𝑥 = 𝑍) | 
| 38 | 37 | ralimi 3082 | . . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑋 (((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) → ∀𝑥 ∈ 𝑋 𝑥 = 𝑍) | 
| 39 |  | eqsn 4828 | . . . . . . . . . . . . . . 15
⊢ (𝑋 ≠ ∅ → (𝑋 = {𝑍} ↔ ∀𝑥 ∈ 𝑋 𝑥 = 𝑍)) | 
| 40 |  | ensn1g 9063 | . . . . . . . . . . . . . . . . 17
⊢ (𝑍 ∈ 𝑋 → {𝑍} ≈ 1o) | 
| 41 | 4, 40 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ RingOps → {𝑍} ≈
1o) | 
| 42 |  | breq1 5145 | . . . . . . . . . . . . . . . 16
⊢ (𝑋 = {𝑍} → (𝑋 ≈ 1o ↔ {𝑍} ≈
1o)) | 
| 43 | 41, 42 | imbitrrid 246 | . . . . . . . . . . . . . . 15
⊢ (𝑋 = {𝑍} → (𝑅 ∈ RingOps → 𝑋 ≈ 1o)) | 
| 44 | 39, 43 | biimtrrdi 254 | . . . . . . . . . . . . . 14
⊢ (𝑋 ≠ ∅ →
(∀𝑥 ∈ 𝑋 𝑥 = 𝑍 → (𝑅 ∈ RingOps → 𝑋 ≈ 1o))) | 
| 45 | 44 | com3l 89 | . . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑋 𝑥 = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))) | 
| 46 | 38, 45 | syl 17 | . . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑋 (((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ (𝑥𝐻𝑍) = 𝑍) → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))) | 
| 47 | 30, 46 | sylbir 235 | . . . . . . . . . . 11
⊢
((∀𝑥 ∈
𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) ∧ ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍) → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))) | 
| 48 | 47 | ex 412 | . . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑋 ((𝑥𝐻𝑈) = 𝑥 ∧ (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))) | 
| 49 | 29, 48 | sylbir 235 | . . . . . . . . 9
⊢
((∀𝑥 ∈
𝑋 (𝑥𝐻𝑈) = 𝑥 ∧ ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍)) → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))) | 
| 50 | 49 | ex 412 | . . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 (𝑥𝐻𝑈) = 𝑥 → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))))) | 
| 51 | 50 | com24 95 | . . . . . . 7
⊢
(∀𝑥 ∈
𝑋 (𝑥𝐻𝑈) = 𝑥 → (𝑅 ∈ RingOps → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍 → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))))) | 
| 52 | 28, 51 | mpcom 38 | . . . . . 6
⊢ (𝑅 ∈ RingOps →
(∀𝑥 ∈ 𝑋 (𝑥𝐻𝑍) = 𝑍 → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (𝑋 ≠ ∅ → 𝑋 ≈ 1o)))) | 
| 53 | 25, 52 | mpd 15 | . . . . 5
⊢ (𝑅 ∈ RingOps →
(∀𝑥 ∈ 𝑋 (𝑥𝐻𝑈) = (𝑥𝐻𝑍) → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))) | 
| 54 | 23, 53 | syl5com 31 | . . . 4
⊢ (𝑈 = 𝑍 → (𝑅 ∈ RingOps → (𝑋 ≠ ∅ → 𝑋 ≈ 1o))) | 
| 55 | 54 | com13 88 | . . 3
⊢ (𝑋 ≠ ∅ → (𝑅 ∈ RingOps → (𝑈 = 𝑍 → 𝑋 ≈ 1o))) | 
| 56 | 21, 55 | mpcom 38 | . 2
⊢ (𝑅 ∈ RingOps → (𝑈 = 𝑍 → 𝑋 ≈ 1o)) | 
| 57 | 20, 56 | impbid 212 | 1
⊢ (𝑅 ∈ RingOps → (𝑋 ≈ 1o ↔
𝑈 = 𝑍)) |