Metamath Proof Explorer

Theorem drngpropd

Description: If two structures have the same group components (properties), one is a division ring iff the other one is. (Contributed by Mario Carneiro, 27-Jun-2015)

Ref Expression
Hypotheses drngpropd.1 
|- ( ph -> B = ( Base ` K ) )
drngpropd.2 
|- ( ph -> B = ( Base ` L ) )
drngpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
drngpropd.4 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion drngpropd 
|- ( ph -> ( K e. DivRing <-> L e. DivRing ) )

Proof

Step Hyp Ref Expression
1 drngpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 drngpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 drngpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 drngpropd.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 1 2 4 unitpropd 
 |-  ( ph -> ( Unit ` K ) = ( Unit ` L ) )
6 5 adantr 
 |-  ( ( ph /\ K e. Ring ) -> ( Unit ` K ) = ( Unit ` L ) )
7 1 2 eqtr3d 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
8 7 adantr 
 |-  ( ( ph /\ K e. Ring ) -> ( Base ` K ) = ( Base ` L ) )
9 1 adantr 
 |-  ( ( ph /\ K e. Ring ) -> B = ( Base ` K ) )
10 2 adantr 
 |-  ( ( ph /\ K e. Ring ) -> B = ( Base ` L ) )
11 3 adantlr 
 |-  ( ( ( ph /\ K e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
12 9 10 11 grpidpropd 
 |-  ( ( ph /\ K e. Ring ) -> ( 0g ` K ) = ( 0g ` L ) )
13 12 sneqd 
 |-  ( ( ph /\ K e. Ring ) -> { ( 0g ` K ) } = { ( 0g ` L ) } )
14 8 13 difeq12d 
 |-  ( ( ph /\ K e. Ring ) -> ( ( Base ` K ) \ { ( 0g ` K ) } ) = ( ( Base ` L ) \ { ( 0g ` L ) } ) )
15 6 14 eqeq12d 
 |-  ( ( ph /\ K e. Ring ) -> ( ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) <-> ( Unit ` L ) = ( ( Base ` L ) \ { ( 0g ` L ) } ) ) )
16 15 pm5.32da 
 |-  ( ph -> ( ( K e. Ring /\ ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) ) <-> ( K e. Ring /\ ( Unit ` L ) = ( ( Base ` L ) \ { ( 0g ` L ) } ) ) ) )
17 1 2 3 4 ringpropd 
 |-  ( ph -> ( K e. Ring <-> L e. Ring ) )
18 17 anbi1d 
 |-  ( ph -> ( ( K e. Ring /\ ( Unit ` L ) = ( ( Base ` L ) \ { ( 0g ` L ) } ) ) <-> ( L e. Ring /\ ( Unit ` L ) = ( ( Base ` L ) \ { ( 0g ` L ) } ) ) ) )
19 16 18 bitrd 
 |-  ( ph -> ( ( K e. Ring /\ ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) ) <-> ( L e. Ring /\ ( Unit ` L ) = ( ( Base ` L ) \ { ( 0g ` L ) } ) ) ) )
20 eqid 
 |-  ( Base ` K ) = ( Base ` K )
21 eqid 
 |-  ( Unit ` K ) = ( Unit ` K )
22 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
23 20 21 22 isdrng 
 |-  ( K e. DivRing <-> ( K e. Ring /\ ( Unit ` K ) = ( ( Base ` K ) \ { ( 0g ` K ) } ) ) )
24 eqid 
 |-  ( Base ` L ) = ( Base ` L )
25 eqid 
 |-  ( Unit ` L ) = ( Unit ` L )
26 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
27 24 25 26 isdrng 
 |-  ( L e. DivRing <-> ( L e. Ring /\ ( Unit ` L ) = ( ( Base ` L ) \ { ( 0g ` L ) } ) ) )
28 19 23 27 3bitr4g 
 |-  ( ph -> ( K e. DivRing <-> L e. DivRing ) )