Step | Hyp | Ref
| Expression |
1 | | on1el3.1 |
. . . . . . . . . 10
⊢ 𝐺 = (1st ‘𝑅) |
2 | 1 | rngogrpo 36415 |
. . . . . . . . 9
⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp) |
3 | | on1el3.2 |
. . . . . . . . . 10
⊢ 𝑋 = ran 𝐺 |
4 | 3 | grpofo 29483 |
. . . . . . . . 9
⊢ (𝐺 ∈ GrpOp → 𝐺:(𝑋 × 𝑋)–onto→𝑋) |
5 | | fof 6757 |
. . . . . . . . 9
⊢ (𝐺:(𝑋 × 𝑋)–onto→𝑋 → 𝐺:(𝑋 × 𝑋)⟶𝑋) |
6 | 2, 4, 5 | 3syl 18 |
. . . . . . . 8
⊢ (𝑅 ∈ RingOps → 𝐺:(𝑋 × 𝑋)⟶𝑋) |
7 | 6 | adantr 482 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → 𝐺:(𝑋 × 𝑋)⟶𝑋) |
8 | | id 22 |
. . . . . . . . 9
⊢ (𝑋 = {𝐴} → 𝑋 = {𝐴}) |
9 | 8 | sqxpeqd 5666 |
. . . . . . . 8
⊢ (𝑋 = {𝐴} → (𝑋 × 𝑋) = ({𝐴} × {𝐴})) |
10 | 9, 8 | feq23d 6664 |
. . . . . . 7
⊢ (𝑋 = {𝐴} → (𝐺:(𝑋 × 𝑋)⟶𝑋 ↔ 𝐺:({𝐴} × {𝐴})⟶{𝐴})) |
11 | 7, 10 | syl5ibcom 244 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} → 𝐺:({𝐴} × {𝐴})⟶{𝐴})) |
12 | 7 | fdmd 6680 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → dom 𝐺 = (𝑋 × 𝑋)) |
13 | 12 | eqcomd 2739 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 × 𝑋) = dom 𝐺) |
14 | | fdm 6678 |
. . . . . . . . 9
⊢ (𝐺:({𝐴} × {𝐴})⟶{𝐴} → dom 𝐺 = ({𝐴} × {𝐴})) |
15 | 14 | eqeq2d 2744 |
. . . . . . . 8
⊢ (𝐺:({𝐴} × {𝐴})⟶{𝐴} → ((𝑋 × 𝑋) = dom 𝐺 ↔ (𝑋 × 𝑋) = ({𝐴} × {𝐴}))) |
16 | 13, 15 | syl5ibcom 244 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝐺:({𝐴} × {𝐴})⟶{𝐴} → (𝑋 × 𝑋) = ({𝐴} × {𝐴}))) |
17 | | xpid11 5888 |
. . . . . . 7
⊢ ((𝑋 × 𝑋) = ({𝐴} × {𝐴}) ↔ 𝑋 = {𝐴}) |
18 | 16, 17 | syl6ib 251 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝐺:({𝐴} × {𝐴})⟶{𝐴} → 𝑋 = {𝐴})) |
19 | 11, 18 | impbid 211 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ 𝐺:({𝐴} × {𝐴})⟶{𝐴})) |
20 | | simpr 486 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵) |
21 | | xpsng 7086 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵) → ({𝐴} × {𝐴}) = {⟨𝐴, 𝐴⟩}) |
22 | 20, 21 | sylancom 589 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → ({𝐴} × {𝐴}) = {⟨𝐴, 𝐴⟩}) |
23 | 22 | feq2d 6655 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝐺:({𝐴} × {𝐴})⟶{𝐴} ↔ 𝐺:{⟨𝐴, 𝐴⟩}⟶{𝐴})) |
24 | | opex 5422 |
. . . . . 6
⊢
⟨𝐴, 𝐴⟩ ∈ V |
25 | | fsng 7084 |
. . . . . 6
⊢
((⟨𝐴, 𝐴⟩ ∈ V ∧ 𝐴 ∈ 𝐵) → (𝐺:{⟨𝐴, 𝐴⟩}⟶{𝐴} ↔ 𝐺 = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩})) |
26 | 24, 20, 25 | sylancr 588 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝐺:{⟨𝐴, 𝐴⟩}⟶{𝐴} ↔ 𝐺 = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩})) |
27 | 19, 23, 26 | 3bitrd 305 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ 𝐺 = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩})) |
28 | 1 | eqeq1i 2738 |
. . . 4
⊢ (𝐺 = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ↔ (1st ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}) |
29 | 27, 28 | bitrdi 287 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ (1st ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩})) |
30 | 29 | anbi1d 631 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → ((𝑋 = {𝐴} ∧ (2nd ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}) ↔ ((1st
‘𝑅) =
{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∧ (2nd ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}))) |
31 | | eqid 2733 |
. . . . . . 7
⊢
(2nd ‘𝑅) = (2nd ‘𝑅) |
32 | 1, 31, 3 | rngosm 36405 |
. . . . . 6
⊢ (𝑅 ∈ RingOps →
(2nd ‘𝑅):(𝑋 × 𝑋)⟶𝑋) |
33 | 32 | adantr 482 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (2nd ‘𝑅):(𝑋 × 𝑋)⟶𝑋) |
34 | 9, 8 | feq23d 6664 |
. . . . 5
⊢ (𝑋 = {𝐴} → ((2nd ‘𝑅):(𝑋 × 𝑋)⟶𝑋 ↔ (2nd ‘𝑅):({𝐴} × {𝐴})⟶{𝐴})) |
35 | 33, 34 | syl5ibcom 244 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} → (2nd ‘𝑅):({𝐴} × {𝐴})⟶{𝐴})) |
36 | 22 | feq2d 6655 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → ((2nd ‘𝑅):({𝐴} × {𝐴})⟶{𝐴} ↔ (2nd ‘𝑅):{⟨𝐴, 𝐴⟩}⟶{𝐴})) |
37 | | fsng 7084 |
. . . . . 6
⊢
((⟨𝐴, 𝐴⟩ ∈ V ∧ 𝐴 ∈ 𝐵) → ((2nd ‘𝑅):{⟨𝐴, 𝐴⟩}⟶{𝐴} ↔ (2nd ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩})) |
38 | 24, 20, 37 | sylancr 588 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → ((2nd ‘𝑅):{⟨𝐴, 𝐴⟩}⟶{𝐴} ↔ (2nd ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩})) |
39 | 36, 38 | bitrd 279 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → ((2nd ‘𝑅):({𝐴} × {𝐴})⟶{𝐴} ↔ (2nd ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩})) |
40 | 35, 39 | sylibd 238 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} → (2nd ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩})) |
41 | 40 | pm4.71d 563 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ (𝑋 = {𝐴} ∧ (2nd ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}))) |
42 | | relrngo 36401 |
. . . . . 6
⊢ Rel
RingOps |
43 | | df-rel 5641 |
. . . . . 6
⊢ (Rel
RingOps ↔ RingOps ⊆ (V × V)) |
44 | 42, 43 | mpbi 229 |
. . . . 5
⊢ RingOps
⊆ (V × V) |
45 | 44 | sseli 3941 |
. . . 4
⊢ (𝑅 ∈ RingOps → 𝑅 ∈ (V ×
V)) |
46 | 45 | adantr 482 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → 𝑅 ∈ (V × V)) |
47 | | eqop 7964 |
. . 3
⊢ (𝑅 ∈ (V × V) →
(𝑅 =
⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩ ↔ ((1st
‘𝑅) =
{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∧ (2nd ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}))) |
48 | 46, 47 | syl 17 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑅 = ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩ ↔ ((1st
‘𝑅) =
{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∧ (2nd ‘𝑅) = {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}))) |
49 | 30, 41, 48 | 3bitr4d 311 |
1
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ 𝑅 = ⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩)) |