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

Metamath Proof Explorer

Theorem grppropd

Description: If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 2-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 grppropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 grppropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 grppropd.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 1 2 3 grpidpropd 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` L ) )
6 5 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( 0g ` K ) = ( 0g ` L ) )
7 3 6 eqeq12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x ( +g ` K ) y ) = ( 0g ` K ) <-> ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
8 7 anass1rs 
 |-  ( ( ( ph /\ y e. B ) /\ x e. B ) -> ( ( x ( +g ` K ) y ) = ( 0g ` K ) <-> ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
9 8 rexbidva 
 |-  ( ( ph /\ y e. B ) -> ( E. x e. B ( x ( +g ` K ) y ) = ( 0g ` K ) <-> E. x e. B ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
10 9 ralbidva 
 |-  ( ph -> ( A. y e. B E. x e. B ( x ( +g ` K ) y ) = ( 0g ` K ) <-> A. y e. B E. x e. B ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
11 1 rexeqdv 
 |-  ( ph -> ( E. x e. B ( x ( +g ` K ) y ) = ( 0g ` K ) <-> E. x e. ( Base ` K ) ( x ( +g ` K ) y ) = ( 0g ` K ) ) )
12 1 11 raleqbidv 
 |-  ( ph -> ( A. y e. B E. x e. B ( x ( +g ` K ) y ) = ( 0g ` K ) <-> A. y e. ( Base ` K ) E. x e. ( Base ` K ) ( x ( +g ` K ) y ) = ( 0g ` K ) ) )
13 2 rexeqdv 
 |-  ( ph -> ( E. x e. B ( x ( +g ` L ) y ) = ( 0g ` L ) <-> E. x e. ( Base ` L ) ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
14 2 13 raleqbidv 
 |-  ( ph -> ( A. y e. B E. x e. B ( x ( +g ` L ) y ) = ( 0g ` L ) <-> A. y e. ( Base ` L ) E. x e. ( Base ` L ) ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
15 10 12 14 3bitr3d 
 |-  ( ph -> ( A. y e. ( Base ` K ) E. x e. ( Base ` K ) ( x ( +g ` K ) y ) = ( 0g ` K ) <-> A. y e. ( Base ` L ) E. x e. ( Base ` L ) ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
16 4 15 anbi12d 
 |-  ( ph -> ( ( K e. Mnd /\ A. y e. ( Base ` K ) E. x e. ( Base ` K ) ( x ( +g ` K ) y ) = ( 0g ` K ) ) <-> ( L e. Mnd /\ A. y e. ( Base ` L ) E. x e. ( Base ` L ) ( x ( +g ` L ) y ) = ( 0g ` L ) ) ) )
17 eqid 
 |-  ( Base ` K ) = ( Base ` K )
18 eqid 
 |-  ( +g ` K ) = ( +g ` K )
19 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
20 17 18 19 isgrp 
 |-  ( K e. Grp <-> ( K e. Mnd /\ A. y e. ( Base ` K ) E. x e. ( Base ` K ) ( x ( +g ` K ) y ) = ( 0g ` K ) ) )
21 eqid 
 |-  ( Base ` L ) = ( Base ` L )
22 eqid 
 |-  ( +g ` L ) = ( +g ` L )
23 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
24 21 22 23 isgrp 
 |-  ( L e. Grp <-> ( L e. Mnd /\ A. y e. ( Base ` L ) E. x e. ( Base ` L ) ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
25 16 20 24 3bitr4g 
 |-  ( ph -> ( K e. Grp <-> L e. Grp ) )