Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
⊢
(1st ‘𝑅) = (1st ‘𝑅) |
2 | | unmnd.1 |
. . . 4
⊢ 𝐻 = (2nd ‘𝑅) |
3 | | eqid 2737 |
. . . 4
⊢ ran
(1st ‘𝑅) =
ran (1st ‘𝑅) |
4 | 1, 2, 3 | rngosm 35800 |
. . 3
⊢ (𝑅 ∈ RingOps → 𝐻:(ran (1st
‘𝑅) × ran
(1st ‘𝑅))⟶ran (1st ‘𝑅)) |
5 | 1, 2, 3 | rngoass 35806 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ (𝑥 ∈ ran (1st
‘𝑅) ∧ 𝑦 ∈ ran (1st
‘𝑅) ∧ 𝑧 ∈ ran (1st
‘𝑅))) → ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))) |
6 | 5 | ralrimivvva 3113 |
. . 3
⊢ (𝑅 ∈ RingOps →
∀𝑥 ∈ ran
(1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)∀𝑧 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))) |
7 | 1, 2, 3 | rngoi 35799 |
. . . 4
⊢ (𝑅 ∈ RingOps →
(((1st ‘𝑅)
∈ AbelOp ∧ 𝐻:(ran
(1st ‘𝑅)
× ran (1st ‘𝑅))⟶ran (1st ‘𝑅)) ∧ (∀𝑥 ∈ ran (1st
‘𝑅)∀𝑦 ∈ ran (1st
‘𝑅)∀𝑧 ∈ ran (1st
‘𝑅)(((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦(1st ‘𝑅)𝑧)) = ((𝑥𝐻𝑦)(1st ‘𝑅)(𝑥𝐻𝑧)) ∧ ((𝑥(1st ‘𝑅)𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)(1st ‘𝑅)(𝑦𝐻𝑧))) ∧ ∃𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))) |
8 | 7 | simprrd 774 |
. . 3
⊢ (𝑅 ∈ RingOps →
∃𝑥 ∈ ran
(1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)) |
9 | 2, 1 | rngorn1 35833 |
. . . 4
⊢ (𝑅 ∈ RingOps → ran
(1st ‘𝑅) =
dom dom 𝐻) |
10 | | xpid11 5806 |
. . . . . . . 8
⊢ ((dom dom
𝐻 × dom dom 𝐻) = (ran (1st
‘𝑅) × ran
(1st ‘𝑅))
↔ dom dom 𝐻 = ran
(1st ‘𝑅)) |
11 | 10 | biimpri 231 |
. . . . . . 7
⊢ (dom dom
𝐻 = ran (1st
‘𝑅) → (dom dom
𝐻 × dom dom 𝐻) = (ran (1st
‘𝑅) × ran
(1st ‘𝑅))) |
12 | | feq23 6534 |
. . . . . . 7
⊢ (((dom
dom 𝐻 × dom dom 𝐻) = (ran (1st
‘𝑅) × ran
(1st ‘𝑅))
∧ dom dom 𝐻 = ran
(1st ‘𝑅))
→ (𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ↔ 𝐻:(ran (1st ‘𝑅) × ran (1st
‘𝑅))⟶ran
(1st ‘𝑅))) |
13 | 11, 12 | mpancom 688 |
. . . . . 6
⊢ (dom dom
𝐻 = ran (1st
‘𝑅) → (𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ↔ 𝐻:(ran (1st ‘𝑅) × ran (1st
‘𝑅))⟶ran
(1st ‘𝑅))) |
14 | | raleq 3324 |
. . . . . . . 8
⊢ (dom dom
𝐻 = ran (1st
‘𝑅) →
(∀𝑧 ∈ dom dom
𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ↔ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)))) |
15 | 14 | raleqbi1dv 3322 |
. . . . . . 7
⊢ (dom dom
𝐻 = ran (1st
‘𝑅) →
(∀𝑦 ∈ dom dom
𝐻∀𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ↔ ∀𝑦 ∈ ran (1st ‘𝑅)∀𝑧 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)))) |
16 | 15 | raleqbi1dv 3322 |
. . . . . 6
⊢ (dom dom
𝐻 = ran (1st
‘𝑅) →
(∀𝑥 ∈ dom dom
𝐻∀𝑦 ∈ dom dom 𝐻∀𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ↔ ∀𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)∀𝑧 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)))) |
17 | | raleq 3324 |
. . . . . . 7
⊢ (dom dom
𝐻 = ran (1st
‘𝑅) →
(∀𝑦 ∈ dom dom
𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦) ↔ ∀𝑦 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))) |
18 | 17 | rexeqbi1dv 3323 |
. . . . . 6
⊢ (dom dom
𝐻 = ran (1st
‘𝑅) →
(∃𝑥 ∈ dom dom
𝐻∀𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦) ↔ ∃𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))) |
19 | 13, 16, 18 | 3anbi123d 1438 |
. . . . 5
⊢ (dom dom
𝐻 = ran (1st
‘𝑅) → ((𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻∀𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)) ↔ (𝐻:(ran (1st ‘𝑅) × ran (1st
‘𝑅))⟶ran
(1st ‘𝑅)
∧ ∀𝑥 ∈ ran
(1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)∀𝑧 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))) |
20 | 19 | eqcoms 2745 |
. . . 4
⊢ (ran
(1st ‘𝑅) =
dom dom 𝐻 → ((𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻∀𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)) ↔ (𝐻:(ran (1st ‘𝑅) × ran (1st
‘𝑅))⟶ran
(1st ‘𝑅)
∧ ∀𝑥 ∈ ran
(1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)∀𝑧 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))) |
21 | 9, 20 | syl 17 |
. . 3
⊢ (𝑅 ∈ RingOps → ((𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻∀𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)) ↔ (𝐻:(ran (1st ‘𝑅) × ran (1st
‘𝑅))⟶ran
(1st ‘𝑅)
∧ ∀𝑥 ∈ ran
(1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)∀𝑧 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ ran (1st ‘𝑅)∀𝑦 ∈ ran (1st ‘𝑅)((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))) |
22 | 4, 6, 8, 21 | mpbir3and 1344 |
. 2
⊢ (𝑅 ∈ RingOps → (𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻∀𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))) |
23 | | fvex 6735 |
. . . 4
⊢
(2nd ‘𝑅) ∈ V |
24 | | eleq1 2825 |
. . . 4
⊢ (𝐻 = (2nd ‘𝑅) → (𝐻 ∈ V ↔ (2nd
‘𝑅) ∈
V)) |
25 | 23, 24 | mpbiri 261 |
. . 3
⊢ (𝐻 = (2nd ‘𝑅) → 𝐻 ∈ V) |
26 | | eqid 2737 |
. . . 4
⊢ dom dom
𝐻 = dom dom 𝐻 |
27 | 26 | ismndo1 35773 |
. . 3
⊢ (𝐻 ∈ V → (𝐻 ∈ MndOp ↔ (𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻∀𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))) |
28 | 2, 25, 27 | mp2b 10 |
. 2
⊢ (𝐻 ∈ MndOp ↔ (𝐻:(dom dom 𝐻 × dom dom 𝐻)⟶dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻∀𝑧 ∈ dom dom 𝐻((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ ∃𝑥 ∈ dom dom 𝐻∀𝑦 ∈ dom dom 𝐻((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))) |
29 | 22, 28 | sylibr 237 |
1
⊢ (𝑅 ∈ RingOps → 𝐻 ∈ MndOp) |