Step |
Hyp |
Ref |
Expression |
1 |
|
hashcl |
⊢ ( 𝑆 ∈ Fin → ( ♯ ‘ 𝑆 ) ∈ ℕ0 ) |
2 |
1
|
adantl |
⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ♯ ‘ 𝑆 ) ∈ ℕ0 ) |
3 |
|
eqid |
⊢ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) = ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) |
4 |
3
|
zncrng |
⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 → ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ CRing ) |
5 |
|
crngring |
⊢ ( ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ CRing → ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ Ring ) |
6 |
|
ringabl |
⊢ ( ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ Ring → ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ Abel ) |
7 |
2 4 5 6
|
4syl |
⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ Abel ) |
8 |
|
hashnncl |
⊢ ( 𝑆 ∈ Fin → ( ( ♯ ‘ 𝑆 ) ∈ ℕ ↔ 𝑆 ≠ ∅ ) ) |
9 |
8
|
biimparc |
⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ♯ ‘ 𝑆 ) ∈ ℕ ) |
10 |
|
eqid |
⊢ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) = ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) |
11 |
3 10
|
znhash |
⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ → ( ♯ ‘ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) = ( ♯ ‘ 𝑆 ) ) |
12 |
9 11
|
syl |
⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ♯ ‘ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) = ( ♯ ‘ 𝑆 ) ) |
13 |
12
|
eqcomd |
⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) ) |
14 |
|
simpr |
⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → 𝑆 ∈ Fin ) |
15 |
3 10
|
znfi |
⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ → ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ∈ Fin ) |
16 |
9 15
|
syl |
⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ∈ Fin ) |
17 |
|
hashen |
⊢ ( ( 𝑆 ∈ Fin ∧ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ∈ Fin ) → ( ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) ↔ 𝑆 ≈ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) ) |
18 |
14 16 17
|
syl2anc |
⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) ↔ 𝑆 ≈ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) ) |
19 |
13 18
|
mpbid |
⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → 𝑆 ≈ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) |
20 |
10
|
isnumbasgrplem1 |
⊢ ( ( ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ Abel ∧ 𝑆 ≈ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) → 𝑆 ∈ ( Base “ Abel ) ) |
21 |
7 19 20
|
syl2anc |
⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → 𝑆 ∈ ( Base “ Abel ) ) |
22 |
21
|
adantll |
⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ 𝑆 ∈ Fin ) → 𝑆 ∈ ( Base “ Abel ) ) |
23 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
24 |
|
eqid |
⊢ ( ℤ/nℤ ‘ 2 ) = ( ℤ/nℤ ‘ 2 ) |
25 |
24
|
zncrng |
⊢ ( 2 ∈ ℕ0 → ( ℤ/nℤ ‘ 2 ) ∈ CRing ) |
26 |
|
crngring |
⊢ ( ( ℤ/nℤ ‘ 2 ) ∈ CRing → ( ℤ/nℤ ‘ 2 ) ∈ Ring ) |
27 |
23 25 26
|
mp2b |
⊢ ( ℤ/nℤ ‘ 2 ) ∈ Ring |
28 |
|
eqid |
⊢ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) = ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) |
29 |
28
|
frlmlmod |
⊢ ( ( ( ℤ/nℤ ‘ 2 ) ∈ Ring ∧ 𝑆 ∈ dom card ) → ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ LMod ) |
30 |
27 29
|
mpan |
⊢ ( 𝑆 ∈ dom card → ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ LMod ) |
31 |
|
lmodabl |
⊢ ( ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ LMod → ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ Abel ) |
32 |
30 31
|
syl |
⊢ ( 𝑆 ∈ dom card → ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ Abel ) |
33 |
32
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ Abel ) |
34 |
|
eqid |
⊢ ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) = ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) |
35 |
24 28 34
|
frlmpwfi |
⊢ ( 𝑆 ∈ dom card → ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ≈ ( 𝒫 𝑆 ∩ Fin ) ) |
36 |
35
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ≈ ( 𝒫 𝑆 ∩ Fin ) ) |
37 |
|
simpll |
⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → 𝑆 ∈ dom card ) |
38 |
|
numinfctb |
⊢ ( ( 𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin ) → ω ≼ 𝑆 ) |
39 |
38
|
adantlr |
⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → ω ≼ 𝑆 ) |
40 |
|
infpwfien |
⊢ ( ( 𝑆 ∈ dom card ∧ ω ≼ 𝑆 ) → ( 𝒫 𝑆 ∩ Fin ) ≈ 𝑆 ) |
41 |
37 39 40
|
syl2anc |
⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → ( 𝒫 𝑆 ∩ Fin ) ≈ 𝑆 ) |
42 |
|
entr |
⊢ ( ( ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ≈ ( 𝒫 𝑆 ∩ Fin ) ∧ ( 𝒫 𝑆 ∩ Fin ) ≈ 𝑆 ) → ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ≈ 𝑆 ) |
43 |
36 41 42
|
syl2anc |
⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ≈ 𝑆 ) |
44 |
43
|
ensymd |
⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → 𝑆 ≈ ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ) |
45 |
34
|
isnumbasgrplem1 |
⊢ ( ( ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ Abel ∧ 𝑆 ≈ ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ) → 𝑆 ∈ ( Base “ Abel ) ) |
46 |
33 44 45
|
syl2anc |
⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → 𝑆 ∈ ( Base “ Abel ) ) |
47 |
22 46
|
pm2.61dan |
⊢ ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) → 𝑆 ∈ ( Base “ Abel ) ) |