| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ringi.1 | . . . 4
⊢ 𝐺 = (1st ‘𝑅) | 
| 2 |  | ringi.2 | . . . 4
⊢ 𝐻 = (2nd ‘𝑅) | 
| 3 |  | ringi.3 | . . . 4
⊢ 𝑋 = ran 𝐺 | 
| 4 | 1, 2, 3 | rngoi 37907 | . . 3
⊢ (𝑅 ∈ RingOps → ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑢𝐻𝑥)𝐻𝑦) = (𝑢𝐻(𝑥𝐻𝑦)) ∧ (𝑢𝐻(𝑥𝐺𝑦)) = ((𝑢𝐻𝑥)𝐺(𝑢𝐻𝑦)) ∧ ((𝑢𝐺𝑥)𝐻𝑦) = ((𝑢𝐻𝑦)𝐺(𝑥𝐻𝑦))) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)))) | 
| 5 | 4 | simprrd 773 | . 2
⊢ (𝑅 ∈ RingOps →
∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) | 
| 6 |  | simpl 482 | . . . . . . 7
⊢ (((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) → (𝑢𝐻𝑥) = 𝑥) | 
| 7 | 6 | ralimi 3082 | . . . . . 6
⊢
(∀𝑥 ∈
𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) → ∀𝑥 ∈ 𝑋 (𝑢𝐻𝑥) = 𝑥) | 
| 8 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑢𝐻𝑥) = (𝑢𝐻𝑦)) | 
| 9 |  | id 22 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) | 
| 10 | 8, 9 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑢𝐻𝑥) = 𝑥 ↔ (𝑢𝐻𝑦) = 𝑦)) | 
| 11 | 10 | rspcv 3617 | . . . . . 6
⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑢𝐻𝑥) = 𝑥 → (𝑢𝐻𝑦) = 𝑦)) | 
| 12 | 7, 11 | syl5 34 | . . . . 5
⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) → (𝑢𝐻𝑦) = 𝑦)) | 
| 13 |  | simpr 484 | . . . . . . 7
⊢ (((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥) → (𝑥𝐻𝑦) = 𝑥) | 
| 14 | 13 | ralimi 3082 | . . . . . 6
⊢
(∀𝑥 ∈
𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥) → ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑦) = 𝑥) | 
| 15 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = 𝑢 → (𝑥𝐻𝑦) = (𝑢𝐻𝑦)) | 
| 16 |  | id 22 | . . . . . . . 8
⊢ (𝑥 = 𝑢 → 𝑥 = 𝑢) | 
| 17 | 15, 16 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑥 = 𝑢 → ((𝑥𝐻𝑦) = 𝑥 ↔ (𝑢𝐻𝑦) = 𝑢)) | 
| 18 | 17 | rspcv 3617 | . . . . . 6
⊢ (𝑢 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑦) = 𝑥 → (𝑢𝐻𝑦) = 𝑢)) | 
| 19 | 14, 18 | syl5 34 | . . . . 5
⊢ (𝑢 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥) → (𝑢𝐻𝑦) = 𝑢)) | 
| 20 | 12, 19 | im2anan9r 621 | . . . 4
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → ((𝑢𝐻𝑦) = 𝑦 ∧ (𝑢𝐻𝑦) = 𝑢))) | 
| 21 |  | eqtr2 2760 | . . . . 5
⊢ (((𝑢𝐻𝑦) = 𝑦 ∧ (𝑢𝐻𝑦) = 𝑢) → 𝑦 = 𝑢) | 
| 22 | 21 | equcomd 2017 | . . . 4
⊢ (((𝑢𝐻𝑦) = 𝑦 ∧ (𝑢𝐻𝑦) = 𝑢) → 𝑢 = 𝑦) | 
| 23 | 20, 22 | syl6 35 | . . 3
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦)) | 
| 24 | 23 | rgen2 3198 | . 2
⊢
∀𝑢 ∈
𝑋 ∀𝑦 ∈ 𝑋 ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦) | 
| 25 |  | oveq1 7439 | . . . . 5
⊢ (𝑢 = 𝑦 → (𝑢𝐻𝑥) = (𝑦𝐻𝑥)) | 
| 26 | 25 | eqeq1d 2738 | . . . 4
⊢ (𝑢 = 𝑦 → ((𝑢𝐻𝑥) = 𝑥 ↔ (𝑦𝐻𝑥) = 𝑥)) | 
| 27 | 26 | ovanraleqv 7456 | . . 3
⊢ (𝑢 = 𝑦 → (∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥))) | 
| 28 | 27 | reu4 3736 | . 2
⊢
(∃!𝑢 ∈
𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ (∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑢 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦))) | 
| 29 | 5, 24, 28 | sylanblrc 590 | 1
⊢ (𝑅 ∈ RingOps →
∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) |