Step |
Hyp |
Ref |
Expression |
1 |
|
zrdivrng.1 |
|- A e. _V |
2 |
|
0ngrp |
|- -. (/) e. GrpOp |
3 |
|
opex |
|- <. A , A >. e. _V |
4 |
3
|
rnsnop |
|- ran { <. <. A , A >. , A >. } = { A } |
5 |
1
|
gidsn |
|- ( GId ` { <. <. A , A >. , A >. } ) = A |
6 |
5
|
sneqi |
|- { ( GId ` { <. <. A , A >. , A >. } ) } = { A } |
7 |
4 6
|
difeq12i |
|- ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) = ( { A } \ { A } ) |
8 |
|
difid |
|- ( { A } \ { A } ) = (/) |
9 |
7 8
|
eqtri |
|- ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) = (/) |
10 |
9
|
xpeq2i |
|- ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) = ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. (/) ) |
11 |
|
xp0 |
|- ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. (/) ) = (/) |
12 |
10 11
|
eqtri |
|- ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) = (/) |
13 |
12
|
reseq2i |
|- ( { <. <. A , A >. , A >. } |` ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) ) = ( { <. <. A , A >. , A >. } |` (/) ) |
14 |
|
res0 |
|- ( { <. <. A , A >. , A >. } |` (/) ) = (/) |
15 |
13 14
|
eqtri |
|- ( { <. <. A , A >. , A >. } |` ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) ) = (/) |
16 |
|
snex |
|- { <. <. A , A >. , A >. } e. _V |
17 |
|
isdivrngo |
|- ( { <. <. A , A >. , A >. } e. _V -> ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps <-> ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. RingOps /\ ( { <. <. A , A >. , A >. } |` ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) ) e. GrpOp ) ) ) |
18 |
16 17
|
ax-mp |
|- ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps <-> ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. RingOps /\ ( { <. <. A , A >. , A >. } |` ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) ) e. GrpOp ) ) |
19 |
18
|
simprbi |
|- ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps -> ( { <. <. A , A >. , A >. } |` ( ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) X. ( ran { <. <. A , A >. , A >. } \ { ( GId ` { <. <. A , A >. , A >. } ) } ) ) ) e. GrpOp ) |
20 |
15 19
|
eqeltrrid |
|- ( <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps -> (/) e. GrpOp ) |
21 |
2 20
|
mto |
|- -. <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps |