Step |
Hyp |
Ref |
Expression |
1 |
|
zrdivrng.1 |
⊢ 𝐴 ∈ V |
2 |
|
0ngrp |
⊢ ¬ ∅ ∈ GrpOp |
3 |
|
opex |
⊢ 〈 𝐴 , 𝐴 〉 ∈ V |
4 |
3
|
rnsnop |
⊢ ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } = { 𝐴 } |
5 |
1
|
gidsn |
⊢ ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) = 𝐴 |
6 |
5
|
sneqi |
⊢ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } = { 𝐴 } |
7 |
4 6
|
difeq12i |
⊢ ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) = ( { 𝐴 } ∖ { 𝐴 } ) |
8 |
|
difid |
⊢ ( { 𝐴 } ∖ { 𝐴 } ) = ∅ |
9 |
7 8
|
eqtri |
⊢ ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) = ∅ |
10 |
9
|
xpeq2i |
⊢ ( ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) × ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) ) = ( ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) × ∅ ) |
11 |
|
xp0 |
⊢ ( ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) × ∅ ) = ∅ |
12 |
10 11
|
eqtri |
⊢ ( ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) × ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) ) = ∅ |
13 |
12
|
reseq2i |
⊢ ( { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ↾ ( ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) × ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) ) ) = ( { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ↾ ∅ ) |
14 |
|
res0 |
⊢ ( { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ↾ ∅ ) = ∅ |
15 |
13 14
|
eqtri |
⊢ ( { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ↾ ( ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) × ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) ) ) = ∅ |
16 |
|
snex |
⊢ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∈ V |
17 |
|
isdivrngo |
⊢ ( { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∈ V → ( 〈 { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } , { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } 〉 ∈ DivRingOps ↔ ( 〈 { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } , { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } 〉 ∈ RingOps ∧ ( { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ↾ ( ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) × ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) ) ) ∈ GrpOp ) ) ) |
18 |
16 17
|
ax-mp |
⊢ ( 〈 { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } , { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } 〉 ∈ DivRingOps ↔ ( 〈 { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } , { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } 〉 ∈ RingOps ∧ ( { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ↾ ( ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) × ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) ) ) ∈ GrpOp ) ) |
19 |
18
|
simprbi |
⊢ ( 〈 { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } , { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } 〉 ∈ DivRingOps → ( { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ↾ ( ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) × ( ran { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ∖ { ( GId ‘ { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } ) } ) ) ) ∈ GrpOp ) |
20 |
15 19
|
eqeltrrid |
⊢ ( 〈 { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } , { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } 〉 ∈ DivRingOps → ∅ ∈ GrpOp ) |
21 |
2 20
|
mto |
⊢ ¬ 〈 { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } , { 〈 〈 𝐴 , 𝐴 〉 , 𝐴 〉 } 〉 ∈ DivRingOps |