Metamath Proof Explorer

Theorem cmnpropd

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

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

Proof

Step Hyp Ref Expression
1 ablpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 ablpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 ablpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 1 2 3 mndpropd 
 |-  ( ph -> ( K e. Mnd <-> L e. Mnd ) )
5 3 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
6 3 oveqrspc2v 
 |-  ( ( ph /\ ( v e. B /\ u e. B ) ) -> ( v ( +g ` K ) u ) = ( v ( +g ` L ) u ) )
7 6 ancom2s 
 |-  ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( v ( +g ` K ) u ) = ( v ( +g ` L ) u ) )
8 5 7 eqeq12d 
 |-  ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) <-> ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) )
9 8 2ralbidva 
 |-  ( ph -> ( A. u e. B A. v e. B ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) <-> A. u e. B A. v e. B ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) )
10 1 raleqdv 
 |-  ( ph -> ( A. v e. B ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) <-> A. v e. ( Base ` K ) ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) ) )
11 1 10 raleqbidv 
 |-  ( ph -> ( A. u e. B A. v e. B ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) ) )
12 2 raleqdv 
 |-  ( ph -> ( A. v e. B ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) <-> A. v e. ( Base ` L ) ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) )
13 2 12 raleqbidv 
 |-  ( ph -> ( A. u e. B A. v e. B ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) )
14 9 11 13 3bitr3d 
 |-  ( ph -> ( A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) )
15 4 14 anbi12d 
 |-  ( ph -> ( ( K e. Mnd /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) ) <-> ( L e. Mnd /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) ) )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 eqid 
 |-  ( +g ` K ) = ( +g ` K )
18 16 17 iscmn 
 |-  ( K e. CMnd <-> ( K e. Mnd /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( u ( +g ` K ) v ) = ( v ( +g ` K ) u ) ) )
19 eqid 
 |-  ( Base ` L ) = ( Base ` L )
20 eqid 
 |-  ( +g ` L ) = ( +g ` L )
21 19 20 iscmn 
 |-  ( L e. CMnd <-> ( L e. Mnd /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( u ( +g ` L ) v ) = ( v ( +g ` L ) u ) ) )
22 15 18 21 3bitr4g 
 |-  ( ph -> ( K e. CMnd <-> L e. CMnd ) )