Step | Hyp | Ref
| Expression |
1 | | opeq1 4834 |
. . . . . 6
⊢ (𝑔 = (1st ‘𝑅) → ⟨𝑔, ℎ⟩ = ⟨(1st ‘𝑅), ℎ⟩) |
2 | 1 | eleq1d 2819 |
. . . . 5
⊢ (𝑔 = (1st ‘𝑅) → (⟨𝑔, ℎ⟩ ∈ RingOps ↔
⟨(1st ‘𝑅), ℎ⟩ ∈ RingOps)) |
3 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑔 = (1st ‘𝑅) → 𝑔 = (1st ‘𝑅)) |
4 | | drngi.1 |
. . . . . . . . . . . 12
⊢ 𝐺 = (1st ‘𝑅) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . . . . . . 11
⊢ (𝑔 = (1st ‘𝑅) → 𝑔 = 𝐺) |
6 | 5 | rneqd 5897 |
. . . . . . . . . 10
⊢ (𝑔 = (1st ‘𝑅) → ran 𝑔 = ran 𝐺) |
7 | | drngi.3 |
. . . . . . . . . 10
⊢ 𝑋 = ran 𝐺 |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝑔 = (1st ‘𝑅) → ran 𝑔 = 𝑋) |
9 | 5 | fveq2d 6850 |
. . . . . . . . . . 11
⊢ (𝑔 = (1st ‘𝑅) → (GId‘𝑔) = (GId‘𝐺)) |
10 | | drngi.4 |
. . . . . . . . . . 11
⊢ 𝑍 = (GId‘𝐺) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . . . . 10
⊢ (𝑔 = (1st ‘𝑅) → (GId‘𝑔) = 𝑍) |
12 | 11 | sneqd 4602 |
. . . . . . . . 9
⊢ (𝑔 = (1st ‘𝑅) → {(GId‘𝑔)} = {𝑍}) |
13 | 8, 12 | difeq12d 4087 |
. . . . . . . 8
⊢ (𝑔 = (1st ‘𝑅) → (ran 𝑔 ∖ {(GId‘𝑔)}) = (𝑋 ∖ {𝑍})) |
14 | 13 | sqxpeqd 5669 |
. . . . . . 7
⊢ (𝑔 = (1st ‘𝑅) → ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)})) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) |
15 | 14 | reseq2d 5941 |
. . . . . 6
⊢ (𝑔 = (1st ‘𝑅) → (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) = (ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) |
16 | 15 | eleq1d 2819 |
. . . . 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 4835 |
. . . . . . 7
⊢ (ℎ = (2nd ‘𝑅) → ⟨(1st
‘𝑅), ℎ⟩ = ⟨(1st
‘𝑅), (2nd
‘𝑅)⟩) |
19 | 18 | eleq1d 2819 |
. . . . . 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 2792 |
. . . . . . . 8
⊢ (ℎ = (2nd ‘𝑅) → 𝐻 = ℎ) |
24 | 23 | reseq1d 5940 |
. . . . . . 7
⊢ (ℎ = (2nd ‘𝑅) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (ℎ ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) |
25 | 24 | eleq1d 2819 |
. . . . . 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 7998 |
. . 3
⊢ (𝑅 ∈ {⟨𝑔, ℎ⟩ ∣ (⟨𝑔, ℎ⟩ ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} →
(⟨(1st ‘𝑅), (2nd ‘𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) |
29 | | df-drngo 36458 |
. . 3
⊢
DivRingOps = {⟨𝑔, ℎ⟩ ∣ (⟨𝑔, ℎ⟩ ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)} |
30 | 28, 29 | eleq2s 2852 |
. 2
⊢ (𝑅 ∈ DivRingOps →
(⟨(1st ‘𝑅), (2nd ‘𝑅)⟩ ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)) |
31 | 29 | relopabiv 5780 |
. . . . 5
⊢ Rel
DivRingOps |
32 | | 1st2nd 7975 |
. . . . 5
⊢ ((Rel
DivRingOps ∧ 𝑅 ∈
DivRingOps) → 𝑅 =
⟨(1st ‘𝑅), (2nd ‘𝑅)⟩) |
33 | 31, 32 | mpan 689 |
. . . 4
⊢ (𝑅 ∈ DivRingOps → 𝑅 = ⟨(1st
‘𝑅), (2nd
‘𝑅)⟩) |
34 | 33 | eleq1d 2819 |
. . 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)) |