This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑂 ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )