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	$⊢ φ \to M \in Grp$
	grpidssd.s	$⊢ φ \to S \in Grp$
	grpidssd.b	$⊢ B = {Base}_{S}$
	grpidssd.c	$⊢ φ \to B \subseteq {Base}_{M}$
	grpidssd.o	$⊢ φ \to \forall x \in B \forall y \in B x +_{M} y = x +_{S} y$
Assertion	grpinvssd	$⊢ φ \to (X \in B \to {inv}_{g} (S) (X) = {inv}_{g} (M) (X))$

Proof

Step	Hyp	Ref	Expression
1		grpidssd.m	$⊢ φ \to M \in Grp$
2		grpidssd.s	$⊢ φ \to S \in Grp$
3		grpidssd.b	$⊢ B = {Base}_{S}$
4		grpidssd.c	$⊢ φ \to B \subseteq {Base}_{M}$
5		grpidssd.o	$⊢ φ \to \forall x \in B \forall y \in B x +_{M} y = x +_{S} y$
6		eqid	$⊢ {inv}_{g} (S) = {inv}_{g} (S)$
7	3 6	grpinvcl	$⊢ (S \in Grp \land X \in B) \to {inv}_{g} (S) (X) \in B$
8	2 7	sylan	$⊢ (φ \land X \in B) \to {inv}_{g} (S) (X) \in B$
9		simpr	$⊢ (φ \land X \in B) \to X \in B$
10	5	adantr	$⊢ (φ \land X \in B) \to \forall x \in B \forall y \in B x +_{M} y = x +_{S} y$
11		oveq1	$⊢ x = {inv}_{g} (S) (X) \to x +_{M} y = {inv}_{g} (S) (X) +_{M} y$
12		oveq1	$⊢ x = {inv}_{g} (S) (X) \to x +_{S} y = {inv}_{g} (S) (X) +_{S} y$
13	11 12	eqeq12d	$⊢ x = {inv}_{g} (S) (X) \to (x +_{M} y = x +_{S} y \leftrightarrow {inv}_{g} (S) (X) +_{M} y = {inv}_{g} (S) (X) +_{S} y)$
14		oveq2	$⊢ y = X \to {inv}_{g} (S) (X) +_{M} y = {inv}_{g} (S) (X) +_{M} X$
15		oveq2	$⊢ y = X \to {inv}_{g} (S) (X) +_{S} y = {inv}_{g} (S) (X) +_{S} X$
16	14 15	eqeq12d	$⊢ y = X \to ({inv}_{g} (S) (X) +_{M} y = {inv}_{g} (S) (X) +_{S} y \leftrightarrow {inv}_{g} (S) (X) +_{M} X = {inv}_{g} (S) (X) +_{S} X)$
17	13 16	rspc2va	$⊢ (({inv}_{g} (S) (X) \in B \land X \in B) \land \forall x \in B \forall y \in B x +_{M} y = x +_{S} y) \to {inv}_{g} (S) (X) +_{M} X = {inv}_{g} (S) (X) +_{S} X$
18	8 9 10 17	syl21anc	$⊢ (φ \land X \in B) \to {inv}_{g} (S) (X) +_{M} X = {inv}_{g} (S) (X) +_{S} X$
19		eqid	$⊢ +_{S} = +_{S}$
20		eqid	$⊢ 0_{S} = 0_{S}$
21	3 19 20 6	grplinv	$⊢ (S \in Grp \land X \in B) \to {inv}_{g} (S) (X) +_{S} X = 0_{S}$
22	2 21	sylan	$⊢ (φ \land X \in B) \to {inv}_{g} (S) (X) +_{S} X = 0_{S}$
23	4	sselda	$⊢ (φ \land X \in B) \to X \in {Base}_{M}$
24		eqid	$⊢ {Base}_{M} = {Base}_{M}$
25		eqid	$⊢ +_{M} = +_{M}$
26		eqid	$⊢ 0_{M} = 0_{M}$
27		eqid	$⊢ {inv}_{g} (M) = {inv}_{g} (M)$
28	24 25 26 27	grplinv	$⊢ (M \in Grp \land X \in {Base}_{M}) \to {inv}_{g} (M) (X) +_{M} X = 0_{M}$
29	1 23 28	syl2an2r	$⊢ (φ \land X \in B) \to {inv}_{g} (M) (X) +_{M} X = 0_{M}$
30	1 2 3 4 5	grpidssd	$⊢ φ \to 0_{M} = 0_{S}$
31	30	adantr	$⊢ (φ \land X \in B) \to 0_{M} = 0_{S}$
32	29 31	eqtr2d	$⊢ (φ \land X \in B) \to 0_{S} = {inv}_{g} (M) (X) +_{M} X$
33	18 22 32	3eqtrd	$⊢ (φ \land X \in B) \to {inv}_{g} (S) (X) +_{M} X = {inv}_{g} (M) (X) +_{M} X$
34	1	adantr	$⊢ (φ \land X \in B) \to M \in Grp$
35	4	adantr	$⊢ (φ \land X \in B) \to B \subseteq {Base}_{M}$
36	35 8	sseldd	$⊢ (φ \land X \in B) \to {inv}_{g} (S) (X) \in {Base}_{M}$
37	24 27	grpinvcl	$⊢ (M \in Grp \land X \in {Base}_{M}) \to {inv}_{g} (M) (X) \in {Base}_{M}$
38	1 23 37	syl2an2r	$⊢ (φ \land X \in B) \to {inv}_{g} (M) (X) \in {Base}_{M}$
39	24 25	grprcan	$⊢ (M \in Grp \land ({inv}_{g} (S) (X) \in {Base}_{M} \land {inv}_{g} (M) (X) \in {Base}_{M} \land X \in {Base}_{M})) \to ({inv}_{g} (S) (X) +_{M} X = {inv}_{g} (M) (X) +_{M} X \leftrightarrow {inv}_{g} (S) (X) = {inv}_{g} (M) (X))$
40	34 36 38 23 39	syl13anc	$⊢ (φ \land X \in B) \to ({inv}_{g} (S) (X) +_{M} X = {inv}_{g} (M) (X) +_{M} X \leftrightarrow {inv}_{g} (S) (X) = {inv}_{g} (M) (X))$
41	33 40	mpbid	$⊢ (φ \land X \in B) \to {inv}_{g} (S) (X) = {inv}_{g} (M) (X)$
42	41	ex	$⊢ φ \to (X \in B \to {inv}_{g} (S) (X) = {inv}_{g} (M) (X))$

Metamath Proof Explorer

Theorem grpinvssd

Proof