Metamath Proof Explorer

Theorem isdrngo3

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses isdivrng1.1 
|- G = ( 1st ` R )
isdivrng1.2 
|- H = ( 2nd ` R )
isdivrng1.3 
|- Z = ( GId ` G )
isdivrng1.4 
|- X = ran G
isdivrng2.5 
|- U = ( GId ` H )
Assertion isdrngo3 
|- ( R e. DivRingOps <-> ( R e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U ) ) )

Proof

Step Hyp Ref Expression
1 isdivrng1.1 
 |-  G = ( 1st ` R )
2 isdivrng1.2 
 |-  H = ( 2nd ` R )
3 isdivrng1.3 
 |-  Z = ( GId ` G )
4 isdivrng1.4 
 |-  X = ran G
5 isdivrng2.5 
 |-  U = ( GId ` H )
6 1 2 3 4 5 isdrngo2 
 |-  ( R e. DivRingOps <-> ( R e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = U ) ) )
7 eldifi 
 |-  ( x e. ( X \ { Z } ) -> x e. X )
8 difss 
 |-  ( X \ { Z } ) C_ X
9 ssrexv 
 |-  ( ( X \ { Z } ) C_ X -> ( E. y e. ( X \ { Z } ) ( y H x ) = U -> E. y e. X ( y H x ) = U ) )
10 8 9 ax-mp 
 |-  ( E. y e. ( X \ { Z } ) ( y H x ) = U -> E. y e. X ( y H x ) = U )
11 neeq1 
 |-  ( ( y H x ) = U -> ( ( y H x ) =/= Z <-> U =/= Z ) )
12 11 biimparc 
 |-  ( ( U =/= Z /\ ( y H x ) = U ) -> ( y H x ) =/= Z )
13 3 4 1 2 rngolz 
 |-  ( ( R e. RingOps /\ x e. X ) -> ( Z H x ) = Z )
14 oveq1 
 |-  ( y = Z -> ( y H x ) = ( Z H x ) )
15 14 eqeq1d 
 |-  ( y = Z -> ( ( y H x ) = Z <-> ( Z H x ) = Z ) )
16 13 15 syl5ibrcom 
 |-  ( ( R e. RingOps /\ x e. X ) -> ( y = Z -> ( y H x ) = Z ) )
17 16 necon3d 
 |-  ( ( R e. RingOps /\ x e. X ) -> ( ( y H x ) =/= Z -> y =/= Z ) )
18 17 imp 
 |-  ( ( ( R e. RingOps /\ x e. X ) /\ ( y H x ) =/= Z ) -> y =/= Z )
19 12 18 sylan2 
 |-  ( ( ( R e. RingOps /\ x e. X ) /\ ( U =/= Z /\ ( y H x ) = U ) ) -> y =/= Z )
20 19 an4s 
 |-  ( ( ( R e. RingOps /\ U =/= Z ) /\ ( x e. X /\ ( y H x ) = U ) ) -> y =/= Z )
21 20 anassrs 
 |-  ( ( ( ( R e. RingOps /\ U =/= Z ) /\ x e. X ) /\ ( y H x ) = U ) -> y =/= Z )
22 pm3.2 
 |-  ( y e. X -> ( y =/= Z -> ( y e. X /\ y =/= Z ) ) )
23 21 22 syl5com 
 |-  ( ( ( ( R e. RingOps /\ U =/= Z ) /\ x e. X ) /\ ( y H x ) = U ) -> ( y e. X -> ( y e. X /\ y =/= Z ) ) )
24 eldifsn 
 |-  ( y e. ( X \ { Z } ) <-> ( y e. X /\ y =/= Z ) )
25 23 24 imbitrrdi 
 |-  ( ( ( ( R e. RingOps /\ U =/= Z ) /\ x e. X ) /\ ( y H x ) = U ) -> ( y e. X -> y e. ( X \ { Z } ) ) )
26 25 imdistanda 
 |-  ( ( ( R e. RingOps /\ U =/= Z ) /\ x e. X ) -> ( ( ( y H x ) = U /\ y e. X ) -> ( ( y H x ) = U /\ y e. ( X \ { Z } ) ) ) )
27 ancom 
 |-  ( ( y e. X /\ ( y H x ) = U ) <-> ( ( y H x ) = U /\ y e. X ) )
28 ancom 
 |-  ( ( y e. ( X \ { Z } ) /\ ( y H x ) = U ) <-> ( ( y H x ) = U /\ y e. ( X \ { Z } ) ) )
29 26 27 28 3imtr4g 
 |-  ( ( ( R e. RingOps /\ U =/= Z ) /\ x e. X ) -> ( ( y e. X /\ ( y H x ) = U ) -> ( y e. ( X \ { Z } ) /\ ( y H x ) = U ) ) )
30 29 reximdv2 
 |-  ( ( ( R e. RingOps /\ U =/= Z ) /\ x e. X ) -> ( E. y e. X ( y H x ) = U -> E. y e. ( X \ { Z } ) ( y H x ) = U ) )
31 10 30 impbid2 
 |-  ( ( ( R e. RingOps /\ U =/= Z ) /\ x e. X ) -> ( E. y e. ( X \ { Z } ) ( y H x ) = U <-> E. y e. X ( y H x ) = U ) )
32 7 31 sylan2 
 |-  ( ( ( R e. RingOps /\ U =/= Z ) /\ x e. ( X \ { Z } ) ) -> ( E. y e. ( X \ { Z } ) ( y H x ) = U <-> E. y e. X ( y H x ) = U ) )
33 32 ralbidva 
 |-  ( ( R e. RingOps /\ U =/= Z ) -> ( A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = U <-> A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U ) )
34 33 pm5.32da 
 |-  ( R e. RingOps -> ( ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = U ) <-> ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U ) ) )
35 34 pm5.32i 
 |-  ( ( R e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = U ) ) <-> ( R e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U ) ) )
36 6 35 bitri 
 |-  ( R e. DivRingOps <-> ( R e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U ) ) )