Metamath Proof Explorer

Theorem zrdivrng

Description: The zero ring is not a division ring. (Contributed by FL, 24-Jan-2010) (Proof shortened by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis zrdivrng.1 
|- A e. _V
Assertion zrdivrng 
|- -. <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. e. DivRingOps

Proof

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