Metamath Proof Explorer

Theorem odcau

Description: Cauchy's theorem for the order of an element in a group. A finite group whose order divides a prime P contains an element of order P . (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypotheses odcau.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
odcau.o ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion odcau ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → ∃ 𝑔 ∈ 𝑋 ( 𝑂 ‘ 𝑔 ) = 𝑃 )

Proof

Step Hyp Ref Expression
1 odcau.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcau.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → 𝐺 ∈ Grp )
4 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → 𝑋 ∈ Fin )
5 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → 𝑃 ∈ ℙ )
6 1nn0 ⊢ 1 ∈ ℕ0
7 6 a1i ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → 1 ∈ ℕ0 )
8 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
9 5 8 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → 𝑃 ∈ ℕ )
10 9 nncnd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → 𝑃 ∈ ℂ )
11 10 exp1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → ( 𝑃 ↑ 1 ) = 𝑃 )
12 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → 𝑃 ∥ ( ♯ ‘ 𝑋 ) )
13 11 12 eqbrtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → ( 𝑃 ↑ 1 ) ∥ ( ♯ ‘ 𝑋 ) )
14 1 3 4 5 7 13 sylow1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → ∃ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 1 ) )
15 11 eqeq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → ( ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 1 ) ↔ ( ♯ ‘ 𝑠 ) = 𝑃 ) )
16 15 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 1 ) ↔ ( ♯ ‘ 𝑠 ) = 𝑃 ) )
17 fvex ⊢ ( 0g ‘ 𝐺 ) ∈ V
18 hashsng ⊢ ( ( 0g ‘ 𝐺 ) ∈ V → ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = 1 )
19 17 18 ax-mp ⊢ ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = 1
20 simprr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ( ♯ ‘ 𝑠 ) = 𝑃 )
21 5 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → 𝑃 ∈ ℙ )
22 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
23 21 22 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
24 20 23 eqeltrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ( ♯ ‘ 𝑠 ) ∈ ( ℤ≥ ‘ 2 ) )
25 eluz2gt1 ⊢ ( ( ♯ ‘ 𝑠 ) ∈ ( ℤ≥ ‘ 2 ) → 1 < ( ♯ ‘ 𝑠 ) )
26 24 25 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → 1 < ( ♯ ‘ 𝑠 ) )
27 19 26 eqbrtrid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) < ( ♯ ‘ 𝑠 ) )
28 snfi ⊢ { ( 0g ‘ 𝐺 ) } ∈ Fin
29 4 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → 𝑋 ∈ Fin )
30 1 subgss ⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → 𝑠 ⊆ 𝑋 )
31 30 ad2antrl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → 𝑠 ⊆ 𝑋 )
32 29 31 ssfid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → 𝑠 ∈ Fin )
33 hashsdom ⊢ ( ( { ( 0g ‘ 𝐺 ) } ∈ Fin ∧ 𝑠 ∈ Fin ) → ( ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) < ( ♯ ‘ 𝑠 ) ↔ { ( 0g ‘ 𝐺 ) } ≺ 𝑠 ) )
34 28 32 33 sylancr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ( ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) < ( ♯ ‘ 𝑠 ) ↔ { ( 0g ‘ 𝐺 ) } ≺ 𝑠 ) )
35 27 34 mpbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → { ( 0g ‘ 𝐺 ) } ≺ 𝑠 )
36 sdomdif ⊢ ( { ( 0g ‘ 𝐺 ) } ≺ 𝑠 → ( 𝑠 ∖ { ( 0g ‘ 𝐺 ) } ) ≠ ∅ )
37 35 36 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ( 𝑠 ∖ { ( 0g ‘ 𝐺 ) } ) ≠ ∅ )
38 n0 ⊢ ( ( 𝑠 ∖ { ( 0g ‘ 𝐺 ) } ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝐺 ) } ) )
39 37 38 sylib ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ∃ 𝑔 𝑔 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝐺 ) } ) )
40 eldifsn ⊢ ( 𝑔 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝐺 ) } ) ↔ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) )
41 31 adantrr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → 𝑠 ⊆ 𝑋 )
42 simprrl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → 𝑔 ∈ 𝑠 )
43 41 42 sseldd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → 𝑔 ∈ 𝑋 )
44 simprrr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → 𝑔 ≠ ( 0g ‘ 𝐺 ) )
45 simprll ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → 𝑠 ∈ ( SubGrp ‘ 𝐺 ) )
46 32 adantrr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → 𝑠 ∈ Fin )
47 2 odsubdvds ⊢ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑠 ∈ Fin ∧ 𝑔 ∈ 𝑠 ) → ( 𝑂 ‘ 𝑔 ) ∥ ( ♯ ‘ 𝑠 ) )
48 45 46 42 47 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( 𝑂 ‘ 𝑔 ) ∥ ( ♯ ‘ 𝑠 ) )
49 simprlr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( ♯ ‘ 𝑠 ) = 𝑃 )
50 48 49 breqtrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( 𝑂 ‘ 𝑔 ) ∥ 𝑃 )
51 3 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → 𝐺 ∈ Grp )
52 4 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → 𝑋 ∈ Fin )
53 1 2 odcl2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑔 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑔 ) ∈ ℕ )
54 51 52 43 53 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( 𝑂 ‘ 𝑔 ) ∈ ℕ )
55 dvdsprime ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑂 ‘ 𝑔 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝑔 ) ∥ 𝑃 ↔ ( ( 𝑂 ‘ 𝑔 ) = 𝑃 ∨ ( 𝑂 ‘ 𝑔 ) = 1 ) ) )
56 5 54 55 syl2an2r ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( ( 𝑂 ‘ 𝑔 ) ∥ 𝑃 ↔ ( ( 𝑂 ‘ 𝑔 ) = 𝑃 ∨ ( 𝑂 ‘ 𝑔 ) = 1 ) ) )
57 50 56 mpbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( ( 𝑂 ‘ 𝑔 ) = 𝑃 ∨ ( 𝑂 ‘ 𝑔 ) = 1 ) )
58 57 ord ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( ¬ ( 𝑂 ‘ 𝑔 ) = 𝑃 → ( 𝑂 ‘ 𝑔 ) = 1 ) )
59 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
60 2 59 1 odeq1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑔 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝑔 ) = 1 ↔ 𝑔 = ( 0g ‘ 𝐺 ) ) )
61 3 43 60 syl2an2r ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( ( 𝑂 ‘ 𝑔 ) = 1 ↔ 𝑔 = ( 0g ‘ 𝐺 ) ) )
62 58 61 sylibd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( ¬ ( 𝑂 ‘ 𝑔 ) = 𝑃 → 𝑔 = ( 0g ‘ 𝐺 ) ) )
63 62 necon1ad ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( 𝑔 ≠ ( 0g ‘ 𝐺 ) → ( 𝑂 ‘ 𝑔 ) = 𝑃 ) )
64 44 63 mpd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( 𝑂 ‘ 𝑔 ) = 𝑃 )
65 43 64 jca ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ∧ ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) ) ) → ( 𝑔 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑔 ) = 𝑃 ) )
66 65 expr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ( ( 𝑔 ∈ 𝑠 ∧ 𝑔 ≠ ( 0g ‘ 𝐺 ) ) → ( 𝑔 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑔 ) = 𝑃 ) ) )
67 40 66 biimtrid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ( 𝑔 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝐺 ) } ) → ( 𝑔 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑔 ) = 𝑃 ) ) )
68 67 eximdv ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ( ∃ 𝑔 𝑔 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝐺 ) } ) → ∃ 𝑔 ( 𝑔 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑔 ) = 𝑃 ) ) )
69 39 68 mpd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ∃ 𝑔 ( 𝑔 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑔 ) = 𝑃 ) )
70 df-rex ⊢ ( ∃ 𝑔 ∈ 𝑋 ( 𝑂 ‘ 𝑔 ) = 𝑃 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑔 ) = 𝑃 ) )
71 69 70 sylibr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑠 ) = 𝑃 ) ) → ∃ 𝑔 ∈ 𝑋 ( 𝑂 ‘ 𝑔 ) = 𝑃 )
72 71 expr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑠 ) = 𝑃 → ∃ 𝑔 ∈ 𝑋 ( 𝑂 ‘ 𝑔 ) = 𝑃 ) )
73 16 72 sylbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) ∧ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 1 ) → ∃ 𝑔 ∈ 𝑋 ( 𝑂 ‘ 𝑔 ) = 𝑃 ) )
74 73 rexlimdva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → ( ∃ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 1 ) → ∃ 𝑔 ∈ 𝑋 ( 𝑂 ‘ 𝑔 ) = 𝑃 ) )
75 14 74 mpd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) ∧ 𝑃 ∥ ( ♯ ‘ 𝑋 ) ) → ∃ 𝑔 ∈ 𝑋 ( 𝑂 ‘ 𝑔 ) = 𝑃 )