Metamath Proof Explorer

Theorem drngprop

Description: If two structures have the same ring components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013) (Revised by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses drngprop.b 
|- ( Base ` K ) = ( Base ` L )
drngprop.p 
|- ( +g ` K ) = ( +g ` L )
drngprop.m 
|- ( .r ` K ) = ( .r ` L )
Assertion drngprop 
|- ( K e. DivRing <-> L e. DivRing )

Proof

Step Hyp Ref Expression
1 drngprop.b 
 |-  ( Base ` K ) = ( Base ` L )
2 drngprop.p 
 |-  ( +g ` K ) = ( +g ` L )
3 drngprop.m 
 |-  ( .r ` K ) = ( .r ` L )
4 eqidd 
 |-  ( K e. Ring -> ( Base ` K ) = ( Base ` K ) )
5 1 a1i 
 |-  ( K e. Ring -> ( Base ` K ) = ( Base ` L ) )
6 3 oveqi 
 |-  ( x ( .r ` K ) y ) = ( x ( .r ` L ) y )
7 6 a1i 
 |-  ( ( K e. Ring /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
8 4 5 7 unitpropd 
 |-  ( K e. Ring -> ( Unit ` K ) = ( Unit ` L ) )
9 2 oveqi 
 |-  ( x ( +g ` K ) y ) = ( x ( +g ` L ) y )
10 9 a1i 
 |-  ( ( K e. Ring /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
11 4 5 10 grpidpropd 
 |-  ( K e. Ring -> ( 0g ` K ) = ( 0g ` L ) )
12 11 sneqd 
 |-  ( K e. Ring -> { ( 0g ` K ) } = { ( 0g ` L ) } )
13 12 difeq2d 
 |-  ( K e. Ring -> ( ( Base ` K ) \ { ( 0g ` K ) } ) = ( ( Base ` K ) \ { ( 0g ` L ) } ) )
14 8 13 eqeq12d 
 |-  ( K e. Ring -> ( ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) <-> ( Unit ` L ) = ( ( Base ` K ) \ { ( 0g ` L ) } ) ) )
15 14 pm5.32i 
 |-  ( ( K e. Ring /\ ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) ) <-> ( K e. Ring /\ ( Unit ` L ) = ( ( Base ` K ) \ { ( 0g ` L ) } ) ) )
16 1 2 3 ringprop 
 |-  ( K e. Ring <-> L e. Ring )
17 16 anbi1i 
 |-  ( ( K e. Ring /\ ( Unit ` L ) = ( ( Base ` K ) \ { ( 0g ` L ) } ) ) <-> ( L e. Ring /\ ( Unit ` L ) = ( ( Base ` K ) \ { ( 0g ` L ) } ) ) )
18 15 17 bitri 
 |-  ( ( K e. Ring /\ ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) ) <-> ( L e. Ring /\ ( Unit ` L ) = ( ( Base ` K ) \ { ( 0g ` L ) } ) ) )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 eqid 
 |-  ( Unit ` K ) = ( Unit ` K )
21 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
22 19 20 21 isdrng 
 |-  ( K e. DivRing <-> ( K e. Ring /\ ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) ) )
23 eqid 
 |-  ( Unit ` L ) = ( Unit ` L )
24 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
25 1 23 24 isdrng 
 |-  ( L e. DivRing <-> ( L e. Ring /\ ( Unit ` L ) = ( ( Base ` K ) \ { ( 0g ` L ) } ) ) )
26 18 22 25 3bitr4i 
 |-  ( K e. DivRing <-> L e. DivRing )