grpissubg

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 (base set of the) group is subgroup of the other group. (Contributed by AV, 14-Mar-2019)

	Ref	Expression
Hypotheses	grpissubg.b	$⊢ B = {Base}_{G}$
	grpissubg.s	$⊢ S = {Base}_{H}$
Assertion	grpissubg	$⊢ (G \in Grp \land H \in Grp) \to ((S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to S \in SubGrp (G))$

Proof

Step	Hyp	Ref	Expression
1		grpissubg.b	$⊢ B = {Base}_{G}$
2		grpissubg.s	$⊢ S = {Base}_{H}$
3		simpl	$⊢ (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to S \subseteq B$
4	3	adantl	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to S \subseteq B$
5	2	grpbn0	$⊢ H \in Grp \to S \neq \emptyset$
6	5	ad2antlr	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to S \neq \emptyset$
7		grpmnd	$⊢ G \in Grp \to G \in Mnd$
8		mndmgm	$⊢ G \in Mnd \to G \in Mgm$
9	7 8	syl	$⊢ G \in Grp \to G \in Mgm$
10		grpmnd	$⊢ H \in Grp \to H \in Mnd$
11		mndmgm	$⊢ H \in Mnd \to H \in Mgm$
12	10 11	syl	$⊢ H \in Grp \to H \in Mgm$
13	9 12	anim12i	$⊢ (G \in Grp \land H \in Grp) \to (G \in Mgm \land H \in Mgm)$
14	13	adantr	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to (G \in Mgm \land H \in Mgm)$
15	14	ad2antrr	$⊢ ((((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land a \in S) \land b \in S) \to (G \in Mgm \land H \in Mgm)$
16		simpr	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})$
17	16	ad2antrr	$⊢ ((((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land a \in S) \land b \in S) \to (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})$
18		simpr	$⊢ (((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land a \in S) \to a \in S$
19	18	anim1i	$⊢ ((((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land a \in S) \land b \in S) \to (a \in S \land b \in S)$
20	1 2	mgmsscl	$⊢ ((G \in Mgm \land H \in Mgm) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \land (a \in S \land b \in S)) \to a +_{G} b \in S$
21	15 17 19 20	syl3anc	$⊢ ((((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land a \in S) \land b \in S) \to a +_{G} b \in S$
22	21	ralrimiva	$⊢ (((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land a \in S) \to \forall b \in S a +_{G} b \in S$
23		simpl	$⊢ (G \in Grp \land H \in Grp) \to G \in Grp$
24	23	adantr	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to G \in Grp$
25		simplr	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to H \in Grp$
26	1	sseq2i	$⊢ S \subseteq B \leftrightarrow S \subseteq {Base}_{G}$
27	26	biimpi	$⊢ S \subseteq B \to S \subseteq {Base}_{G}$
28	27	adantr	$⊢ (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to S \subseteq {Base}_{G}$
29	28	adantl	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to S \subseteq {Base}_{G}$
30		ovres	$⊢ (x \in S \land y \in S) \to x ({+_{G} ↾}_{(S \times S)}) y = x +_{G} y$
31	30	adantl	$⊢ (((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land (x \in S \land y \in S)) \to x ({+_{G} ↾}_{(S \times S)}) y = x +_{G} y$
32		oveq	$⊢ +_{H} = {+_{G} ↾}_{(S \times S)} \to x +_{H} y = x ({+_{G} ↾}_{(S \times S)}) y$
33	32	adantl	$⊢ (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to x +_{H} y = x ({+_{G} ↾}_{(S \times S)}) y$
34	33	eqcomd	$⊢ (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to x ({+_{G} ↾}_{(S \times S)}) y = x +_{H} y$
35	34	ad2antlr	$⊢ (((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land (x \in S \land y \in S)) \to x ({+_{G} ↾}_{(S \times S)}) y = x +_{H} y$
36	31 35	eqtr3d	$⊢ (((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land (x \in S \land y \in S)) \to x +_{G} y = x +_{H} y$
37	36	ralrimivva	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to \forall x \in S \forall y \in S x +_{G} y = x +_{H} y$
38	24 25 2 29 37	grpinvssd	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to (a \in S \to {inv}_{g} (H) (a) = {inv}_{g} (G) (a))$
39	38	imp	$⊢ (((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land a \in S) \to {inv}_{g} (H) (a) = {inv}_{g} (G) (a)$
40		eqid	$⊢ {inv}_{g} (H) = {inv}_{g} (H)$
41	2 40	grpinvcl	$⊢ (H \in Grp \land a \in S) \to {inv}_{g} (H) (a) \in S$
42	41	ad4ant24	$⊢ (((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land a \in S) \to {inv}_{g} (H) (a) \in S$
43	39 42	eqeltrrd	$⊢ (((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land a \in S) \to {inv}_{g} (G) (a) \in S$
44	22 43	jca	$⊢ (((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \land a \in S) \to (\forall b \in S a +_{G} b \in S \land {inv}_{g} (G) (a) \in S)$
45	44	ralrimiva	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to \forall a \in S (\forall b \in S a +_{G} b \in S \land {inv}_{g} (G) (a) \in S)$
46		eqid	$⊢ +_{G} = +_{G}$
47		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
48	1 46 47	issubg2	$⊢ G \in Grp \to (S \in SubGrp (G) \leftrightarrow (S \subseteq B \land S \neq \emptyset \land \forall a \in S (\forall b \in S a +_{G} b \in S \land {inv}_{g} (G) (a) \in S)))$
49	48	ad2antrr	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to (S \in SubGrp (G) \leftrightarrow (S \subseteq B \land S \neq \emptyset \land \forall a \in S (\forall b \in S a +_{G} b \in S \land {inv}_{g} (G) (a) \in S)))$
50	4 6 45 49	mpbir3and	$⊢ ((G \in Grp \land H \in Grp) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to S \in SubGrp (G)$
51	50	ex	$⊢ (G \in Grp \land H \in Grp) \to ((S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to S \in SubGrp (G))$

Metamath Proof Explorer

Theorem grpissubg

Proof