Theorem 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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	ispgp.2	⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion	ispgp	⊢ ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ ℕ0 ( 𝑂 ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ispgp.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		ispgp.2	⊢ 𝑂 = ( od ‘ 𝐺 )
3		simpr	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
4	3	fveq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
5	4 1	eqtr4di	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( Base ‘ 𝑔 ) = 𝑋 )
6	3	fveq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( od ‘ 𝑔 ) = ( od ‘ 𝐺 ) )
7	6 2	eqtr4di	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( od ‘ 𝑔 ) = 𝑂 )
8	7	fveq1d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑂 ‘ 𝑥 ) )
9		simpl	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → 𝑝 = 𝑃 )
10	9	oveq1d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( 𝑝 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑛 ) )
11	8 10	eqeq12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 ) ↔ ( 𝑂 ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
12	11	rexbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ( 𝑂 ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
13	5 12	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ ℕ0 ( 𝑂 ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
14		df-pgp	⊢ pGrp = { ⟨ 𝑝 , 𝑔 ⟩ ∣ ( ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 ) ) }
15	13 14	brab2a	⊢ ( 𝑃 pGrp 𝐺 ↔ ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ ℕ0 ( 𝑂 ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
16		df-3an	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ ℕ0 ( 𝑂 ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) ↔ ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ ℕ0 ( 𝑂 ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
17	15 16	bitr4i	⊢ ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ ℕ0 ( 𝑂 ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )