Proof of Theorem idomodle
| Step | Hyp | Ref
| Expression |
| 1 | | idomodle.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
| 2 | 1 | fvexi 6920 |
. . . 4
⊢ 𝐵 ∈ V |
| 3 | 2 | rabex 5339 |
. . 3
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ V |
| 4 | | hashxrcl 14396 |
. . 3
⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ V → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ∈
ℝ*) |
| 5 | 3, 4 | mp1i 13 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(♯‘{𝑥 ∈
𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ∈
ℝ*) |
| 6 | | fvex 6919 |
. . . 4
⊢
(Base‘𝑅)
∈ V |
| 7 | 6 | rabex 5339 |
. . 3
⊢ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ∈ V |
| 8 | | hashxrcl 14396 |
. . 3
⊢ ({𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ∈ V → (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ∈
ℝ*) |
| 9 | 7, 8 | mp1i 13 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(♯‘{𝑥 ∈
(Base‘𝑅) ∣
(𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ∈
ℝ*) |
| 10 | | nnre 12273 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 11 | 10 | rexrd 11311 |
. . 3
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ*) |
| 12 | 11 | adantl 481 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ*) |
| 13 | | isidom 20725 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
| 14 | 13 | simplbi 497 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
| 15 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ CRing) |
| 16 | | crngring 20242 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ Ring) |
| 18 | 17 | adantr 480 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ Ring) |
| 19 | | eqid 2737 |
. . . . . . . . 9
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
| 20 | | idomodle.g |
. . . . . . . . 9
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s
(Unit‘𝑅)) |
| 21 | 19, 20 | unitgrp 20383 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp) |
| 22 | 18, 21 | syl 17 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝐺 ∈ Grp) |
| 23 | | simpr 484 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
| 24 | | nnz 12634 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 25 | 24 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ ℤ) |
| 26 | | idomodle.o |
. . . . . . . 8
⊢ 𝑂 = (od‘𝐺) |
| 27 | | eqid 2737 |
. . . . . . . 8
⊢
(.g‘𝐺) = (.g‘𝐺) |
| 28 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 29 | 1, 26, 27, 28 | oddvds 19565 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑁 ∈ ℤ) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑁(.g‘𝐺)𝑥) = (0g‘𝐺))) |
| 30 | 22, 23, 25, 29 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑁(.g‘𝐺)𝑥) = (0g‘𝐺))) |
| 31 | | eqid 2737 |
. . . . . . . . . 10
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 32 | 19, 31 | unitsubm 20386 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(Unit‘𝑅) ∈
(SubMnd‘(mulGrp‘𝑅))) |
| 33 | 18, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → (Unit‘𝑅) ∈ (SubMnd‘(mulGrp‘𝑅))) |
| 34 | | nnnn0 12533 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 35 | 34 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈
ℕ0) |
| 36 | 19, 20 | unitgrpbas 20382 |
. . . . . . . . . 10
⊢
(Unit‘𝑅) =
(Base‘𝐺) |
| 37 | 1, 36 | eqtr4i 2768 |
. . . . . . . . 9
⊢ 𝐵 = (Unit‘𝑅) |
| 38 | 23, 37 | eleqtrdi 2851 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (Unit‘𝑅)) |
| 39 | | eqid 2737 |
. . . . . . . . 9
⊢
(.g‘(mulGrp‘𝑅)) =
(.g‘(mulGrp‘𝑅)) |
| 40 | 39, 20, 27 | submmulg 19136 |
. . . . . . . 8
⊢
(((Unit‘𝑅)
∈ (SubMnd‘(mulGrp‘𝑅)) ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ (Unit‘𝑅)) → (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (𝑁(.g‘𝐺)𝑥)) |
| 41 | 33, 35, 38, 40 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (𝑁(.g‘𝐺)𝑥)) |
| 42 | | eqid 2737 |
. . . . . . . . 9
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 43 | 19, 20, 42 | unitgrpid 20385 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(1r‘𝑅) =
(0g‘𝐺)) |
| 44 | 18, 43 | syl 17 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → (1r‘𝑅) = (0g‘𝐺)) |
| 45 | 41, 44 | eqeq12d 2753 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → ((𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅) ↔ (𝑁(.g‘𝐺)𝑥) = (0g‘𝐺))) |
| 46 | 30, 45 | bitr4d 282 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅))) |
| 47 | 46 | rabbidva 3443 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} = {𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) |
| 48 | 47 | fveq2d 6910 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(♯‘{𝑥 ∈
𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) = (♯‘{𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)})) |
| 49 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 50 | 49, 37 | unitss 20376 |
. . . . . 6
⊢ 𝐵 ⊆ (Base‘𝑅) |
| 51 | | rabss2 4078 |
. . . . . 6
⊢ (𝐵 ⊆ (Base‘𝑅) → {𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ⊆ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) |
| 52 | 50, 51 | mp1i 13 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → {𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ⊆ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) |
| 53 | | ssdomg 9040 |
. . . . 5
⊢ ({𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ∈ V → ({𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ⊆ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} → {𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ≼ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)})) |
| 54 | 7, 52, 53 | mpsyl 68 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → {𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ≼ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) |
| 55 | | hashdomi 14419 |
. . . 4
⊢ ({𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ≼ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ≤ (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)})) |
| 56 | 54, 55 | syl 17 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(♯‘{𝑥 ∈
𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ≤ (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)})) |
| 57 | 48, 56 | eqbrtrd 5165 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(♯‘{𝑥 ∈
𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ≤ (♯‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)})) |
| 58 | | simpl 482 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ IDomn) |
| 59 | 49, 42 | ringidcl 20262 |
. . . 4
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
| 60 | 17, 59 | syl 17 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(1r‘𝑅)
∈ (Base‘𝑅)) |
| 61 | | simpr 484 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ) |
| 62 | 49, 39 | idomrootle 26212 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧
(1r‘𝑅)
∈ (Base‘𝑅) ∧
𝑁 ∈ ℕ) →
(♯‘{𝑥 ∈
(Base‘𝑅) ∣
(𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ≤ 𝑁) |
| 63 | 58, 60, 61, 62 | syl3anc 1373 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(♯‘{𝑥 ∈
(Base‘𝑅) ∣
(𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ≤ 𝑁) |
| 64 | 5, 9, 12, 57, 63 | xrletrd 13204 |
1
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(♯‘{𝑥 ∈
𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ≤ 𝑁) |