| Step | Hyp | Ref
| Expression |
| 1 | | df-drngo 37956 |
. . . 4
⊢
DivRingOps = {〈𝑔, ℎ〉 ∣ (〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} |
| 2 | 1 | relopabiv 5830 |
. . 3
⊢ Rel
DivRingOps |
| 3 | | 1st2nd 8064 |
. . 3
⊢ ((Rel
DivRingOps ∧ 𝑅 ∈
DivRingOps) → 𝑅 =
〈(1st ‘𝑅), (2nd ‘𝑅)〉) |
| 4 | 2, 3 | mpan 690 |
. 2
⊢ (𝑅 ∈ DivRingOps → 𝑅 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉) |
| 5 | | relrngo 37903 |
. . . 4
⊢ Rel
RingOps |
| 6 | | 1st2nd 8064 |
. . . 4
⊢ ((Rel
RingOps ∧ 𝑅 ∈
RingOps) → 𝑅 =
〈(1st ‘𝑅), (2nd ‘𝑅)〉) |
| 7 | 5, 6 | mpan 690 |
. . 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 4878 |
. . . 4
⊢
〈𝐺, 𝐻〉 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉 |
| 12 | 11 | eqeq2i 2750 |
. . 3
⊢ (𝑅 = 〈𝐺, 𝐻〉 ↔ 𝑅 = 〈(1st ‘𝑅), (2nd ‘𝑅)〉) |
| 13 | 10 | fvexi 6920 |
. . . . . 6
⊢ 𝐻 ∈ V |
| 14 | | isdivrngo 37957 |
. . . . . 6
⊢ (𝐻 ∈ V → (〈𝐺, 𝐻〉 ∈ DivRingOps ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) |
| 15 | 13, 14 | ax-mp 5 |
. . . . 5
⊢
(〈𝐺, 𝐻〉 ∈ DivRingOps ↔
(〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) |
| 16 | | isdivrng1.4 |
. . . . . . . . . 10
⊢ 𝑋 = ran 𝐺 |
| 17 | | isdivrng1.3 |
. . . . . . . . . . 11
⊢ 𝑍 = (GId‘𝐺) |
| 18 | 17 | sneqi 4637 |
. . . . . . . . . 10
⊢ {𝑍} = {(GId‘𝐺)} |
| 19 | 16, 18 | difeq12i 4124 |
. . . . . . . . 9
⊢ (𝑋 ∖ {𝑍}) = (ran 𝐺 ∖ {(GId‘𝐺)}) |
| 20 | 19, 19 | xpeq12i 5713 |
. . . . . . . 8
⊢ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) = ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)})) |
| 21 | 20 | reseq2i 5994 |
. . . . . . 7
⊢ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) |
| 22 | 21 | eleq1i 2832 |
. . . . . 6
⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ↔ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp) |
| 23 | 22 | anbi2i 623 |
. . . . 5
⊢
((〈𝐺, 𝐻〉 ∈ RingOps ∧
(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) |
| 24 | 15, 23 | bitr4i 278 |
. . . 4
⊢
(〈𝐺, 𝐻〉 ∈ DivRingOps ↔
(〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) |
| 25 | | eleq1 2829 |
. . . . 5
⊢ (𝑅 = 〈𝐺, 𝐻〉 → (𝑅 ∈ DivRingOps ↔ 〈𝐺, 𝐻〉 ∈ DivRingOps)) |
| 26 | | eleq1 2829 |
. . . . . 6
⊢ (𝑅 = 〈𝐺, 𝐻〉 → (𝑅 ∈ RingOps ↔ 〈𝐺, 𝐻〉 ∈ RingOps)) |
| 27 | 26 | anbi1d 631 |
. . . . 5
⊢ (𝑅 = 〈𝐺, 𝐻〉 → ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) |
| 28 | 25, 27 | bibi12d 345 |
. . . 4
⊢ (𝑅 = 〈𝐺, 𝐻〉 → ((𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) ↔ (〈𝐺, 𝐻〉 ∈ DivRingOps ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)))) |
| 29 | 24, 28 | mpbiri 258 |
. . 3
⊢ (𝑅 = 〈𝐺, 𝐻〉 → (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) |
| 30 | 12, 29 | sylbir 235 |
. 2
⊢ (𝑅 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉 →
(𝑅 ∈ DivRingOps ↔
(𝑅 ∈ RingOps ∧
(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) |
| 31 | 4, 8, 30 | pm5.21nii 378 |
1
⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) |