Step |
Hyp |
Ref |
Expression |
1 |
|
odf1.1 |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
odf1.2 |
⊢ 𝑂 = ( od ‘ 𝐺 ) |
3 |
|
odf1.3 |
⊢ · = ( .g ‘ 𝐺 ) |
4 |
|
odf1.4 |
⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) |
5 |
|
znnen |
⊢ ℤ ≈ ℕ |
6 |
|
nnenom |
⊢ ℕ ≈ ω |
7 |
5 6
|
entr2i |
⊢ ω ≈ ℤ |
8 |
1 2 3 4
|
odf1 |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 ↔ 𝐹 : ℤ –1-1→ 𝑋 ) ) |
9 |
8
|
biimp3a |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → 𝐹 : ℤ –1-1→ 𝑋 ) |
10 |
|
f1f |
⊢ ( 𝐹 : ℤ –1-1→ 𝑋 → 𝐹 : ℤ ⟶ 𝑋 ) |
11 |
|
zex |
⊢ ℤ ∈ V |
12 |
1
|
fvexi |
⊢ 𝑋 ∈ V |
13 |
|
fex2 |
⊢ ( ( 𝐹 : ℤ ⟶ 𝑋 ∧ ℤ ∈ V ∧ 𝑋 ∈ V ) → 𝐹 ∈ V ) |
14 |
11 12 13
|
mp3an23 |
⊢ ( 𝐹 : ℤ ⟶ 𝑋 → 𝐹 ∈ V ) |
15 |
9 10 14
|
3syl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → 𝐹 ∈ V ) |
16 |
|
f1f1orn |
⊢ ( 𝐹 : ℤ –1-1→ 𝑋 → 𝐹 : ℤ –1-1-onto→ ran 𝐹 ) |
17 |
9 16
|
syl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → 𝐹 : ℤ –1-1-onto→ ran 𝐹 ) |
18 |
|
f1oen3g |
⊢ ( ( 𝐹 ∈ V ∧ 𝐹 : ℤ –1-1-onto→ ran 𝐹 ) → ℤ ≈ ran 𝐹 ) |
19 |
15 17 18
|
syl2anc |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ℤ ≈ ran 𝐹 ) |
20 |
|
entr |
⊢ ( ( ω ≈ ℤ ∧ ℤ ≈ ran 𝐹 ) → ω ≈ ran 𝐹 ) |
21 |
7 19 20
|
sylancr |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ω ≈ ran 𝐹 ) |
22 |
|
endom |
⊢ ( ω ≈ ran 𝐹 → ω ≼ ran 𝐹 ) |
23 |
|
domnsym |
⊢ ( ω ≼ ran 𝐹 → ¬ ran 𝐹 ≺ ω ) |
24 |
21 22 23
|
3syl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ¬ ran 𝐹 ≺ ω ) |
25 |
|
isfinite |
⊢ ( ran 𝐹 ∈ Fin ↔ ran 𝐹 ≺ ω ) |
26 |
24 25
|
sylnibr |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ¬ ran 𝐹 ∈ Fin ) |