Step | Hyp | Ref
| Expression |
1 | | dvdsq1p.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | dvdsq1p.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑃) |
3 | | dvdsq1p.c |
. . . . . 6
⊢ 𝐶 =
(Unic1p‘𝑅) |
4 | 1, 2, 3 | uc1pcl 23903 |
. . . . 5
⊢ (𝐺 ∈ 𝐶 → 𝐺 ∈ 𝐵) |
5 | 4 | 3ad2ant3 1084 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → 𝐺 ∈ 𝐵) |
6 | | dvdsq1p.d |
. . . . 5
⊢ ∥ =
(∥r‘𝑃) |
7 | | dvdsq1p.t |
. . . . 5
⊢ · =
(.r‘𝑃) |
8 | 2, 6, 7 | dvdsr2 18647 |
. . . 4
⊢ (𝐺 ∈ 𝐵 → (𝐺 ∥ 𝐹 ↔ ∃𝑞 ∈ 𝐵 (𝑞 · 𝐺) = 𝐹)) |
9 | 5, 8 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ ∃𝑞 ∈ 𝐵 (𝑞 · 𝐺) = 𝐹)) |
10 | | eqcom 2629 |
. . . . 5
⊢ ((𝑞 · 𝐺) = 𝐹 ↔ 𝐹 = (𝑞 · 𝐺)) |
11 | | simprr 796 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝐹 = (𝑞 · 𝐺)) |
12 | | simprl 794 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝑞 ∈ 𝐵) |
13 | | simpl1 1064 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑅 ∈ Ring) |
14 | 1 | ply1ring 19618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑃 ∈ Ring) |
16 | | ringgrp 18552 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑃 ∈ Grp) |
18 | | simpl2 1065 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
19 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑞 ∈ 𝐵) |
20 | 5 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
21 | 2, 7 | ringcl 18561 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Ring ∧ 𝑞 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑞 · 𝐺) ∈ 𝐵) |
22 | 15, 19, 20, 21 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → (𝑞 · 𝐺) ∈ 𝐵) |
23 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑃) = (0g‘𝑃) |
24 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(-g‘𝑃) = (-g‘𝑃) |
25 | 2, 23, 24 | grpsubeq0 17501 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ (𝑞 · 𝐺) ∈ 𝐵) → ((𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃) ↔ 𝐹 = (𝑞 · 𝐺))) |
26 | 17, 18, 22, 25 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → ((𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃) ↔ 𝐹 = (𝑞 · 𝐺))) |
27 | 26 | biimprd 238 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → (𝐹 = (𝑞 · 𝐺) → (𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃))) |
28 | 27 | impr 649 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃)) |
29 | 28 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (( deg1 ‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) = (( deg1 ‘𝑅)‘(0g‘𝑃))) |
30 | | simpl1 1064 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝑅 ∈ Ring) |
31 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (
deg1 ‘𝑅) =
( deg1 ‘𝑅) |
32 | 31, 1, 23 | deg1z 23847 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → ((
deg1 ‘𝑅)‘(0g‘𝑃)) = -∞) |
33 | 30, 32 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (( deg1 ‘𝑅)‘(0g‘𝑃)) = -∞) |
34 | 29, 33 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (( deg1 ‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) = -∞) |
35 | 31, 3 | uc1pdeg 23907 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐶) → (( deg1 ‘𝑅)‘𝐺) ∈
ℕ0) |
36 | 35 | 3adant2 1080 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (( deg1 ‘𝑅)‘𝐺) ∈
ℕ0) |
37 | 36 | nn0red 11352 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (( deg1 ‘𝑅)‘𝐺) ∈ ℝ) |
38 | 37 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (( deg1 ‘𝑅)‘𝐺) ∈ ℝ) |
39 | | mnflt 11957 |
. . . . . . . . . . 11
⊢ (((
deg1 ‘𝑅)‘𝐺) ∈ ℝ → -∞ < ((
deg1 ‘𝑅)‘𝐺)) |
40 | 38, 39 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → -∞ < (( deg1
‘𝑅)‘𝐺)) |
41 | 34, 40 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (( deg1 ‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) < (( deg1 ‘𝑅)‘𝐺)) |
42 | | dvdsq1p.q |
. . . . . . . . . . 11
⊢ 𝑄 =
(quot1p‘𝑅) |
43 | 42, 1, 2, 31, 24, 7, 3 | q1peqb 23914 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((𝑞 ∈ 𝐵 ∧ (( deg1 ‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) < (( deg1 ‘𝑅)‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑞)) |
44 | 43 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((𝑞 ∈ 𝐵 ∧ (( deg1 ‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) < (( deg1 ‘𝑅)‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑞)) |
45 | 12, 41, 44 | mpbi2and 956 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (𝐹𝑄𝐺) = 𝑞) |
46 | 45 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((𝐹𝑄𝐺) · 𝐺) = (𝑞 · 𝐺)) |
47 | 11, 46 | eqtr4d 2659 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝐹 = ((𝐹𝑄𝐺) · 𝐺)) |
48 | 47 | expr 643 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → (𝐹 = (𝑞 · 𝐺) → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |
49 | 10, 48 | syl5bi 232 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → ((𝑞 · 𝐺) = 𝐹 → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |
50 | 49 | rexlimdva 3031 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (∃𝑞 ∈ 𝐵 (𝑞 · 𝐺) = 𝐹 → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |
51 | 9, 50 | sylbid 230 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |
52 | 42, 1, 2, 3 | q1pcl 23915 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝑄𝐺) ∈ 𝐵) |
53 | 2, 6, 7 | dvdsrmul 18648 |
. . . 4
⊢ ((𝐺 ∈ 𝐵 ∧ (𝐹𝑄𝐺) ∈ 𝐵) → 𝐺 ∥ ((𝐹𝑄𝐺) · 𝐺)) |
54 | 5, 52, 53 | syl2anc 693 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → 𝐺 ∥ ((𝐹𝑄𝐺) · 𝐺)) |
55 | | breq2 4657 |
. . 3
⊢ (𝐹 = ((𝐹𝑄𝐺) · 𝐺) → (𝐺 ∥ 𝐹 ↔ 𝐺 ∥ ((𝐹𝑄𝐺) · 𝐺))) |
56 | 54, 55 | syl5ibrcom 237 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹 = ((𝐹𝑄𝐺) · 𝐺) → 𝐺 ∥ 𝐹)) |
57 | 51, 56 | impbid 202 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |