Step | Hyp | Ref
| Expression |
1 | | fidomndrng.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 })) |
2 | 1 | eldifad 3904 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
3 | | eldifsni 4729 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝐵 ∖ { 0 }) → 𝐴 ≠ 0 ) |
4 | 1, 3 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≠ 0 ) |
5 | 4 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑦) = 0 ) → 𝐴 ≠ 0 ) |
6 | | oveq1 7278 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝑥 · 𝐴) = (𝑦 · 𝐴)) |
7 | | fidomndrng.f |
. . . . . . . . . . . . . . . . 17
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴)) |
8 | | ovex 7304 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 · 𝐴) ∈ V |
9 | 6, 7, 8 | fvmpt 6872 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝐵 → (𝐹‘𝑦) = (𝑦 · 𝐴)) |
10 | 9 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝐹‘𝑦) = (𝑦 · 𝐴)) |
11 | 10 | eqeq1d 2742 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝐹‘𝑦) = 0 ↔ (𝑦 · 𝐴) = 0 )) |
12 | | fidomndrng.r |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 ∈ Domn) |
13 | 12 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑅 ∈ Domn) |
14 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
15 | 2 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐴 ∈ 𝐵) |
16 | | fidomndrng.b |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = (Base‘𝑅) |
17 | | fidomndrng.t |
. . . . . . . . . . . . . . . 16
⊢ · =
(.r‘𝑅) |
18 | | fidomndrng.z |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝑅) |
19 | 16, 17, 18 | domneq0 20566 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Domn ∧ 𝑦 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵) → ((𝑦 · 𝐴) = 0 ↔ (𝑦 = 0 ∨ 𝐴 = 0 ))) |
20 | 13, 14, 15, 19 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦 · 𝐴) = 0 ↔ (𝑦 = 0 ∨ 𝐴 = 0 ))) |
21 | 11, 20 | bitrd 278 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝐹‘𝑦) = 0 ↔ (𝑦 = 0 ∨ 𝐴 = 0 ))) |
22 | 21 | biimpa 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑦) = 0 ) → (𝑦 = 0 ∨ 𝐴 = 0 )) |
23 | 22 | ord 861 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑦) = 0 ) → (¬ 𝑦 = 0 → 𝐴 = 0 )) |
24 | 23 | necon1ad 2962 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑦) = 0 ) → (𝐴 ≠ 0 → 𝑦 = 0 )) |
25 | 5, 24 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑦) = 0 ) → 𝑦 = 0 ) |
26 | 25 | ex 413 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝐹‘𝑦) = 0 → 𝑦 = 0 )) |
27 | 26 | ralrimiva 3110 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ((𝐹‘𝑦) = 0 → 𝑦 = 0 )) |
28 | | domnring 20565 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) |
29 | 12, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
30 | 16, 17 | ringrghm 19842 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴)) ∈ (𝑅 GrpHom 𝑅)) |
31 | 29, 2, 30 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴)) ∈ (𝑅 GrpHom 𝑅)) |
32 | 7, 31 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑅)) |
33 | 16, 16, 18, 18 | ghmf1 18861 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑅 GrpHom 𝑅) → (𝐹:𝐵–1-1→𝐵 ↔ ∀𝑦 ∈ 𝐵 ((𝐹‘𝑦) = 0 → 𝑦 = 0 ))) |
34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹:𝐵–1-1→𝐵 ↔ ∀𝑦 ∈ 𝐵 ((𝐹‘𝑦) = 0 → 𝑦 = 0 ))) |
35 | 27, 34 | mpbird 256 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐵–1-1→𝐵) |
36 | | fidomndrng.x |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ Fin) |
37 | | enrefg 8755 |
. . . . . . . 8
⊢ (𝐵 ∈ Fin → 𝐵 ≈ 𝐵) |
38 | 36, 37 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ≈ 𝐵) |
39 | | f1finf1o 9024 |
. . . . . . 7
⊢ ((𝐵 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐵–1-1→𝐵 ↔ 𝐹:𝐵–1-1-onto→𝐵)) |
40 | 38, 36, 39 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐹:𝐵–1-1→𝐵 ↔ 𝐹:𝐵–1-1-onto→𝐵)) |
41 | 35, 40 | mpbid 231 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐵) |
42 | | f1ocnv 6726 |
. . . . 5
⊢ (𝐹:𝐵–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐵) |
43 | | f1of 6714 |
. . . . 5
⊢ (◡𝐹:𝐵–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐵) |
44 | 41, 42, 43 | 3syl 18 |
. . . 4
⊢ (𝜑 → ◡𝐹:𝐵⟶𝐵) |
45 | | fidomndrng.o |
. . . . . 6
⊢ 1 =
(1r‘𝑅) |
46 | 16, 45 | ringidcl 19805 |
. . . . 5
⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵) |
47 | 29, 46 | syl 17 |
. . . 4
⊢ (𝜑 → 1 ∈ 𝐵) |
48 | 44, 47 | ffvelrnd 6959 |
. . 3
⊢ (𝜑 → (◡𝐹‘ 1 ) ∈ 𝐵) |
49 | | fidomndrng.d |
. . . 4
⊢ ∥ =
(∥r‘𝑅) |
50 | 16, 49, 17 | dvdsrmul 19888 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ (◡𝐹‘ 1 ) ∈ 𝐵) → 𝐴 ∥ ((◡𝐹‘ 1 ) · 𝐴)) |
51 | 2, 48, 50 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝐴 ∥ ((◡𝐹‘ 1 ) · 𝐴)) |
52 | | oveq1 7278 |
. . . . 5
⊢ (𝑦 = (◡𝐹‘ 1 ) → (𝑦 · 𝐴) = ((◡𝐹‘ 1 ) · 𝐴)) |
53 | 6 | cbvmptv 5192 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝐴)) = (𝑦 ∈ 𝐵 ↦ (𝑦 · 𝐴)) |
54 | 7, 53 | eqtri 2768 |
. . . . 5
⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑦 · 𝐴)) |
55 | | ovex 7304 |
. . . . 5
⊢ ((◡𝐹‘ 1 ) · 𝐴) ∈ V |
56 | 52, 54, 55 | fvmpt 6872 |
. . . 4
⊢ ((◡𝐹‘ 1 ) ∈ 𝐵 → (𝐹‘(◡𝐹‘ 1 )) = ((◡𝐹‘ 1 ) · 𝐴)) |
57 | 48, 56 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹‘(◡𝐹‘ 1 )) = ((◡𝐹‘ 1 ) · 𝐴)) |
58 | | f1ocnvfv2 7146 |
. . . 4
⊢ ((𝐹:𝐵–1-1-onto→𝐵 ∧ 1 ∈ 𝐵) → (𝐹‘(◡𝐹‘ 1 )) = 1 ) |
59 | 41, 47, 58 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐹‘(◡𝐹‘ 1 )) = 1 ) |
60 | 57, 59 | eqtr3d 2782 |
. 2
⊢ (𝜑 → ((◡𝐹‘ 1 ) · 𝐴) = 1 ) |
61 | 51, 60 | breqtrd 5105 |
1
⊢ (𝜑 → 𝐴 ∥ 1 ) |