Step | Hyp | Ref
| Expression |
1 | | df-br 5110 |
. . . . 5
⊢ (𝐺DivRingOps𝐻 ↔ ⟨𝐺, 𝐻⟩ ∈ DivRingOps) |
2 | | df-drngo 36458 |
. . . . . . 7
⊢
DivRingOps = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ RingOps ∧ (𝑦 ↾ ((ran 𝑥 ∖ {(GId‘𝑥)}) × (ran 𝑥 ∖ {(GId‘𝑥)}))) ∈
GrpOp)} |
3 | 2 | relopabiv 5780 |
. . . . . 6
⊢ Rel
DivRingOps |
4 | 3 | brrelex1i 5692 |
. . . . 5
⊢ (𝐺DivRingOps𝐻 → 𝐺 ∈ V) |
5 | 1, 4 | sylbir 234 |
. . . 4
⊢
(⟨𝐺, 𝐻⟩ ∈ DivRingOps →
𝐺 ∈
V) |
6 | 5 | anim1i 616 |
. . 3
⊢
((⟨𝐺, 𝐻⟩ ∈ DivRingOps ∧
𝐻 ∈ 𝐴) → (𝐺 ∈ V ∧ 𝐻 ∈ 𝐴)) |
7 | 6 | ancoms 460 |
. 2
⊢ ((𝐻 ∈ 𝐴 ∧ ⟨𝐺, 𝐻⟩ ∈ DivRingOps) → (𝐺 ∈ V ∧ 𝐻 ∈ 𝐴)) |
8 | | rngoablo2 36418 |
. . . . 5
⊢
(⟨𝐺, 𝐻⟩ ∈ RingOps →
𝐺 ∈
AbelOp) |
9 | | elex 3465 |
. . . . 5
⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ V) |
10 | 8, 9 | syl 17 |
. . . 4
⊢
(⟨𝐺, 𝐻⟩ ∈ RingOps →
𝐺 ∈
V) |
11 | 10 | ad2antrl 727 |
. . 3
⊢ ((𝐻 ∈ 𝐴 ∧ (⟨𝐺, 𝐻⟩ ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) → 𝐺 ∈ V) |
12 | | simpl 484 |
. . 3
⊢ ((𝐻 ∈ 𝐴 ∧ (⟨𝐺, 𝐻⟩ ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) → 𝐻 ∈ 𝐴) |
13 | 11, 12 | jca 513 |
. 2
⊢ ((𝐻 ∈ 𝐴 ∧ (⟨𝐺, 𝐻⟩ ∈ RingOps ∧ (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) ∈ GrpOp)) → (𝐺 ∈ V ∧ 𝐻 ∈ 𝐴)) |
14 | | df-drngo 36458 |
. . . 4
⊢
DivRingOps = {⟨𝑔, ℎ⟩ ∣ (⟨𝑔, ℎ⟩ ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} |
15 | 14 | eleq2i 2826 |
. . 3
⊢
(⟨𝐺, 𝐻⟩ ∈ DivRingOps ↔
⟨𝐺, 𝐻⟩ ∈ {⟨𝑔, ℎ⟩ ∣ (⟨𝑔, ℎ⟩ ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}) |
16 | | opeq1 4834 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ⟨𝑔, ℎ⟩ = ⟨𝐺, ℎ⟩) |
17 | 16 | eleq1d 2819 |
. . . . 5
⊢ (𝑔 = 𝐺 → (⟨𝑔, ℎ⟩ ∈ RingOps ↔ ⟨𝐺, ℎ⟩ ∈ RingOps)) |
18 | | rneq 5895 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺) |
19 | | fveq2 6846 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (GId‘𝑔) = (GId‘𝐺)) |
20 | 19 | sneqd 4602 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → {(GId‘𝑔)} = {(GId‘𝐺)}) |
21 | 18, 20 | difeq12d 4087 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (ran 𝑔 ∖ {(GId‘𝑔)}) = (ran 𝐺 ∖ {(GId‘𝐺)})) |
22 | 21 | sqxpeqd 5669 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)})) = ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) |
23 | 22 | reseq2d 5941 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) = (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)})))) |
24 | 23 | eleq1d 2819 |
. . . . 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 4835 |
. . . . . 6
⊢ (ℎ = 𝐻 → ⟨𝐺, ℎ⟩ = ⟨𝐺, 𝐻⟩) |
27 | 26 | eleq1d 2819 |
. . . . 5
⊢ (ℎ = 𝐻 → (⟨𝐺, ℎ⟩ ∈ RingOps ↔ ⟨𝐺, 𝐻⟩ ∈ RingOps)) |
28 | | reseq1 5935 |
. . . . . 6
⊢ (ℎ = 𝐻 → (ℎ ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)}))) = (𝐻 ↾ ((ran 𝐺 ∖ {(GId‘𝐺)}) × (ran 𝐺 ∖ {(GId‘𝐺)})))) |
29 | 28 | eleq1d 2819 |
. . . . 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 5499 |
. . 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))) |