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 ) )