Step |
Hyp |
Ref |
Expression |
1 |
|
on1el3.1 |
⊢ 𝐺 = ( 1st ‘ 𝑅 ) |
2 |
|
on1el3.2 |
⊢ 𝑋 = ran 𝐺 |
3 |
1
|
rngogrpo |
⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp ) |
4 |
2
|
grpofo |
⊢ ( 𝐺 ∈ GrpOp → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ) |
5 |
|
fof |
⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) |
6 |
3 4 5
|
3syl |
⊢ ( 𝑅 ∈ RingOps → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) |
7 |
6
|
adantr |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) |
8 |
|
id |
⊢ ( 𝑋 = { 𝐴 } → 𝑋 = { 𝐴 } ) |
9 |
8
|
sqxpeqd |
⊢ ( 𝑋 = { 𝐴 } → ( 𝑋 × 𝑋 ) = ( { 𝐴 } × { 𝐴 } ) ) |
10 |
9 8
|
feq23d |
⊢ ( 𝑋 = { 𝐴 } → ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ↔ 𝐺 : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } ) ) |
11 |
7 10
|
syl5ibcom |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 = { 𝐴 } → 𝐺 : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } ) ) |
12 |
7
|
fdmd |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → dom 𝐺 = ( 𝑋 × 𝑋 ) ) |
13 |
12
|
eqcomd |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 × 𝑋 ) = dom 𝐺 ) |
14 |
|
fdm |
⊢ ( 𝐺 : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } → dom 𝐺 = ( { 𝐴 } × { 𝐴 } ) ) |
15 |
14
|
eqeq2d |
⊢ ( 𝐺 : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } → ( ( 𝑋 × 𝑋 ) = dom 𝐺 ↔ ( 𝑋 × 𝑋 ) = ( { 𝐴 } × { 𝐴 } ) ) ) |
16 |
13 15
|
syl5ibcom |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝐺 : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } → ( 𝑋 × 𝑋 ) = ( { 𝐴 } × { 𝐴 } ) ) ) |
17 |
|
xpid11 |
⊢ ( ( 𝑋 × 𝑋 ) = ( { 𝐴 } × { 𝐴 } ) ↔ 𝑋 = { 𝐴 } ) |
18 |
16 17
|
syl6ib |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝐺 : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } → 𝑋 = { 𝐴 } ) ) |
19 |
11 18
|
impbid |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 = { 𝐴 } ↔ 𝐺 : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } ) ) |
20 |
|
simpr |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 ) |
21 |
|
xpsng |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( { 𝐴 } × { 𝐴 } ) = { 〈 𝐴 , 𝐴 〉 } ) |
22 |
20 21
|
sylancom |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( { 𝐴 } × { 𝐴 } ) = { 〈 𝐴 , 𝐴 〉 } ) |
23 |
22
|
feq2d |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝐺 : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } ↔ 𝐺 : { 〈 𝐴 , 𝐴 〉 } ⟶ { 𝐴 } ) ) |
24 |
|
opex |
⊢ 〈 𝐴 , 𝐴 〉 ∈ V |
25 |
|
fsng |
⊢ ( ( 〈 𝐴 , 𝐴 〉 ∈ V ∧ 𝐴 ∈ 𝐵 ) → ( 𝐺 : { 〈 𝐴 , 𝐴 〉 } ⟶ { 𝐴 } ↔ 𝐺 = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) |
26 |
24 20 25
|
sylancr |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝐺 : { 〈 𝐴 , 𝐴 〉 } ⟶ { 𝐴 } ↔ 𝐺 = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) |
27 |
19 23 26
|
3bitrd |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 = { 𝐴 } ↔ 𝐺 = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) |
28 |
1
|
eqeq1i |
⊢ ( 𝐺 = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ↔ ( 1st ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) |
29 |
27 28
|
syl6bb |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 = { 𝐴 } ↔ ( 1st ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) |
30 |
29
|
anbi1d |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑋 = { 𝐴 } ∧ ( 2nd ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ↔ ( ( 1st ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∧ ( 2nd ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) ) |
31 |
|
eqid |
⊢ ( 2nd ‘ 𝑅 ) = ( 2nd ‘ 𝑅 ) |
32 |
1 31 2
|
rngosm |
⊢ ( 𝑅 ∈ RingOps → ( 2nd ‘ 𝑅 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) |
33 |
32
|
adantr |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 2nd ‘ 𝑅 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) |
34 |
9 8
|
feq23d |
⊢ ( 𝑋 = { 𝐴 } → ( ( 2nd ‘ 𝑅 ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ↔ ( 2nd ‘ 𝑅 ) : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } ) ) |
35 |
33 34
|
syl5ibcom |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 = { 𝐴 } → ( 2nd ‘ 𝑅 ) : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } ) ) |
36 |
22
|
feq2d |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( ( 2nd ‘ 𝑅 ) : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } ↔ ( 2nd ‘ 𝑅 ) : { 〈 𝐴 , 𝐴 〉 } ⟶ { 𝐴 } ) ) |
37 |
|
fsng |
⊢ ( ( 〈 𝐴 , 𝐴 〉 ∈ V ∧ 𝐴 ∈ 𝐵 ) → ( ( 2nd ‘ 𝑅 ) : { 〈 𝐴 , 𝐴 〉 } ⟶ { 𝐴 } ↔ ( 2nd ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) |
38 |
24 20 37
|
sylancr |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( ( 2nd ‘ 𝑅 ) : { 〈 𝐴 , 𝐴 〉 } ⟶ { 𝐴 } ↔ ( 2nd ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) |
39 |
36 38
|
bitrd |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( ( 2nd ‘ 𝑅 ) : ( { 𝐴 } × { 𝐴 } ) ⟶ { 𝐴 } ↔ ( 2nd ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) |
40 |
35 39
|
sylibd |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 = { 𝐴 } → ( 2nd ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) |
41 |
40
|
pm4.71d |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 = { 𝐴 } ↔ ( 𝑋 = { 𝐴 } ∧ ( 2nd ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) ) |
42 |
|
relrngo |
⊢ Rel RingOps |
43 |
|
df-rel |
⊢ ( Rel RingOps ↔ RingOps ⊆ ( V × V ) ) |
44 |
42 43
|
mpbi |
⊢ RingOps ⊆ ( V × V ) |
45 |
44
|
sseli |
⊢ ( 𝑅 ∈ RingOps → 𝑅 ∈ ( V × V ) ) |
46 |
45
|
adantr |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → 𝑅 ∈ ( V × V ) ) |
47 |
|
eqop |
⊢ ( 𝑅 ∈ ( V × V ) → ( 𝑅 = 〈 { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } , { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } 〉 ↔ ( ( 1st ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∧ ( 2nd ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) ) |
48 |
46 47
|
syl |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝑅 = 〈 { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } , { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } 〉 ↔ ( ( 1st ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∧ ( 2nd ‘ 𝑅 ) = { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) ) ) |
49 |
30 41 48
|
3bitr4d |
⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 = { 𝐴 } ↔ 𝑅 = 〈 { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } , { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } 〉 ) ) |