Metamath Proof Explorer

Theorem grpinvpropd

Description: If two structures have the same group components (properties), they have the same group inversion function. (Contributed by Mario Carneiro, 27-Nov-2014) (Revised by Stefan O'Rear, 21-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 grpinvpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 grpinvpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 grpinvpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 1 2 3 grpidpropd 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` L ) )
5 4 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( 0g ` K ) = ( 0g ` L ) )
6 3 5 eqeq12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x ( +g ` K ) y ) = ( 0g ` K ) <-> ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
7 6 anass1rs 
 |-  ( ( ( ph /\ y e. B ) /\ x e. B ) -> ( ( x ( +g ` K ) y ) = ( 0g ` K ) <-> ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
8 7 riotabidva 
 |-  ( ( ph /\ y e. B ) -> ( iota_ x e. B ( x ( +g ` K ) y ) = ( 0g ` K ) ) = ( iota_ x e. B ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
9 8 mpteq2dva 
 |-  ( ph -> ( y e. B |-> ( iota_ x e. B ( x ( +g ` K ) y ) = ( 0g ` K ) ) ) = ( y e. B |-> ( iota_ x e. B ( x ( +g ` L ) y ) = ( 0g ` L ) ) ) )
10 1 riotaeqdv 
 |-  ( ph -> ( iota_ x e. B ( x ( +g ` K ) y ) = ( 0g ` K ) ) = ( iota_ x e. ( Base ` K ) ( x ( +g ` K ) y ) = ( 0g ` K ) ) )
11 1 10 mpteq12dv 
 |-  ( ph -> ( y e. B |-> ( iota_ x e. B ( x ( +g ` K ) y ) = ( 0g ` K ) ) ) = ( y e. ( Base ` K ) |-> ( iota_ x e. ( Base ` K ) ( x ( +g ` K ) y ) = ( 0g ` K ) ) ) )
12 2 riotaeqdv 
 |-  ( ph -> ( iota_ x e. B ( x ( +g ` L ) y ) = ( 0g ` L ) ) = ( iota_ x e. ( Base ` L ) ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
13 2 12 mpteq12dv 
 |-  ( ph -> ( y e. B |-> ( iota_ x e. B ( x ( +g ` L ) y ) = ( 0g ` L ) ) ) = ( y e. ( Base ` L ) |-> ( iota_ x e. ( Base ` L ) ( x ( +g ` L ) y ) = ( 0g ` L ) ) ) )
14 9 11 13 3eqtr3d 
 |-  ( ph -> ( y e. ( Base ` K ) |-> ( iota_ x e. ( Base ` K ) ( x ( +g ` K ) y ) = ( 0g ` K ) ) ) = ( y e. ( Base ` L ) |-> ( iota_ x e. ( Base ` L ) ( x ( +g ` L ) y ) = ( 0g ` L ) ) ) )
15 eqid 
 |-  ( Base ` K ) = ( Base ` K )
16 eqid 
 |-  ( +g ` K ) = ( +g ` K )
17 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
18 eqid 
 |-  ( invg ` K ) = ( invg ` K )
19 15 16 17 18 grpinvfval 
 |-  ( invg ` K ) = ( y e. ( Base ` K ) |-> ( iota_ x e. ( Base ` K ) ( x ( +g ` K ) y ) = ( 0g ` K ) ) )
20 eqid 
 |-  ( Base ` L ) = ( Base ` L )
21 eqid 
 |-  ( +g ` L ) = ( +g ` L )
22 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
23 eqid 
 |-  ( invg ` L ) = ( invg ` L )
24 20 21 22 23 grpinvfval 
 |-  ( invg ` L ) = ( y e. ( Base ` L ) |-> ( iota_ x e. ( Base ` L ) ( x ( +g ` L ) y ) = ( 0g ` L ) ) )
25 14 19 24 3eqtr4g 
 |-  ( ph -> ( invg ` K ) = ( invg ` L ) )