Step | Hyp | Ref
| Expression |
1 | | ringi.1 |
. . . . 5
⊢ 𝐺 = (1st ‘𝑅) |
2 | | ringi.2 |
. . . . 5
⊢ 𝐻 = (2nd ‘𝑅) |
3 | | ringi.3 |
. . . . 5
⊢ 𝑋 = ran 𝐺 |
4 | 1, 2, 3 | rngoi 32868 |
. . . 4
⊢ (𝑅 ∈ RingOps → ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑢𝐻𝑥)𝐻𝑦) = (𝑢𝐻(𝑥𝐻𝑦)) ∧ (𝑢𝐻(𝑥𝐺𝑦)) = ((𝑢𝐻𝑥)𝐺(𝑢𝐻𝑦)) ∧ ((𝑢𝐺𝑥)𝐻𝑦) = ((𝑢𝐻𝑦)𝐺(𝑥𝐻𝑦))) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)))) |
5 | 4 | simprrd 793 |
. . 3
⊢ (𝑅 ∈ RingOps →
∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) |
6 | | simpl 472 |
. . . . . . . 8
⊢ (((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) → (𝑢𝐻𝑥) = 𝑥) |
7 | 6 | ralimi 2936 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) → ∀𝑥 ∈ 𝑋 (𝑢𝐻𝑥) = 𝑥) |
8 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑢𝐻𝑥) = (𝑢𝐻𝑦)) |
9 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
10 | 8, 9 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑢𝐻𝑥) = 𝑥 ↔ (𝑢𝐻𝑦) = 𝑦)) |
11 | 10 | rspcv 3278 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑢𝐻𝑥) = 𝑥 → (𝑢𝐻𝑦) = 𝑦)) |
12 | 7, 11 | syl5 33 |
. . . . . 6
⊢ (𝑦 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) → (𝑢𝐻𝑦) = 𝑦)) |
13 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥) → (𝑥𝐻𝑦) = 𝑥) |
14 | 13 | ralimi 2936 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥) → ∀𝑥 ∈ 𝑋 (𝑥𝐻𝑦) = 𝑥) |
15 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → (𝑥𝐻𝑦) = (𝑢𝐻𝑦)) |
16 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → 𝑥 = 𝑢) |
17 | 15, 16 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((𝑥𝐻𝑦) = 𝑥 ↔ (𝑢𝐻𝑦) = 𝑢)) |
18 | 17 | rspcv 3278 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (𝑥𝐻𝑦) = 𝑥 → (𝑢𝐻𝑦) = 𝑢)) |
19 | 14, 18 | syl5 33 |
. . . . . 6
⊢ (𝑢 ∈ 𝑋 → (∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥) → (𝑢𝐻𝑦) = 𝑢)) |
20 | 12, 19 | im2anan9r 877 |
. . . . 5
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → ((𝑢𝐻𝑦) = 𝑦 ∧ (𝑢𝐻𝑦) = 𝑢))) |
21 | | eqtr2 2630 |
. . . . . 6
⊢ (((𝑢𝐻𝑦) = 𝑦 ∧ (𝑢𝐻𝑦) = 𝑢) → 𝑦 = 𝑢) |
22 | 21 | eqcomd 2616 |
. . . . 5
⊢ (((𝑢𝐻𝑦) = 𝑦 ∧ (𝑢𝐻𝑦) = 𝑢) → 𝑢 = 𝑦) |
23 | 20, 22 | syl6 34 |
. . . 4
⊢ ((𝑢 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦)) |
24 | 23 | rgen2a 2960 |
. . 3
⊢
∀𝑢 ∈
𝑋 ∀𝑦 ∈ 𝑋 ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦) |
25 | 5, 24 | jctir 559 |
. 2
⊢ (𝑅 ∈ RingOps →
(∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑢 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦))) |
26 | | oveq1 6556 |
. . . . . 6
⊢ (𝑢 = 𝑦 → (𝑢𝐻𝑥) = (𝑦𝐻𝑥)) |
27 | 26 | eqeq1d 2612 |
. . . . 5
⊢ (𝑢 = 𝑦 → ((𝑢𝐻𝑥) = 𝑥 ↔ (𝑦𝐻𝑥) = 𝑥)) |
28 | | oveq2 6557 |
. . . . . 6
⊢ (𝑢 = 𝑦 → (𝑥𝐻𝑢) = (𝑥𝐻𝑦)) |
29 | 28 | eqeq1d 2612 |
. . . . 5
⊢ (𝑢 = 𝑦 → ((𝑥𝐻𝑢) = 𝑥 ↔ (𝑥𝐻𝑦) = 𝑥)) |
30 | 27, 29 | anbi12d 743 |
. . . 4
⊢ (𝑢 = 𝑦 → (((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥))) |
31 | 30 | ralbidv 2969 |
. . 3
⊢ (𝑢 = 𝑦 → (∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥))) |
32 | 31 | reu4 3367 |
. 2
⊢
(∃!𝑢 ∈
𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ↔ (∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑢 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥) ∧ ∀𝑥 ∈ 𝑋 ((𝑦𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑦) = 𝑥)) → 𝑢 = 𝑦))) |
33 | 25, 32 | sylibr 223 |
1
⊢ (𝑅 ∈ RingOps →
∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑢) = 𝑥)) |