subgpgp

Description: A subgroup of a p-group is a p-group. (Contributed by Mario Carneiro, 27-Apr-2016)

		Ref	Expression
	Assertion	subgpgp	$⊢ (P pGrp G \land S \in SubGrp (G)) \to P pGrp (G ↾_{𝑠} S)$

Proof

Step	Hyp	Ref	Expression
1		pgpprm	$⊢ P pGrp G \to P \in ℙ$
2	1	adantr	$⊢ (P pGrp G \land S \in SubGrp (G)) \to P \in ℙ$
3		eqid	$⊢ G ↾_{𝑠} S = G ↾_{𝑠} S$
4	3	subggrp	$⊢ S \in SubGrp (G) \to G ↾_{𝑠} S \in Grp$
5	4	adantl	$⊢ (P pGrp G \land S \in SubGrp (G)) \to G ↾_{𝑠} S \in Grp$
6		eqid	$⊢ {Base}_{G} = {Base}_{G}$
7		eqid	$⊢ od (G) = od (G)$
8	6 7	ispgp	$⊢ P pGrp G \leftrightarrow (P \in ℙ \land G \in Grp \land \forall x \in {Base}_{G} \exists n \in ℕ_{0} od (G) (x) = P^{n})$
9	8	simp3bi	$⊢ P pGrp G \to \forall x \in {Base}_{G} \exists n \in ℕ_{0} od (G) (x) = P^{n}$
10	9	adantr	$⊢ (P pGrp G \land S \in SubGrp (G)) \to \forall x \in {Base}_{G} \exists n \in ℕ_{0} od (G) (x) = P^{n}$
11	6	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
12	11	adantl	$⊢ (P pGrp G \land S \in SubGrp (G)) \to S \subseteq {Base}_{G}$
13		ssralv	$⊢ S \subseteq {Base}_{G} \to (\forall x \in {Base}_{G} \exists n \in ℕ_{0} od (G) (x) = P^{n} \to \forall x \in S \exists n \in ℕ_{0} od (G) (x) = P^{n})$
14	12 13	syl	$⊢ (P pGrp G \land S \in SubGrp (G)) \to (\forall x \in {Base}_{G} \exists n \in ℕ_{0} od (G) (x) = P^{n} \to \forall x \in S \exists n \in ℕ_{0} od (G) (x) = P^{n})$
15		eqid	$⊢ od (G ↾_{𝑠} S) = od (G ↾_{𝑠} S)$
16	3 7 15	subgod	$⊢ (S \in SubGrp (G) \land x \in S) \to od (G) (x) = od (G ↾_{𝑠} S) (x)$
17	16	adantll	$⊢ ((P pGrp G \land S \in SubGrp (G)) \land x \in S) \to od (G) (x) = od (G ↾_{𝑠} S) (x)$
18	17	eqeq1d	$⊢ ((P pGrp G \land S \in SubGrp (G)) \land x \in S) \to (od (G) (x) = P^{n} \leftrightarrow od (G ↾_{𝑠} S) (x) = P^{n})$
19	18	rexbidv	$⊢ ((P pGrp G \land S \in SubGrp (G)) \land x \in S) \to (\exists n \in ℕ_{0} od (G) (x) = P^{n} \leftrightarrow \exists n \in ℕ_{0} od (G ↾_{𝑠} S) (x) = P^{n})$
20	19	ralbidva	$⊢ (P pGrp G \land S \in SubGrp (G)) \to (\forall x \in S \exists n \in ℕ_{0} od (G) (x) = P^{n} \leftrightarrow \forall x \in S \exists n \in ℕ_{0} od (G ↾_{𝑠} S) (x) = P^{n})$
21	14 20	sylibd	$⊢ (P pGrp G \land S \in SubGrp (G)) \to (\forall x \in {Base}_{G} \exists n \in ℕ_{0} od (G) (x) = P^{n} \to \forall x \in S \exists n \in ℕ_{0} od (G ↾_{𝑠} S) (x) = P^{n})$
22	10 21	mpd	$⊢ (P pGrp G \land S \in SubGrp (G)) \to \forall x \in S \exists n \in ℕ_{0} od (G ↾_{𝑠} S) (x) = P^{n}$
23	3	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{(G ↾_{𝑠} S)}$
24	23	adantl	$⊢ (P pGrp G \land S \in SubGrp (G)) \to S = {Base}_{(G ↾_{𝑠} S)}$
25	22 24	raleqtrdv	$⊢ (P pGrp G \land S \in SubGrp (G)) \to \forall x \in {Base}_{(G ↾_{𝑠} S)} \exists n \in ℕ_{0} od (G ↾_{𝑠} S) (x) = P^{n}$
26		eqid	$⊢ {Base}_{(G ↾_{𝑠} S)} = {Base}_{(G ↾_{𝑠} S)}$
27	26 15	ispgp	$⊢ P pGrp (G ↾_{𝑠} S) \leftrightarrow (P \in ℙ \land G ↾_{𝑠} S \in Grp \land \forall x \in {Base}_{(G ↾_{𝑠} S)} \exists n \in ℕ_{0} od (G ↾_{𝑠} S) (x) = P^{n})$
28	2 5 25 27	syl3anbrc	$⊢ (P pGrp G \land S \in SubGrp (G)) \to P pGrp (G ↾_{𝑠} S)$

Metamath Proof Explorer

Theorem subgpgp

Proof