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