Metamath Proof Explorer

Theorem grpinvssd

Description: If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the elements of the first group have the same inverses in both groups. (Contributed by AV, 15-Mar-2019)

Ref Expression
Hypotheses grpidssd.m 
|- ( ph -> M e. Grp )
grpidssd.s 
|- ( ph -> S e. Grp )
grpidssd.b 
|- B = ( Base ` S )
grpidssd.c 
|- ( ph -> B C_ ( Base ` M ) )
grpidssd.o 
|- ( ph -> A. x e. B A. y e. B ( x ( +g ` M ) y ) = ( x ( +g ` S ) y ) )
Assertion grpinvssd 
|- ( ph -> ( X e. B -> ( ( invg ` S ) ` X ) = ( ( invg ` M ) ` X ) ) )

Proof

Step Hyp Ref Expression
1 grpidssd.m 
 |-  ( ph -> M e. Grp )
2 grpidssd.s 
 |-  ( ph -> S e. Grp )
3 grpidssd.b 
 |-  B = ( Base ` S )
4 grpidssd.c 
 |-  ( ph -> B C_ ( Base ` M ) )
5 grpidssd.o 
 |-  ( ph -> A. x e. B A. y e. B ( x ( +g ` M ) y ) = ( x ( +g ` S ) y ) )
6 eqid 
 |-  ( invg ` S ) = ( invg ` S )
7 3 6 grpinvcl 
 |-  ( ( S e. Grp /\ X e. B ) -> ( ( invg ` S ) ` X ) e. B )
8 2 7 sylan 
 |-  ( ( ph /\ X e. B ) -> ( ( invg ` S ) ` X ) e. B )
9 simpr 
 |-  ( ( ph /\ X e. B ) -> X e. B )
10 5 adantr 
 |-  ( ( ph /\ X e. B ) -> A. x e. B A. y e. B ( x ( +g ` M ) y ) = ( x ( +g ` S ) y ) )
11 oveq1 
 |-  ( x = ( ( invg ` S ) ` X ) -> ( x ( +g ` M ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` M ) y ) )
12 oveq1 
 |-  ( x = ( ( invg ` S ) ` X ) -> ( x ( +g ` S ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) y ) )
13 11 12 eqeq12d 
 |-  ( x = ( ( invg ` S ) ` X ) -> ( ( x ( +g ` M ) y ) = ( x ( +g ` S ) y ) <-> ( ( ( invg ` S ) ` X ) ( +g ` M ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) y ) ) )
14 oveq2 
 |-  ( y = X -> ( ( ( invg ` S ) ` X ) ( +g ` M ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` M ) X ) )
15 oveq2 
 |-  ( y = X -> ( ( ( invg ` S ) ` X ) ( +g ` S ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) X ) )
16 14 15 eqeq12d 
 |-  ( y = X -> ( ( ( ( invg ` S ) ` X ) ( +g ` M ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) y ) <-> ( ( ( invg ` S ) ` X ) ( +g ` M ) X ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) X ) ) )
17 13 16 rspc2va 
 |-  ( ( ( ( ( invg ` S ) ` X ) e. B /\ X e. B ) /\ A. x e. B A. y e. B ( x ( +g ` M ) y ) = ( x ( +g ` S ) y ) ) -> ( ( ( invg ` S ) ` X ) ( +g ` M ) X ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) X ) )
18 8 9 10 17 syl21anc 
 |-  ( ( ph /\ X e. B ) -> ( ( ( invg ` S ) ` X ) ( +g ` M ) X ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) X ) )
19 eqid 
 |-  ( +g ` S ) = ( +g ` S )
20 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
21 3 19 20 6 grplinv 
 |-  ( ( S e. Grp /\ X e. B ) -> ( ( ( invg ` S ) ` X ) ( +g ` S ) X ) = ( 0g ` S ) )
22 2 21 sylan 
 |-  ( ( ph /\ X e. B ) -> ( ( ( invg ` S ) ` X ) ( +g ` S ) X ) = ( 0g ` S ) )
23 4 sselda 
 |-  ( ( ph /\ X e. B ) -> X e. ( Base ` M ) )
24 eqid 
 |-  ( Base ` M ) = ( Base ` M )
25 eqid 
 |-  ( +g ` M ) = ( +g ` M )
26 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
27 eqid 
 |-  ( invg ` M ) = ( invg ` M )
28 24 25 26 27 grplinv 
 |-  ( ( M e. Grp /\ X e. ( Base ` M ) ) -> ( ( ( invg ` M ) ` X ) ( +g ` M ) X ) = ( 0g ` M ) )
29 1 23 28 syl2an2r 
 |-  ( ( ph /\ X e. B ) -> ( ( ( invg ` M ) ` X ) ( +g ` M ) X ) = ( 0g ` M ) )
30 1 2 3 4 5 grpidssd 
 |-  ( ph -> ( 0g ` M ) = ( 0g ` S ) )
31 30 adantr 
 |-  ( ( ph /\ X e. B ) -> ( 0g ` M ) = ( 0g ` S ) )
32 29 31 eqtr2d 
 |-  ( ( ph /\ X e. B ) -> ( 0g ` S ) = ( ( ( invg ` M ) ` X ) ( +g ` M ) X ) )
33 18 22 32 3eqtrd 
 |-  ( ( ph /\ X e. B ) -> ( ( ( invg ` S ) ` X ) ( +g ` M ) X ) = ( ( ( invg ` M ) ` X ) ( +g ` M ) X ) )
34 1 adantr 
 |-  ( ( ph /\ X e. B ) -> M e. Grp )
35 4 adantr 
 |-  ( ( ph /\ X e. B ) -> B C_ ( Base ` M ) )
36 35 8 sseldd 
 |-  ( ( ph /\ X e. B ) -> ( ( invg ` S ) ` X ) e. ( Base ` M ) )
37 24 27 grpinvcl 
 |-  ( ( M e. Grp /\ X e. ( Base ` M ) ) -> ( ( invg ` M ) ` X ) e. ( Base ` M ) )
38 1 23 37 syl2an2r 
 |-  ( ( ph /\ X e. B ) -> ( ( invg ` M ) ` X ) e. ( Base ` M ) )
39 24 25 grprcan 
 |-  ( ( M e. Grp /\ ( ( ( invg ` S ) ` X ) e. ( Base ` M ) /\ ( ( invg ` M ) ` X ) e. ( Base ` M ) /\ X e. ( Base ` M ) ) ) -> ( ( ( ( invg ` S ) ` X ) ( +g ` M ) X ) = ( ( ( invg ` M ) ` X ) ( +g ` M ) X ) <-> ( ( invg ` S ) ` X ) = ( ( invg ` M ) ` X ) ) )
40 34 36 38 23 39 syl13anc 
 |-  ( ( ph /\ X e. B ) -> ( ( ( ( invg ` S ) ` X ) ( +g ` M ) X ) = ( ( ( invg ` M ) ` X ) ( +g ` M ) X ) <-> ( ( invg ` S ) ` X ) = ( ( invg ` M ) ` X ) ) )
41 33 40 mpbid 
 |-  ( ( ph /\ X e. B ) -> ( ( invg ` S ) ` X ) = ( ( invg ` M ) ` X ) )
42 41 ex 
 |-  ( ph -> ( X e. B -> ( ( invg ` S ) ` X ) = ( ( invg ` M ) ` X ) ) )