Proof of Theorem idomodle
Step | Hyp | Ref
| Expression |
1 | | idomodle.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
2 | | fvex 6201 |
. . . . 5
⊢
(Base‘𝐺)
∈ V |
3 | 1, 2 | eqeltri 2697 |
. . . 4
⊢ 𝐵 ∈ V |
4 | 3 | rabex 4813 |
. . 3
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ V |
5 | | hashxrcl 13148 |
. . 3
⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ V → (#‘{𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ∈
ℝ*) |
6 | 4, 5 | mp1i 13 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(#‘{𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ∈
ℝ*) |
7 | | fvex 6201 |
. . . 4
⊢
(Base‘𝑅)
∈ V |
8 | 7 | rabex 4813 |
. . 3
⊢ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ∈ V |
9 | | hashxrcl 13148 |
. . 3
⊢ ({𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ∈ V → (#‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ∈
ℝ*) |
10 | 8, 9 | mp1i 13 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(#‘{𝑥 ∈
(Base‘𝑅) ∣
(𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ∈
ℝ*) |
11 | | nnre 11027 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
12 | 11 | rexrd 10089 |
. . 3
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ*) |
13 | 12 | adantl 482 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ*) |
14 | | isidom 19304 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
15 | 14 | simplbi 476 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
16 | 15 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ CRing) |
17 | | crngring 18558 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ Ring) |
19 | 18 | adantr 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ Ring) |
20 | | eqid 2622 |
. . . . . . . . 9
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
21 | | idomodle.g |
. . . . . . . . 9
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s
(Unit‘𝑅)) |
22 | 20, 21 | unitgrp 18667 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp) |
23 | 19, 22 | syl 17 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝐺 ∈ Grp) |
24 | | simpr 477 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
25 | | nnz 11399 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
26 | 25 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ ℤ) |
27 | | idomodle.o |
. . . . . . . 8
⊢ 𝑂 = (od‘𝐺) |
28 | | eqid 2622 |
. . . . . . . 8
⊢
(.g‘𝐺) = (.g‘𝐺) |
29 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
30 | 1, 27, 28, 29 | oddvds 17966 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑁 ∈ ℤ) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑁(.g‘𝐺)𝑥) = (0g‘𝐺))) |
31 | 23, 24, 26, 30 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑁(.g‘𝐺)𝑥) = (0g‘𝐺))) |
32 | | eqid 2622 |
. . . . . . . . . 10
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
33 | 20, 32 | unitsubm 18670 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(Unit‘𝑅) ∈
(SubMnd‘(mulGrp‘𝑅))) |
34 | 19, 33 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → (Unit‘𝑅) ∈ (SubMnd‘(mulGrp‘𝑅))) |
35 | | nnnn0 11299 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
36 | 35 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈
ℕ0) |
37 | 20, 21 | unitgrpbas 18666 |
. . . . . . . . . 10
⊢
(Unit‘𝑅) =
(Base‘𝐺) |
38 | 1, 37 | eqtr4i 2647 |
. . . . . . . . 9
⊢ 𝐵 = (Unit‘𝑅) |
39 | 24, 38 | syl6eleq 2711 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (Unit‘𝑅)) |
40 | | eqid 2622 |
. . . . . . . . 9
⊢
(.g‘(mulGrp‘𝑅)) =
(.g‘(mulGrp‘𝑅)) |
41 | 40, 21, 28 | submmulg 17586 |
. . . . . . . 8
⊢
(((Unit‘𝑅)
∈ (SubMnd‘(mulGrp‘𝑅)) ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ (Unit‘𝑅)) → (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (𝑁(.g‘𝐺)𝑥)) |
42 | 34, 36, 39, 41 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (𝑁(.g‘𝐺)𝑥)) |
43 | | eqid 2622 |
. . . . . . . . 9
⊢
(1r‘𝑅) = (1r‘𝑅) |
44 | 20, 21, 43 | unitgrpid 18669 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(1r‘𝑅) =
(0g‘𝐺)) |
45 | 19, 44 | syl 17 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → (1r‘𝑅) = (0g‘𝐺)) |
46 | 42, 45 | eqeq12d 2637 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → ((𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅) ↔ (𝑁(.g‘𝐺)𝑥) = (0g‘𝐺))) |
47 | 31, 46 | bitr4d 271 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅))) |
48 | 47 | rabbidva 3188 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} = {𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) |
49 | 48 | fveq2d 6195 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(#‘{𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) = (#‘{𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)})) |
50 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
51 | 50, 38 | unitss 18660 |
. . . . . 6
⊢ 𝐵 ⊆ (Base‘𝑅) |
52 | | rabss2 3685 |
. . . . . 6
⊢ (𝐵 ⊆ (Base‘𝑅) → {𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ⊆ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) |
53 | 51, 52 | mp1i 13 |
. . . . 5
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → {𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ⊆ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) |
54 | | ssdomg 8001 |
. . . . 5
⊢ ({𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ∈ V → ({𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ⊆ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} → {𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ≼ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)})) |
55 | 8, 53, 54 | mpsyl 68 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → {𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ≼ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) |
56 | | hashdomi 13169 |
. . . 4
⊢ ({𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} ≼ {𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)} → (#‘{𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ≤ (#‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)})) |
57 | 55, 56 | syl 17 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(#‘{𝑥 ∈ 𝐵 ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ≤ (#‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)})) |
58 | 49, 57 | eqbrtrd 4675 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(#‘{𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ≤ (#‘{𝑥 ∈ (Base‘𝑅) ∣ (𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)})) |
59 | | simpl 473 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑅 ∈ IDomn) |
60 | 50, 43 | ringidcl 18568 |
. . . 4
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
61 | 18, 60 | syl 17 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(1r‘𝑅)
∈ (Base‘𝑅)) |
62 | | simpr 477 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ) |
63 | 50, 40 | idomrootle 37773 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧
(1r‘𝑅)
∈ (Base‘𝑅) ∧
𝑁 ∈ ℕ) →
(#‘{𝑥 ∈
(Base‘𝑅) ∣
(𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ≤ 𝑁) |
64 | 59, 61, 62, 63 | syl3anc 1326 |
. 2
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(#‘{𝑥 ∈
(Base‘𝑅) ∣
(𝑁(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅)}) ≤ 𝑁) |
65 | 6, 10, 13, 58, 64 | xrletrd 11993 |
1
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
(#‘{𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ≤ 𝑁) |