Metamath Proof Explorer

Theorem dvrunz

Description: In a division ring the ring unit is different from the zero. (Contributed by FL, 14-Feb-2010) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dvrunz.1 
|- G = ( 1st ` R )
dvrunz.2 
|- H = ( 2nd ` R )
dvrunz.3 
|- X = ran G
dvrunz.4 
|- Z = ( GId ` G )
dvrunz.5 
|- U = ( GId ` H )
Assertion dvrunz 
|- ( R e. DivRingOps -> U =/= Z )

Proof

Step Hyp Ref Expression
1 dvrunz.1 
 |-  G = ( 1st ` R )
2 dvrunz.2 
 |-  H = ( 2nd ` R )
3 dvrunz.3 
 |-  X = ran G
4 dvrunz.4 
 |-  Z = ( GId ` G )
5 dvrunz.5 
 |-  U = ( GId ` H )
6 4 fvexi 
 |-  Z e. _V
7 6 zrdivrng 
 |-  -. <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. e. DivRingOps
8 1 2 3 4 drngoi 
 |-  ( R e. DivRingOps -> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )
9 8 simpld 
 |-  ( R e. DivRingOps -> R e. RingOps )
10 1 2 4 5 3 rngoueqz 
 |-  ( R e. RingOps -> ( X ~~ 1o <-> U = Z ) )
11 9 10 syl 
 |-  ( R e. DivRingOps -> ( X ~~ 1o <-> U = Z ) )
12 1 3 4 rngosn6 
 |-  ( R e. RingOps -> ( X ~~ 1o <-> R = <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. ) )
13 9 12 syl 
 |-  ( R e. DivRingOps -> ( X ~~ 1o <-> R = <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. ) )
14 eleq1 
 |-  ( R = <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. -> ( R e. DivRingOps <-> <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. e. DivRingOps ) )
15 14 biimpd 
 |-  ( R = <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. -> ( R e. DivRingOps -> <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. e. DivRingOps ) )
16 13 15 biimtrdi 
 |-  ( R e. DivRingOps -> ( X ~~ 1o -> ( R e. DivRingOps -> <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. e. DivRingOps ) ) )
17 16 pm2.43a 
 |-  ( R e. DivRingOps -> ( X ~~ 1o -> <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. e. DivRingOps ) )
18 11 17 sylbird 
 |-  ( R e. DivRingOps -> ( U = Z -> <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. e. DivRingOps ) )
19 18 necon3bd 
 |-  ( R e. DivRingOps -> ( -. <. { <. <. Z , Z >. , Z >. } , { <. <. Z , Z >. , Z >. } >. e. DivRingOps -> U =/= Z ) )
20 7 19 mpi 
 |-  ( R e. DivRingOps -> U =/= Z )