Step | Hyp | Ref
| Expression |
1 | | simpll 767 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑅 ∈ IDomn) |
2 | | isidom 20367 |
. . . . . . 7
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
3 | 2 | simprbi 500 |
. . . . . 6
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Domn) |
4 | | domnring 20359 |
. . . . . 6
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) |
5 | | eqid 2738 |
. . . . . . 7
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
6 | | idomsubgmo.g |
. . . . . . 7
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s
(Unit‘𝑅)) |
7 | 5, 6 | unitgrp 19710 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp) |
8 | 1, 3, 4, 7 | 4syl 19 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝐺 ∈ Grp) |
9 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
10 | 9 | subgacs 18602 |
. . . . 5
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
11 | | acsmre 17180 |
. . . . 5
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
12 | 8, 10, 11 | 3syl 18 |
. . . 4
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
13 | | proot1mul.k |
. . . 4
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) |
14 | | simprl 771 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑋 ∈ (◡𝑂 “ {𝑁})) |
15 | | proot1mul.o |
. . . . . . . . 9
⊢ 𝑂 = (od‘𝐺) |
16 | 9, 15 | odf 18954 |
. . . . . . . 8
⊢ 𝑂:(Base‘𝐺)⟶ℕ0 |
17 | | ffn 6564 |
. . . . . . . 8
⊢ (𝑂:(Base‘𝐺)⟶ℕ0 → 𝑂 Fn (Base‘𝐺)) |
18 | | fniniseg 6899 |
. . . . . . . 8
⊢ (𝑂 Fn (Base‘𝐺) → (𝑋 ∈ (◡𝑂 “ {𝑁}) ↔ (𝑋 ∈ (Base‘𝐺) ∧ (𝑂‘𝑋) = 𝑁))) |
19 | 16, 17, 18 | mp2b 10 |
. . . . . . 7
⊢ (𝑋 ∈ (◡𝑂 “ {𝑁}) ↔ (𝑋 ∈ (Base‘𝐺) ∧ (𝑂‘𝑋) = 𝑁)) |
20 | 14, 19 | sylib 221 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (𝑋 ∈ (Base‘𝐺) ∧ (𝑂‘𝑋) = 𝑁)) |
21 | 20 | simpld 498 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑋 ∈ (Base‘𝐺)) |
22 | 21 | snssd 4737 |
. . . 4
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → {𝑋} ⊆ (Base‘𝐺)) |
23 | 12, 13, 22 | mrcssidd 17153 |
. . 3
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → {𝑋} ⊆ (𝐾‘{𝑋})) |
24 | | snssg 4713 |
. . . 4
⊢ (𝑋 ∈ (◡𝑂 “ {𝑁}) → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋}))) |
25 | 14, 24 | syl 17 |
. . 3
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋}))) |
26 | 23, 25 | mpbird 260 |
. 2
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑋 ∈ (𝐾‘{𝑋})) |
27 | 6 | idomsubgmo 40755 |
. . . 4
⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) →
∃*𝑥 ∈
(SubGrp‘𝐺)(♯‘𝑥) = 𝑁) |
28 | 27 | adantr 484 |
. . 3
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → ∃*𝑥 ∈ (SubGrp‘𝐺)(♯‘𝑥) = 𝑁) |
29 | 13 | mrccl 17139 |
. . . 4
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ {𝑋} ⊆ (Base‘𝐺)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) |
30 | 12, 22, 29 | syl2anc 587 |
. . 3
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) |
31 | 20 | simprd 499 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (𝑂‘𝑋) = 𝑁) |
32 | | simplr 769 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑁 ∈ ℕ) |
33 | 31, 32 | eqeltrd 2839 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (𝑂‘𝑋) ∈ ℕ) |
34 | 9, 15, 13 | odhash2 18989 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐺) ∧ (𝑂‘𝑋) ∈ ℕ) →
(♯‘(𝐾‘{𝑋})) = (𝑂‘𝑋)) |
35 | 8, 21, 33, 34 | syl3anc 1373 |
. . . 4
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (♯‘(𝐾‘{𝑋})) = (𝑂‘𝑋)) |
36 | 35, 31 | eqtrd 2778 |
. . 3
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (♯‘(𝐾‘{𝑋})) = 𝑁) |
37 | | simprr 773 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑌 ∈ (◡𝑂 “ {𝑁})) |
38 | | fniniseg 6899 |
. . . . . . . 8
⊢ (𝑂 Fn (Base‘𝐺) → (𝑌 ∈ (◡𝑂 “ {𝑁}) ↔ (𝑌 ∈ (Base‘𝐺) ∧ (𝑂‘𝑌) = 𝑁))) |
39 | 16, 17, 38 | mp2b 10 |
. . . . . . 7
⊢ (𝑌 ∈ (◡𝑂 “ {𝑁}) ↔ (𝑌 ∈ (Base‘𝐺) ∧ (𝑂‘𝑌) = 𝑁)) |
40 | 37, 39 | sylib 221 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (𝑌 ∈ (Base‘𝐺) ∧ (𝑂‘𝑌) = 𝑁)) |
41 | 40 | simpld 498 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑌 ∈ (Base‘𝐺)) |
42 | 41 | snssd 4737 |
. . . 4
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → {𝑌} ⊆ (Base‘𝐺)) |
43 | 13 | mrccl 17139 |
. . . 4
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ {𝑌} ⊆ (Base‘𝐺)) → (𝐾‘{𝑌}) ∈ (SubGrp‘𝐺)) |
44 | 12, 42, 43 | syl2anc 587 |
. . 3
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (𝐾‘{𝑌}) ∈ (SubGrp‘𝐺)) |
45 | 40 | simprd 499 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (𝑂‘𝑌) = 𝑁) |
46 | 45, 32 | eqeltrd 2839 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (𝑂‘𝑌) ∈ ℕ) |
47 | 9, 15, 13 | odhash2 18989 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ (Base‘𝐺) ∧ (𝑂‘𝑌) ∈ ℕ) →
(♯‘(𝐾‘{𝑌})) = (𝑂‘𝑌)) |
48 | 8, 41, 46, 47 | syl3anc 1373 |
. . . 4
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (♯‘(𝐾‘{𝑌})) = (𝑂‘𝑌)) |
49 | 48, 45 | eqtrd 2778 |
. . 3
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (♯‘(𝐾‘{𝑌})) = 𝑁) |
50 | | fveqeq2 6745 |
. . . 4
⊢ (𝑥 = (𝐾‘{𝑋}) → ((♯‘𝑥) = 𝑁 ↔ (♯‘(𝐾‘{𝑋})) = 𝑁)) |
51 | | fveqeq2 6745 |
. . . 4
⊢ (𝑥 = (𝐾‘{𝑌}) → ((♯‘𝑥) = 𝑁 ↔ (♯‘(𝐾‘{𝑌})) = 𝑁)) |
52 | 50, 51 | rmoi 3818 |
. . 3
⊢
((∃*𝑥 ∈
(SubGrp‘𝐺)(♯‘𝑥) = 𝑁 ∧ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (♯‘(𝐾‘{𝑋})) = 𝑁) ∧ ((𝐾‘{𝑌}) ∈ (SubGrp‘𝐺) ∧ (♯‘(𝐾‘{𝑌})) = 𝑁)) → (𝐾‘{𝑋}) = (𝐾‘{𝑌})) |
53 | 28, 30, 36, 44, 49, 52 | syl122anc 1381 |
. 2
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → (𝐾‘{𝑋}) = (𝐾‘{𝑌})) |
54 | 26, 53 | eleqtrd 2841 |
1
⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑋 ∈ (𝐾‘{𝑌})) |