subsubg

Description: A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015)

		Ref	Expression
	Hypothesis	subsubg.h	$⊢ H = G ↾_{𝑠} S$
	Assertion	subsubg	$⊢ S \in SubGrp (G) \to (A \in SubGrp (H) \leftrightarrow (A \in SubGrp (G) \land A \subseteq S))$

Proof

Step	Hyp	Ref	Expression
1		subsubg.h	$⊢ H = G ↾_{𝑠} S$
2		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
3	2	adantr	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to G \in Grp$
4		eqid	$⊢ {Base}_{H} = {Base}_{H}$
5	4	subgss	$⊢ A \in SubGrp (H) \to A \subseteq {Base}_{H}$
6	5	adantl	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to A \subseteq {Base}_{H}$
7	1	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{H}$
8	7	adantr	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to S = {Base}_{H}$
9	6 8	sseqtrrd	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to A \subseteq S$
10		eqid	$⊢ {Base}_{G} = {Base}_{G}$
11	10	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
12	11	adantr	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to S \subseteq {Base}_{G}$
13	9 12	sstrd	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to A \subseteq {Base}_{G}$
14	1	oveq1i	$⊢ H ↾_{𝑠} A = (G ↾_{𝑠} S) ↾_{𝑠} A$
15		ressabs	$⊢ (S \in SubGrp (G) \land A \subseteq S) \to (G ↾_{𝑠} S) ↾_{𝑠} A = G ↾_{𝑠} A$
16	14 15	eqtrid	$⊢ (S \in SubGrp (G) \land A \subseteq S) \to H ↾_{𝑠} A = G ↾_{𝑠} A$
17	9 16	syldan	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to H ↾_{𝑠} A = G ↾_{𝑠} A$
18		eqid	$⊢ H ↾_{𝑠} A = H ↾_{𝑠} A$
19	18	subggrp	$⊢ A \in SubGrp (H) \to H ↾_{𝑠} A \in Grp$
20	19	adantl	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to H ↾_{𝑠} A \in Grp$
21	17 20	eqeltrrd	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to G ↾_{𝑠} A \in Grp$
22	10	issubg	$⊢ A \in SubGrp (G) \leftrightarrow (G \in Grp \land A \subseteq {Base}_{G} \land G ↾_{𝑠} A \in Grp)$
23	3 13 21 22	syl3anbrc	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to A \in SubGrp (G)$
24	23 9	jca	$⊢ (S \in SubGrp (G) \land A \in SubGrp (H)) \to (A \in SubGrp (G) \land A \subseteq S)$
25	1	subggrp	$⊢ S \in SubGrp (G) \to H \in Grp$
26	25	adantr	$⊢ (S \in SubGrp (G) \land (A \in SubGrp (G) \land A \subseteq S)) \to H \in Grp$
27		simprr	$⊢ (S \in SubGrp (G) \land (A \in SubGrp (G) \land A \subseteq S)) \to A \subseteq S$
28	7	adantr	$⊢ (S \in SubGrp (G) \land (A \in SubGrp (G) \land A \subseteq S)) \to S = {Base}_{H}$
29	27 28	sseqtrd	$⊢ (S \in SubGrp (G) \land (A \in SubGrp (G) \land A \subseteq S)) \to A \subseteq {Base}_{H}$
30	16	adantrl	$⊢ (S \in SubGrp (G) \land (A \in SubGrp (G) \land A \subseteq S)) \to H ↾_{𝑠} A = G ↾_{𝑠} A$
31		eqid	$⊢ G ↾_{𝑠} A = G ↾_{𝑠} A$
32	31	subggrp	$⊢ A \in SubGrp (G) \to G ↾_{𝑠} A \in Grp$
33	32	ad2antrl	$⊢ (S \in SubGrp (G) \land (A \in SubGrp (G) \land A \subseteq S)) \to G ↾_{𝑠} A \in Grp$
34	30 33	eqeltrd	$⊢ (S \in SubGrp (G) \land (A \in SubGrp (G) \land A \subseteq S)) \to H ↾_{𝑠} A \in Grp$
35	4	issubg	$⊢ A \in SubGrp (H) \leftrightarrow (H \in Grp \land A \subseteq {Base}_{H} \land H ↾_{𝑠} A \in Grp)$
36	26 29 34 35	syl3anbrc	$⊢ (S \in SubGrp (G) \land (A \in SubGrp (G) \land A \subseteq S)) \to A \in SubGrp (H)$
37	24 36	impbida	$⊢ S \in SubGrp (G) \to (A \in SubGrp (H) \leftrightarrow (A \in SubGrp (G) \land A \subseteq S))$

Metamath Proof Explorer

Theorem subsubg

Proof