Proof of Theorem rngosn3
Step | Hyp | Ref
| Expression |
1 | | on1el3.1 |
. . . . . . . . . 10
⊢ 𝐺 = (1st ‘𝑅) |
2 | 1 | rngogrpo 32879 |
. . . . . . . . 9
⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp) |
3 | | on1el3.2 |
. . . . . . . . . 10
⊢ 𝑋 = ran 𝐺 |
4 | 3 | grpofo 26737 |
. . . . . . . . 9
⊢ (𝐺 ∈ GrpOp → 𝐺:(𝑋 × 𝑋)–onto→𝑋) |
5 | | fof 6028 |
. . . . . . . . 9
⊢ (𝐺:(𝑋 × 𝑋)–onto→𝑋 → 𝐺:(𝑋 × 𝑋)⟶𝑋) |
6 | 2, 4, 5 | 3syl 18 |
. . . . . . . 8
⊢ (𝑅 ∈ RingOps → 𝐺:(𝑋 × 𝑋)⟶𝑋) |
7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → 𝐺:(𝑋 × 𝑋)⟶𝑋) |
8 | | id 22 |
. . . . . . . . 9
⊢ (𝑋 = {𝐴} → 𝑋 = {𝐴}) |
9 | 8 | sqxpeqd 5065 |
. . . . . . . 8
⊢ (𝑋 = {𝐴} → (𝑋 × 𝑋) = ({𝐴} × {𝐴})) |
10 | 9, 8 | feq23d 5953 |
. . . . . . 7
⊢ (𝑋 = {𝐴} → (𝐺:(𝑋 × 𝑋)⟶𝑋 ↔ 𝐺:({𝐴} × {𝐴})⟶{𝐴})) |
11 | 7, 10 | syl5ibcom 234 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} → 𝐺:({𝐴} × {𝐴})⟶{𝐴})) |
12 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝐺:(𝑋 × 𝑋)⟶𝑋 → dom 𝐺 = (𝑋 × 𝑋)) |
13 | 7, 12 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → dom 𝐺 = (𝑋 × 𝑋)) |
14 | 13 | eqcomd 2616 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 × 𝑋) = dom 𝐺) |
15 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝐺:({𝐴} × {𝐴})⟶{𝐴} → dom 𝐺 = ({𝐴} × {𝐴})) |
16 | 15 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝐺:({𝐴} × {𝐴})⟶{𝐴} → ((𝑋 × 𝑋) = dom 𝐺 ↔ (𝑋 × 𝑋) = ({𝐴} × {𝐴}))) |
17 | 14, 16 | syl5ibcom 234 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝐺:({𝐴} × {𝐴})⟶{𝐴} → (𝑋 × 𝑋) = ({𝐴} × {𝐴}))) |
18 | | xpid11 5268 |
. . . . . . 7
⊢ ((𝑋 × 𝑋) = ({𝐴} × {𝐴}) ↔ 𝑋 = {𝐴}) |
19 | 17, 18 | syl6ib 240 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝐺:({𝐴} × {𝐴})⟶{𝐴} → 𝑋 = {𝐴})) |
20 | 11, 19 | impbid 201 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ 𝐺:({𝐴} × {𝐴})⟶{𝐴})) |
21 | | simpr 476 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵) |
22 | | xpsng 6312 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵) → ({𝐴} × {𝐴}) = {〈𝐴, 𝐴〉}) |
23 | 21, 22 | sylancom 698 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → ({𝐴} × {𝐴}) = {〈𝐴, 𝐴〉}) |
24 | 23 | feq2d 5944 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝐺:({𝐴} × {𝐴})⟶{𝐴} ↔ 𝐺:{〈𝐴, 𝐴〉}⟶{𝐴})) |
25 | | opex 4859 |
. . . . . 6
⊢
〈𝐴, 𝐴〉 ∈ V |
26 | | fsng 6310 |
. . . . . 6
⊢
((〈𝐴, 𝐴〉 ∈ V ∧ 𝐴 ∈ 𝐵) → (𝐺:{〈𝐴, 𝐴〉}⟶{𝐴} ↔ 𝐺 = {〈〈𝐴, 𝐴〉, 𝐴〉})) |
27 | 25, 21, 26 | sylancr 694 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝐺:{〈𝐴, 𝐴〉}⟶{𝐴} ↔ 𝐺 = {〈〈𝐴, 𝐴〉, 𝐴〉})) |
28 | 20, 24, 27 | 3bitrd 293 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ 𝐺 = {〈〈𝐴, 𝐴〉, 𝐴〉})) |
29 | 1 | eqeq1i 2615 |
. . . 4
⊢ (𝐺 = {〈〈𝐴, 𝐴〉, 𝐴〉} ↔ (1st ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉}) |
30 | 28, 29 | syl6bb 275 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ (1st ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉})) |
31 | 30 | anbi1d 737 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → ((𝑋 = {𝐴} ∧ (2nd ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉}) ↔ ((1st
‘𝑅) =
{〈〈𝐴, 𝐴〉, 𝐴〉} ∧ (2nd ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉}))) |
32 | | eqid 2610 |
. . . . . . 7
⊢
(2nd ‘𝑅) = (2nd ‘𝑅) |
33 | 1, 32, 3 | rngosm 32869 |
. . . . . 6
⊢ (𝑅 ∈ RingOps →
(2nd ‘𝑅):(𝑋 × 𝑋)⟶𝑋) |
34 | 33 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (2nd ‘𝑅):(𝑋 × 𝑋)⟶𝑋) |
35 | 9, 8 | feq23d 5953 |
. . . . 5
⊢ (𝑋 = {𝐴} → ((2nd ‘𝑅):(𝑋 × 𝑋)⟶𝑋 ↔ (2nd ‘𝑅):({𝐴} × {𝐴})⟶{𝐴})) |
36 | 34, 35 | syl5ibcom 234 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} → (2nd ‘𝑅):({𝐴} × {𝐴})⟶{𝐴})) |
37 | 23 | feq2d 5944 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → ((2nd ‘𝑅):({𝐴} × {𝐴})⟶{𝐴} ↔ (2nd ‘𝑅):{〈𝐴, 𝐴〉}⟶{𝐴})) |
38 | | fsng 6310 |
. . . . . 6
⊢
((〈𝐴, 𝐴〉 ∈ V ∧ 𝐴 ∈ 𝐵) → ((2nd ‘𝑅):{〈𝐴, 𝐴〉}⟶{𝐴} ↔ (2nd ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉})) |
39 | 25, 21, 38 | sylancr 694 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → ((2nd ‘𝑅):{〈𝐴, 𝐴〉}⟶{𝐴} ↔ (2nd ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉})) |
40 | 37, 39 | bitrd 267 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → ((2nd ‘𝑅):({𝐴} × {𝐴})⟶{𝐴} ↔ (2nd ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉})) |
41 | 36, 40 | sylibd 228 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} → (2nd ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉})) |
42 | 41 | pm4.71d 664 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ (𝑋 = {𝐴} ∧ (2nd ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉}))) |
43 | | relrngo 32865 |
. . . . . 6
⊢ Rel
RingOps |
44 | | df-rel 5045 |
. . . . . 6
⊢ (Rel
RingOps ↔ RingOps ⊆ (V × V)) |
45 | 43, 44 | mpbi 219 |
. . . . 5
⊢ RingOps
⊆ (V × V) |
46 | 45 | sseli 3564 |
. . . 4
⊢ (𝑅 ∈ RingOps → 𝑅 ∈ (V ×
V)) |
47 | 46 | adantr 480 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → 𝑅 ∈ (V × V)) |
48 | | eqop 7099 |
. . 3
⊢ (𝑅 ∈ (V × V) →
(𝑅 =
〈{〈〈𝐴, 𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ↔ ((1st
‘𝑅) =
{〈〈𝐴, 𝐴〉, 𝐴〉} ∧ (2nd ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉}))) |
49 | 47, 48 | syl 17 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑅 = 〈{〈〈𝐴, 𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ↔ ((1st
‘𝑅) =
{〈〈𝐴, 𝐴〉, 𝐴〉} ∧ (2nd ‘𝑅) = {〈〈𝐴, 𝐴〉, 𝐴〉}))) |
50 | 31, 42, 49 | 3bitr4d 299 |
1
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵) → (𝑋 = {𝐴} ↔ 𝑅 = 〈{〈〈𝐴, 𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉)) |