This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem crngpropd

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

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

Proof

Step Hyp Ref Expression
1 ringpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 ringpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 ringpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 ringpropd.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 1 2 3 4 ringpropd 
 |-  ( ph -> ( K e. Ring <-> L e. Ring ) )
6 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 6 7 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
9 1 8 eqtrdi 
 |-  ( ph -> B = ( Base ` ( mulGrp ` K ) ) )
10 eqid 
 |-  ( mulGrp ` L ) = ( mulGrp ` L )
11 eqid 
 |-  ( Base ` L ) = ( Base ` L )
12 10 11 mgpbas 
 |-  ( Base ` L ) = ( Base ` ( mulGrp ` L ) )
13 2 12 eqtrdi 
 |-  ( ph -> B = ( Base ` ( mulGrp ` L ) ) )
14 eqid 
 |-  ( .r ` K ) = ( .r ` K )
15 6 14 mgpplusg 
 |-  ( .r ` K ) = ( +g ` ( mulGrp ` K ) )
16 15 oveqi 
 |-  ( x ( .r ` K ) y ) = ( x ( +g ` ( mulGrp ` K ) ) y )
17 eqid 
 |-  ( .r ` L ) = ( .r ` L )
18 10 17 mgpplusg 
 |-  ( .r ` L ) = ( +g ` ( mulGrp ` L ) )
19 18 oveqi 
 |-  ( x ( .r ` L ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y )
20 4 16 19 3eqtr3g 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` ( mulGrp ` K ) ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y ) )
21 9 13 20 cmnpropd 
 |-  ( ph -> ( ( mulGrp ` K ) e. CMnd <-> ( mulGrp ` L ) e. CMnd ) )
22 5 21 anbi12d 
 |-  ( ph -> ( ( K e. Ring /\ ( mulGrp ` K ) e. CMnd ) <-> ( L e. Ring /\ ( mulGrp ` L ) e. CMnd ) ) )
23 6 iscrng 
 |-  ( K e. CRing <-> ( K e. Ring /\ ( mulGrp ` K ) e. CMnd ) )
24 10 iscrng 
 |-  ( L e. CRing <-> ( L e. Ring /\ ( mulGrp ` L ) e. CMnd ) )
25 22 23 24 3bitr4g 
 |-  ( ph -> ( K e. CRing <-> L e. CRing ) )