Step | Hyp | Ref
| Expression |
1 | | df-br 5075 |
. . . . 5
⊢ (𝐺DivRingOps𝐻 ↔ 〈𝐺, 𝐻〉 ∈ DivRingOps) |
2 | | df-drngo 36107 |
. . . . . . 7
⊢
DivRingOps = {〈𝑥, 𝑦〉 ∣ (〈𝑥, 𝑦〉 ∈ RingOps ∧ (𝑦 ↾ ((ran 𝑥 ∖ {(GId‘𝑥)}) × (ran 𝑥 ∖ {(GId‘𝑥)}))) ∈
GrpOp)} |
3 | 2 | relopabiv 5730 |
. . . . . 6
⊢ Rel
DivRingOps |
4 | 3 | brrelex1i 5643 |
. . . . 5
⊢ (𝐺DivRingOps𝐻 → 𝐺 ∈ V) |
5 | 1, 4 | sylbir 234 |
. . . 4
⊢
(〈𝐺, 𝐻〉 ∈ DivRingOps →
𝐺 ∈
V) |
6 | 5 | anim1i 615 |
. . 3
⊢
((〈𝐺, 𝐻〉 ∈ DivRingOps ∧
𝐻 ∈ 𝐴) → (𝐺 ∈ V ∧ 𝐻 ∈ 𝐴)) |
7 | 6 | ancoms 459 |
. 2
⊢ ((𝐻 ∈ 𝐴 ∧ 〈𝐺, 𝐻〉 ∈ DivRingOps) → (𝐺 ∈ V ∧ 𝐻 ∈ 𝐴)) |
8 | | rngoablo2 36067 |
. . . . 5
⊢
(〈𝐺, 𝐻〉 ∈ RingOps →
𝐺 ∈
AbelOp) |
9 | | elex 3450 |
. . . . 5
⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ V) |
10 | 8, 9 | syl 17 |
. . . 4
⊢
(〈𝐺, 𝐻〉 ∈ RingOps →
𝐺 ∈
V) |
11 | 10 | ad2antrl 725 |
. . 3
⊢ ((𝐻 ∈ 𝐴 ∧ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) → 𝐺 ∈ V) |
12 | | simpl 483 |
. . 3
⊢ ((𝐻 ∈ 𝐴 ∧ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) → 𝐻 ∈ 𝐴) |
13 | 11, 12 | jca 512 |
. 2
⊢ ((𝐻 ∈ 𝐴 ∧ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) → (𝐺 ∈ V ∧ 𝐻 ∈ 𝐴)) |
14 | | df-drngo 36107 |
. . . 4
⊢
DivRingOps = {〈𝑔, ℎ〉 ∣ (〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} |
15 | 14 | eleq2i 2830 |
. . 3
⊢
(〈𝐺, 𝐻〉 ∈ DivRingOps ↔
〈𝐺, 𝐻〉 ∈ {〈𝑔, ℎ〉 ∣ (〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}) |
16 | | opeq1 4804 |
. . . . . 6
⊢ (𝑔 = 𝐺 → 〈𝑔, ℎ〉 = 〈𝐺, ℎ〉) |
17 | 16 | eleq1d 2823 |
. . . . 5
⊢ (𝑔 = 𝐺 → (〈𝑔, ℎ〉 ∈ RingOps ↔ 〈𝐺, ℎ〉 ∈ RingOps)) |
18 | | rneq 5845 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺) |
19 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (GId‘𝑔) = (GId‘𝐺)) |
20 | 19 | sneqd 4573 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → {(GId‘𝑔)} = {(GId‘𝐺)}) |
21 | 18, 20 | difeq12d 4058 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (ran 𝑔 ∖ {(GId‘𝑔)}) = (ran 𝐺 ∖ {(GId‘𝐺)})) |
22 | 21 | sqxpeqd 5621 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)})) = ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) |
23 | 22 | reseq2d 5891 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) = (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)})))) |
24 | 23 | eleq1d 2823 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp ↔ (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) |
25 | 17, 24 | anbi12d 631 |
. . . 4
⊢ (𝑔 = 𝐺 → ((〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp) ↔ (〈𝐺, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) |
26 | | opeq2 4805 |
. . . . . 6
⊢ (ℎ = 𝐻 → 〈𝐺, ℎ〉 = 〈𝐺, 𝐻〉) |
27 | 26 | eleq1d 2823 |
. . . . 5
⊢ (ℎ = 𝐻 → (〈𝐺, ℎ〉 ∈ RingOps ↔ 〈𝐺, 𝐻〉 ∈ RingOps)) |
28 | | reseq1 5885 |
. . . . . 6
⊢ (ℎ = 𝐻 → (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) = (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)})))) |
29 | 28 | eleq1d 2823 |
. . . . 5
⊢ (ℎ = 𝐻 → ((ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp ↔ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) |
30 | 27, 29 | anbi12d 631 |
. . . 4
⊢ (ℎ = 𝐻 → ((〈𝐺, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp) ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) |
31 | 25, 30 | opelopabg 5451 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ 𝐴) → (〈𝐺, 𝐻〉 ∈ {〈𝑔, ℎ〉 ∣ (〈𝑔, ℎ〉 ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) |
32 | 15, 31 | syl5bb 283 |
. 2
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ 𝐴) → (〈𝐺, 𝐻〉 ∈ DivRingOps ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) |
33 | 7, 13, 32 | pm5.21nd 799 |
1
⊢ (𝐻 ∈ 𝐴 → (〈𝐺, 𝐻〉 ∈ DivRingOps ↔ (〈𝐺, 𝐻〉 ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp))) |