Theorem grpinvssd 12798

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

Hypotheses

Ref	Expression
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

Ref	Expression
grpinvssd	|- ( ph -> ( X e. B -> ( ( invg ` S ) ` X ) = ( ( invg ` M ) ` X ) ) )

Distinct variable groups:   x, B, y   x, M, y   x, S, y   x, X, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem grpinvssd

Step	Hyp	Ref	Expression
1		grpidssd.s	. . . . . 6 |- ( ph -> S e. Grp )
2		grpidssd.b	. . . . . . 7 |- B = ( Base ` S )
3		eqid 2171	. . . . . . 7 |- ( invg ` S ) = ( invg ` S )
4	2, 3	grpinvcl 12773	. . . . . 6 |- ( ( S e. Grp /\ X e. B ) -> ( ( invg ` S ) ` X ) e. B )
5	1, 4	sylan 281	. . . . 5 |- ( ( ph /\ X e. B ) -> ( ( invg ` S ) ` X ) e. B )
6		simpr 109	. . . . 5 |- ( ( ph /\ X e. B ) -> X e. B )
7		grpidssd.o	. . . . . 6 |- ( ph -> A. x e. B A. y e. B ( x ( +g ` M ) y ) = ( x ( +g ` S ) y ) )
8	7	adantr 274	. . . . 5 |- ( ( ph /\ X e. B ) -> A. x e. B A. y e. B ( x ( +g ` M ) y ) = ( x ( +g ` S ) y ) )
9		oveq1 5864	. . . . . . 7 |- ( x = ( ( invg ` S ) ` X ) -> ( x ( +g ` M ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` M ) y ) )
10		oveq1 5864	. . . . . . 7 |- ( x = ( ( invg ` S ) ` X ) -> ( x ( +g ` S ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) y ) )
11	9, 10	eqeq12d 2186	. . . . . 6 |- ( x = ( ( invg ` S ) ` X ) -> ( ( x ( +g ` M ) y ) = ( x ( +g ` S ) y ) <-> ( ( ( invg ` S ) ` X ) ( +g ` M ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) y ) ) )
12		oveq2 5865	. . . . . . 7 |- ( y = X -> ( ( ( invg ` S ) ` X ) ( +g ` M ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` M ) X ) )
13		oveq2 5865	. . . . . . 7 |- ( y = X -> ( ( ( invg ` S ) ` X ) ( +g ` S ) y ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) X ) )
14	12, 13	eqeq12d 2186	. . . . . 6 |- ( 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 ) ) )
15	11, 14	rspc2va 2849	. . . . 5 |- ( ( ( ( ( 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 ) )
16	5, 6, 8, 15	syl21anc 1233	. . . 4 |- ( ( ph /\ X e. B ) -> ( ( ( invg ` S ) ` X ) ( +g ` M ) X ) = ( ( ( invg ` S ) ` X ) ( +g ` S ) X ) )
17		eqid 2171	. . . . . 6 |- ( +g ` S ) = ( +g ` S )
18		eqid 2171	. . . . . 6 |- ( 0g ` S ) = ( 0g ` S )
19	2, 17, 18, 3	grplinv 12774	. . . . 5 |- ( ( S e. Grp /\ X e. B ) -> ( ( ( invg ` S ) ` X ) ( +g ` S ) X ) = ( 0g ` S ) )
20	1, 19	sylan 281	. . . 4 |- ( ( ph /\ X e. B ) -> ( ( ( invg ` S ) ` X ) ( +g ` S ) X ) = ( 0g ` S ) )
21		grpidssd.m	. . . . . 6 |- ( ph -> M e. Grp )
22		grpidssd.c	. . . . . . 7 |- ( ph -> B C_ ( Base ` M ) )
23	22	sselda 3148	. . . . . 6 |- ( ( ph /\ X e. B ) -> X e. ( Base ` M ) )
24		eqid 2171	. . . . . . 7 |- ( Base ` M ) = ( Base ` M )
25		eqid 2171	. . . . . . 7 |- ( +g ` M ) = ( +g ` M )
26		eqid 2171	. . . . . . 7 |- ( 0g ` M ) = ( 0g ` M )
27		eqid 2171	. . . . . . 7 |- ( invg ` M ) = ( invg ` M )
28	24, 25, 26, 27	grplinv 12774	. . . . . 6 |- ( ( M e. Grp /\ X e. ( Base ` M ) ) -> ( ( ( invg ` M ) ` X ) ( +g ` M ) X ) = ( 0g ` M ) )
29	21, 23, 28	syl2an2r 591	. . . . 5 |- ( ( ph /\ X e. B ) -> ( ( ( invg ` M ) ` X ) ( +g ` M ) X ) = ( 0g ` M ) )
30	21, 1, 2, 22, 7	grpidssd 12797	. . . . . 6 |- ( ph -> ( 0g ` M ) = ( 0g ` S ) )
31	30	adantr 274	. . . . 5 |- ( ( ph /\ X e. B ) -> ( 0g ` M ) = ( 0g ` S ) )
32	29, 31	eqtr2d 2205	. . . 4 |- ( ( ph /\ X e. B ) -> ( 0g ` S ) = ( ( ( invg ` M ) ` X ) ( +g ` M ) X ) )
33	16, 20, 32	3eqtrd 2208	. . 3 |- ( ( ph /\ X e. B ) -> ( ( ( invg ` S ) ` X ) ( +g ` M ) X ) = ( ( ( invg ` M ) ` X ) ( +g ` M ) X ) )
34	21	adantr 274	. . . 4 |- ( ( ph /\ X e. B ) -> M e. Grp )
35	22	adantr 274	. . . . 5 |- ( ( ph /\ X e. B ) -> B C_ ( Base ` M ) )
36	35, 5	sseldd 3149	. . . 4 |- ( ( ph /\ X e. B ) -> ( ( invg ` S ) ` X ) e. ( Base ` M ) )
37	24, 27	grpinvcl 12773	. . . . 5 |- ( ( M e. Grp /\ X e. ( Base ` M ) ) -> ( ( invg ` M ) ` X ) e. ( Base ` M ) )
38	21, 23, 37	syl2an2r 591	. . . 4 |- ( ( ph /\ X e. B ) -> ( ( invg ` M ) ` X ) e. ( Base ` M ) )
39	24, 25	grprcan 12762	. . . 4 |- ( ( 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 1236	. . 3 |- ( ( 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 146	. 2 |- ( ( ph /\ X e. B ) -> ( ( invg ` S ) ` X ) = ( ( invg ` M ) ` X ) )
42	41	ex 114	1 |- ( ph -> ( X e. B -> ( ( invg ` S ) ` X ) = ( ( invg ` M ) ` X ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1349   e. wcel 2142   A.wral 2449   C_ wss 3122   ` cfv 5200  (class class class)co 5857   Basecbs 12420   +g cplusg 12484   0gc0g 12618   Grpcgrp 12730   invgcminusg 12731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-coll 4105  ax-sep 4108  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-cnex 7869  ax-resscn 7870  ax-1re 7872  ax-addrcl 7875

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-reu 2456  df-rmo 2457  df-rab 2458  df-v 2733  df-sbc 2957  df-csb 3051  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-iun 3876  df-br 3991  df-opab 4052  df-mpt 4053  df-id 4279  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-f1 5205  df-fo 5206  df-f1o 5207  df-fv 5208  df-riota 5813  df-ov 5860  df-inn 8883  df-2 8941  df-ndx 12423  df-slot 12424  df-base 12426  df-plusg 12497  df-0g 12620  df-mgm 12632  df-sgrp 12665  df-mnd 12675  df-grp 12733  df-minusg 12734

This theorem is referenced by: (None)