| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | opeq1 4872 | . . . . . 6
⊢ (𝑔 = (1st ‘𝑅) → 〈𝑔, ℎ〉 = 〈(1st ‘𝑅), ℎ〉) | 
| 2 | 1 | eleq1d 2825 | . . . . 5
⊢ (𝑔 = (1st ‘𝑅) → (〈𝑔, ℎ〉 ∈ RingOps ↔
〈(1st ‘𝑅), ℎ〉 ∈ RingOps)) | 
| 3 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑔 = (1st ‘𝑅) → 𝑔 = (1st ‘𝑅)) | 
| 4 |  | drngi.1 | . . . . . . . . . . . 12
⊢ 𝐺 = (1st ‘𝑅) | 
| 5 | 3, 4 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑔 = (1st ‘𝑅) → 𝑔 = 𝐺) | 
| 6 | 5 | rneqd 5948 | . . . . . . . . . 10
⊢ (𝑔 = (1st ‘𝑅) → ran 𝑔 = ran 𝐺) | 
| 7 |  | drngi.3 | . . . . . . . . . 10
⊢ 𝑋 = ran 𝐺 | 
| 8 | 6, 7 | eqtr4di 2794 | . . . . . . . . 9
⊢ (𝑔 = (1st ‘𝑅) → ran 𝑔 = 𝑋) | 
| 9 | 5 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑔 = (1st ‘𝑅) → (GId‘𝑔) = (GId‘𝐺)) | 
| 10 |  | drngi.4 | . . . . . . . . . . 11
⊢ 𝑍 = (GId‘𝐺) | 
| 11 | 9, 10 | eqtr4di 2794 | . . . . . . . . . 10
⊢ (𝑔 = (1st ‘𝑅) → (GId‘𝑔) = 𝑍) | 
| 12 | 11 | sneqd 4637 | . . . . . . . . 9
⊢ (𝑔 = (1st ‘𝑅) → {(GId‘𝑔)} = {𝑍}) | 
| 13 | 8, 12 | difeq12d 4126 | . . . . . . . 8
⊢ (𝑔 = (1st ‘𝑅) → (ran 𝑔 ∖ {(GId‘𝑔)}) = (𝑋 ∖ {𝑍})) | 
| 14 | 13 | sqxpeqd 5716 | . . . . . . 7
⊢ (𝑔 = (1st ‘𝑅) → ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)})) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) | 
| 15 | 14 | reseq2d 5996 | . . . . . 6
⊢ (𝑔 = (1st ‘𝑅) → (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) = (ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) | 
| 16 | 15 | eleq1d 2825 | . . . . 5
⊢ (𝑔 = (1st ‘𝑅) → ((ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp ↔ (ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) | 
| 17 | 2, 16 | anbi12d 632 | . . . 4
⊢ (𝑔 = (1st ‘𝑅) → ((〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp) ↔
(〈(1st ‘𝑅), ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) | 
| 18 |  | opeq2 4873 | . . . . . . 7
⊢ (ℎ = (2nd ‘𝑅) → 〈(1st
‘𝑅), ℎ〉 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉) | 
| 19 | 18 | eleq1d 2825 | . . . . . 6
⊢ (ℎ = (2nd ‘𝑅) → (〈(1st
‘𝑅), ℎ〉 ∈ RingOps ↔
〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ RingOps)) | 
| 20 | 19 | anbi1d 631 | . . . . 5
⊢ (ℎ = (2nd ‘𝑅) → ((〈(1st
‘𝑅), ℎ〉 ∈ RingOps ∧
(ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔
(〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ RingOps ∧ (ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) | 
| 21 |  | drngi.2 | . . . . . . . . 9
⊢ 𝐻 = (2nd ‘𝑅) | 
| 22 |  | id 22 | . . . . . . . . 9
⊢ (ℎ = (2nd ‘𝑅) → ℎ = (2nd ‘𝑅)) | 
| 23 | 21, 22 | eqtr4id 2795 | . . . . . . . 8
⊢ (ℎ = (2nd ‘𝑅) → 𝐻 = ℎ) | 
| 24 | 23 | reseq1d 5995 | . . . . . . 7
⊢ (ℎ = (2nd ‘𝑅) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) | 
| 25 | 24 | eleq1d 2825 | . . . . . 6
⊢ (ℎ = (2nd ‘𝑅) → ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ↔ (ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) | 
| 26 | 25 | anbi2d 630 | . . . . 5
⊢ (ℎ = (2nd ‘𝑅) → ((〈(1st
‘𝑅), (2nd
‘𝑅)〉 ∈
RingOps ∧ (𝐻 ↾
((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔
(〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ RingOps ∧ (ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) | 
| 27 | 20, 26 | bitr4d 282 | . . . 4
⊢ (ℎ = (2nd ‘𝑅) → ((〈(1st
‘𝑅), ℎ〉 ∈ RingOps ∧
(ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔
(〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) | 
| 28 | 17, 27 | elopabi 8088 | . . 3
⊢ (𝑅 ∈ {〈𝑔, ℎ〉 ∣ (〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} →
(〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) | 
| 29 |  | df-drngo 37957 | . . 3
⊢
DivRingOps = {〈𝑔, ℎ〉 ∣ (〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} | 
| 30 | 28, 29 | eleq2s 2858 | . 2
⊢ (𝑅 ∈ DivRingOps →
(〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) | 
| 31 | 29 | relopabiv 5829 | . . . . 5
⊢ Rel
DivRingOps | 
| 32 |  | 1st2nd 8065 | . . . . 5
⊢ ((Rel
DivRingOps ∧ 𝑅 ∈
DivRingOps) → 𝑅 =
〈(1st ‘𝑅), (2nd ‘𝑅)〉) | 
| 33 | 31, 32 | mpan 690 | . . . 4
⊢ (𝑅 ∈ DivRingOps → 𝑅 = 〈(1st
‘𝑅), (2nd
‘𝑅)〉) | 
| 34 | 33 | eleq1d 2825 | . . 3
⊢ (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ↔
〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ RingOps)) | 
| 35 | 34 | anbi1d 631 | . 2
⊢ (𝑅 ∈ DivRingOps →
((𝑅 ∈ RingOps ∧
(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔
(〈(1st ‘𝑅), (2nd ‘𝑅)〉 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))) | 
| 36 | 30, 35 | mpbird 257 | 1
⊢ (𝑅 ∈ DivRingOps → (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) |