ispgp

Description: A group is a P -group if every element has some power of P as its order. (Contributed by Mario Carneiro, 15-Jan-2015)

	Ref	Expression
Hypotheses	ispgp.1	$⊢ X = {Base}_{G}$
	ispgp.2	$⊢ O = od (G)$
Assertion	ispgp	$⊢ P pGrp G \leftrightarrow (P \in ℙ \land G \in Grp \land \forall x \in X \exists n \in ℕ_{0} O (x) = P^{n})$

Step	Hyp	Ref	Expression
1		ispgp.1	$⊢ X = {Base}_{G}$
2		ispgp.2	$⊢ O = od (G)$
3		simpr	$⊢ (p = P \land g = G) \to g = G$
4	3	fveq2d	$⊢ (p = P \land g = G) \to {Base}_{g} = {Base}_{G}$
5	4 1	eqtr4di	$⊢ (p = P \land g = G) \to {Base}_{g} = X$
6	3	fveq2d	$⊢ (p = P \land g = G) \to od (g) = od (G)$
7	6 2	eqtr4di	$⊢ (p = P \land g = G) \to od (g) = O$
8	7	fveq1d	$⊢ (p = P \land g = G) \to od (g) (x) = O (x)$
9		simpl	$⊢ (p = P \land g = G) \to p = P$
10	9	oveq1d	$⊢ (p = P \land g = G) \to p^{n} = P^{n}$
11	8 10	eqeq12d	$⊢ (p = P \land g = G) \to (od (g) (x) = p^{n} \leftrightarrow O (x) = P^{n})$
12	11	rexbidv	$⊢ (p = P \land g = G) \to (\exists n \in ℕ_{0} od (g) (x) = p^{n} \leftrightarrow \exists n \in ℕ_{0} O (x) = P^{n})$
13	5 12	raleqbidv	$⊢ (p = P \land g = G) \to (\forall x \in {Base}_{g} \exists n \in ℕ_{0} od (g) (x) = p^{n} \leftrightarrow \forall x \in X \exists n \in ℕ_{0} O (x) = P^{n})$
14		df-pgp	$⊢ pGrp = \{⟨p, g⟩ \| ((p \in ℙ \land g \in Grp) \land \forall x \in {Base}_{g} \exists n \in ℕ_{0} od (g) (x) = p^{n})\}$
15	13 14	brab2a	$⊢ P pGrp G \leftrightarrow ((P \in ℙ \land G \in Grp) \land \forall x \in X \exists n \in ℕ_{0} O (x) = P^{n})$
16		df-3an	$⊢ (P \in ℙ \land G \in Grp \land \forall x \in X \exists n \in ℕ_{0} O (x) = P^{n}) \leftrightarrow ((P \in ℙ \land G \in Grp) \land \forall x \in X \exists n \in ℕ_{0} O (x) = P^{n})$
17	15 16	bitr4i	$⊢ P pGrp G \leftrightarrow (P \in ℙ \land G \in Grp \land \forall x \in X \exists n \in ℕ_{0} O (x) = P^{n})$

Metamath Proof Explorer