Step | Hyp | Ref
| Expression |
1 | | df-drngo 32918 |
. . . 4
⊢
DivRingOps = {〈𝑔, ℎ〉 ∣ (〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} |
2 | 1 | relopabi 5167 |
. . 3
⊢ Rel
DivRingOps |
3 | | 1st2nd 7105 |
. . 3
⊢ ((Rel
DivRingOps ∧ 𝑅 ∈
DivRingOps) → 𝑅 =
〈(1st ‘𝑅), (2nd ‘𝑅)〉) |
4 | 2, 3 | mpan 702 |
. 2
⊢ (𝑅 ∈ DivRingOps → 𝑅 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉) |
5 | | relrngo 32865 |
. . . 4
⊢ Rel
RingOps |
6 | | 1st2nd 7105 |
. . . 4
⊢ ((Rel
RingOps ∧ 𝑅 ∈
RingOps) → 𝑅 =
〈(1st ‘𝑅), (2nd ‘𝑅)〉) |
7 | 5, 6 | mpan 702 |
. . 3
⊢ (𝑅 ∈ RingOps → 𝑅 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉) |
8 | 7 | adantr 480 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑅 = 〈(1st ‘𝑅), (2nd ‘𝑅)〉) |
9 | | isdivrng1.1 |
. . . . 5
⊢ 𝐺 = (1st ‘𝑅) |
10 | | isdivrng1.2 |
. . . . 5
⊢ 𝐻 = (2nd ‘𝑅) |
11 | 9, 10 | opeq12i 4345 |
. . . 4
⊢
〈𝐺, 𝐻〉 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉 |
12 | 11 | eqeq2i 2622 |
. . 3
⊢ (𝑅 = 〈𝐺, 𝐻〉 ↔ 𝑅 = 〈(1st ‘𝑅), (2nd ‘𝑅)〉) |
13 | | fvex 6113 |
. . . . . . 7
⊢
(2nd ‘𝑅) ∈ V |
14 | 10, 13 | eqeltri 2684 |
. . . . . 6
⊢ 𝐻 ∈ V |
15 | | isdivrngo 32919 |
. . . . . 6
⊢ (𝐻 ∈ V → (〈𝐺, 𝐻〉 ∈ DivRingOps ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) |
16 | 14, 15 | ax-mp 5 |
. . . . 5
⊢
(〈𝐺, 𝐻〉 ∈ DivRingOps ↔
(〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) |
17 | | isdivrng1.4 |
. . . . . . . . . 10
⊢ 𝑋 = ran 𝐺 |
18 | | isdivrng1.3 |
. . . . . . . . . . 11
⊢ 𝑍 = (GId‘𝐺) |
19 | 18 | sneqi 4136 |
. . . . . . . . . 10
⊢ {𝑍} = {(GId‘𝐺)} |
20 | 17, 19 | difeq12i 3688 |
. . . . . . . . 9
⊢ (𝑋 ∖ {𝑍}) = (ran 𝐺 ∖ {(GId‘𝐺)}) |
21 | 20, 20 | xpeq12i 5061 |
. . . . . . . 8
⊢ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) = ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)})) |
22 | 21 | reseq2i 5314 |
. . . . . . 7
⊢ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) |
23 | 22 | eleq1i 2679 |
. . . . . 6
⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ↔ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp) |
24 | 23 | anbi2i 726 |
. . . . 5
⊢
((〈𝐺, 𝐻〉 ∈ RingOps ∧
(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) |
25 | 16, 24 | bitr4i 266 |
. . . 4
⊢
(〈𝐺, 𝐻〉 ∈ DivRingOps ↔
(〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) |
26 | | eleq1 2676 |
. . . . 5
⊢ (𝑅 = 〈𝐺, 𝐻〉 → (𝑅 ∈ DivRingOps ↔ 〈𝐺, 𝐻〉 ∈ DivRingOps)) |
27 | | eleq1 2676 |
. . . . . 6
⊢ (𝑅 = 〈𝐺, 𝐻〉 → (𝑅 ∈ RingOps ↔ 〈𝐺, 𝐻〉 ∈ RingOps)) |
28 | 27 | anbi1d 737 |
. . . . 5
⊢ (𝑅 = 〈𝐺, 𝐻〉 → ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) |
29 | 26, 28 | bibi12d 334 |
. . . 4
⊢ (𝑅 = 〈𝐺, 𝐻〉 → ((𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) ↔ (〈𝐺, 𝐻〉 ∈ DivRingOps ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))) |
30 | 25, 29 | mpbiri 247 |
. . 3
⊢ (𝑅 = 〈𝐺, 𝐻〉 → (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) |
31 | 12, 30 | sylbir 224 |
. 2
⊢ (𝑅 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉 →
(𝑅 ∈ DivRingOps ↔
(𝑅 ∈ RingOps ∧
(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) |
32 | 4, 8, 31 | pm5.21nii 367 |
1
⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) |