| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-br 5143 | . . . . 5
⊢ (𝐺DivRingOps𝐻 ↔ 〈𝐺, 𝐻〉 ∈ DivRingOps) | 
| 2 |  | df-drngo 37957 | . . . . . . 7
⊢
DivRingOps = {〈𝑥, 𝑦〉 ∣ (〈𝑥, 𝑦〉 ∈ RingOps ∧ (𝑦 ↾ ((ran 𝑥 ∖ {(GId‘𝑥)}) × (ran 𝑥 ∖ {(GId‘𝑥)}))) ∈
GrpOp)} | 
| 3 | 2 | relopabiv 5829 | . . . . . 6
⊢ Rel
DivRingOps | 
| 4 | 3 | brrelex1i 5740 | . . . . 5
⊢ (𝐺DivRingOps𝐻 → 𝐺 ∈ V) | 
| 5 | 1, 4 | sylbir 235 | . . . 4
⊢
(〈𝐺, 𝐻〉 ∈ DivRingOps →
𝐺 ∈
V) | 
| 6 | 5 | anim1i 615 | . . 3
⊢
((〈𝐺, 𝐻〉 ∈ DivRingOps ∧
𝐻 ∈ 𝐴) → (𝐺 ∈ V ∧ 𝐻 ∈ 𝐴)) | 
| 7 | 6 | ancoms 458 | . 2
⊢ ((𝐻 ∈ 𝐴 ∧ 〈𝐺, 𝐻〉 ∈ DivRingOps) → (𝐺 ∈ V ∧ 𝐻 ∈ 𝐴)) | 
| 8 |  | rngoablo2 37917 | . . . . 5
⊢
(〈𝐺, 𝐻〉 ∈ RingOps →
𝐺 ∈
AbelOp) | 
| 9 |  | elex 3500 | . . . . 5
⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ V) | 
| 10 | 8, 9 | syl 17 | . . . 4
⊢
(〈𝐺, 𝐻〉 ∈ RingOps →
𝐺 ∈
V) | 
| 11 | 10 | ad2antrl 728 | . . 3
⊢ ((𝐻 ∈ 𝐴 ∧ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) → 𝐺 ∈ V) | 
| 12 |  | simpl 482 | . . 3
⊢ ((𝐻 ∈ 𝐴 ∧ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) → 𝐻 ∈ 𝐴) | 
| 13 | 11, 12 | jca 511 | . 2
⊢ ((𝐻 ∈ 𝐴 ∧ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) → (𝐺 ∈ V ∧ 𝐻 ∈ 𝐴)) | 
| 14 |  | df-drngo 37957 | . . . 4
⊢
DivRingOps = {〈𝑔, ℎ〉 ∣ (〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} | 
| 15 | 14 | eleq2i 2832 | . . 3
⊢
(〈𝐺, 𝐻〉 ∈ DivRingOps ↔
〈𝐺, 𝐻〉 ∈ {〈𝑔, ℎ〉 ∣ (〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}) | 
| 16 |  | opeq1 4872 | . . . . . 6
⊢ (𝑔 = 𝐺 → 〈𝑔, ℎ〉 = 〈𝐺, ℎ〉) | 
| 17 | 16 | eleq1d 2825 | . . . . 5
⊢ (𝑔 = 𝐺 → (〈𝑔, ℎ〉 ∈ RingOps ↔ 〈𝐺, ℎ〉 ∈ RingOps)) | 
| 18 |  | rneq 5946 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺) | 
| 19 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (GId‘𝑔) = (GId‘𝐺)) | 
| 20 | 19 | sneqd 4637 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → {(GId‘𝑔)} = {(GId‘𝐺)}) | 
| 21 | 18, 20 | difeq12d 4126 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (ran 𝑔 ∖ {(GId‘𝑔)}) = (ran 𝐺 ∖ {(GId‘𝐺)})) | 
| 22 | 21 | sqxpeqd 5716 | . . . . . . 7
⊢ (𝑔 = 𝐺 → ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)})) = ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) | 
| 23 | 22 | reseq2d 5996 | . . . . . 6
⊢ (𝑔 = 𝐺 → (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) = (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)})))) | 
| 24 | 23 | eleq1d 2825 | . . . . 5
⊢ (𝑔 = 𝐺 → ((ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp ↔ (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) | 
| 25 | 17, 24 | anbi12d 632 | . . . 4
⊢ (𝑔 = 𝐺 → ((〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp) ↔ (〈𝐺, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) | 
| 26 |  | opeq2 4873 | . . . . . 6
⊢ (ℎ = 𝐻 → 〈𝐺, ℎ〉 = 〈𝐺, 𝐻〉) | 
| 27 | 26 | eleq1d 2825 | . . . . 5
⊢ (ℎ = 𝐻 → (〈𝐺, ℎ〉 ∈ RingOps ↔ 〈𝐺, 𝐻〉 ∈ RingOps)) | 
| 28 |  | reseq1 5990 | . . . . . 6
⊢ (ℎ = 𝐻 → (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) = (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)})))) | 
| 29 | 28 | eleq1d 2825 | . . . . 5
⊢ (ℎ = 𝐻 → ((ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp ↔ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) | 
| 30 | 27, 29 | anbi12d 632 | . . . 4
⊢ (ℎ = 𝐻 → ((〈𝐺, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp) ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) | 
| 31 | 25, 30 | opelopabg 5542 | . . 3
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ 𝐴) → (〈𝐺, 𝐻〉 ∈ {〈𝑔, ℎ〉 ∣ (〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) | 
| 32 | 15, 31 | bitrid 283 | . 2
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ 𝐴) → (〈𝐺, 𝐻〉 ∈ DivRingOps ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) | 
| 33 | 7, 13, 32 | pm5.21nd 801 | 1
⊢ (𝐻 ∈ 𝐴 → (〈𝐺, 𝐻〉 ∈ DivRingOps ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) |