Step | Hyp | Ref
| Expression |
1 | | dvdsq1p.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | dvdsq1p.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑃) |
3 | | dvdsq1p.c |
. . . . . 6
⊢ 𝐶 =
(Unic1p‘𝑅) |
4 | 1, 2, 3 | uc1pcl 23707 |
. . . . 5
⊢ (𝐺 ∈ 𝐶 → 𝐺 ∈ 𝐵) |
5 | 4 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → 𝐺 ∈ 𝐵) |
6 | | dvdsq1p.d |
. . . . 5
⊢ ∥ =
(∥r‘𝑃) |
7 | | dvdsq1p.t |
. . . . 5
⊢ · =
(.r‘𝑃) |
8 | 2, 6, 7 | dvdsr2 18470 |
. . . 4
⊢ (𝐺 ∈ 𝐵 → (𝐺 ∥ 𝐹 ↔ ∃𝑞 ∈ 𝐵 (𝑞 · 𝐺) = 𝐹)) |
9 | 5, 8 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ ∃𝑞 ∈ 𝐵 (𝑞 · 𝐺) = 𝐹)) |
10 | | eqcom 2617 |
. . . . 5
⊢ ((𝑞 · 𝐺) = 𝐹 ↔ 𝐹 = (𝑞 · 𝐺)) |
11 | | simprr 792 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝐹 = (𝑞 · 𝐺)) |
12 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝑞 ∈ 𝐵) |
13 | | simpl1 1057 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑅 ∈ Ring) |
14 | 1 | ply1ring 19439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑃 ∈ Ring) |
16 | | ringgrp 18375 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑃 ∈ Grp) |
18 | | simpl2 1058 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝐹 ∈ 𝐵) |
19 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑞 ∈ 𝐵) |
20 | 5 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
21 | 2, 7 | ringcl 18384 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Ring ∧ 𝑞 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑞 · 𝐺) ∈ 𝐵) |
22 | 15, 19, 20, 21 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → (𝑞 · 𝐺) ∈ 𝐵) |
23 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑃) = (0g‘𝑃) |
24 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(-g‘𝑃) = (-g‘𝑃) |
25 | 2, 23, 24 | grpsubeq0 17324 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ (𝑞 · 𝐺) ∈ 𝐵) → ((𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃) ↔ 𝐹 = (𝑞 · 𝐺))) |
26 | 17, 18, 22, 25 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → ((𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃) ↔ 𝐹 = (𝑞 · 𝐺))) |
27 | 26 | biimprd 237 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → (𝐹 = (𝑞 · 𝐺) → (𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃))) |
28 | 27 | impr 647 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃)) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (( deg1 ‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) = (( deg1 ‘𝑅)‘(0g‘𝑃))) |
30 | | simpl1 1057 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝑅 ∈ Ring) |
31 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (
deg1 ‘𝑅) =
( deg1 ‘𝑅) |
32 | 31, 1, 23 | deg1z 23651 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → ((
deg1 ‘𝑅)‘(0g‘𝑃)) = -∞) |
33 | 30, 32 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (( deg1 ‘𝑅)‘(0g‘𝑃)) = -∞) |
34 | 29, 33 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (( deg1 ‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) = -∞) |
35 | 31, 3 | uc1pdeg 23711 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐶) → (( deg1 ‘𝑅)‘𝐺) ∈
ℕ0) |
36 | 35 | 3adant2 1073 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (( deg1 ‘𝑅)‘𝐺) ∈
ℕ0) |
37 | 36 | nn0red 11229 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (( deg1 ‘𝑅)‘𝐺) ∈ ℝ) |
38 | 37 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (( deg1 ‘𝑅)‘𝐺) ∈ ℝ) |
39 | | mnflt 11833 |
. . . . . . . . . . 11
⊢ (((
deg1 ‘𝑅)‘𝐺) ∈ ℝ → -∞ < ((
deg1 ‘𝑅)‘𝐺)) |
40 | 38, 39 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → -∞ < (( deg1
‘𝑅)‘𝐺)) |
41 | 34, 40 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (( deg1 ‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) < (( deg1 ‘𝑅)‘𝐺)) |
42 | | dvdsq1p.q |
. . . . . . . . . . 11
⊢ 𝑄 =
(quot1p‘𝑅) |
43 | 42, 1, 2, 31, 24, 7, 3 | q1peqb 23718 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((𝑞 ∈ 𝐵 ∧ (( deg1 ‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) < (( deg1 ‘𝑅)‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑞)) |
44 | 43 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((𝑞 ∈ 𝐵 ∧ (( deg1 ‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) < (( deg1 ‘𝑅)‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑞)) |
45 | 12, 41, 44 | mpbi2and 958 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (𝐹𝑄𝐺) = 𝑞) |
46 | 45 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((𝐹𝑄𝐺) · 𝐺) = (𝑞 · 𝐺)) |
47 | 11, 46 | eqtr4d 2647 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝐹 = ((𝐹𝑄𝐺) · 𝐺)) |
48 | 47 | expr 641 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → (𝐹 = (𝑞 · 𝐺) → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |
49 | 10, 48 | syl5bi 231 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → ((𝑞 · 𝐺) = 𝐹 → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |
50 | 49 | rexlimdva 3013 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (∃𝑞 ∈ 𝐵 (𝑞 · 𝐺) = 𝐹 → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |
51 | 9, 50 | sylbid 229 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |
52 | 42, 1, 2, 3 | q1pcl 23719 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝑄𝐺) ∈ 𝐵) |
53 | 2, 6, 7 | dvdsrmul 18471 |
. . . 4
⊢ ((𝐺 ∈ 𝐵 ∧ (𝐹𝑄𝐺) ∈ 𝐵) → 𝐺 ∥ ((𝐹𝑄𝐺) · 𝐺)) |
54 | 5, 52, 53 | syl2anc 691 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → 𝐺 ∥ ((𝐹𝑄𝐺) · 𝐺)) |
55 | | breq2 4587 |
. . 3
⊢ (𝐹 = ((𝐹𝑄𝐺) · 𝐺) → (𝐺 ∥ 𝐹 ↔ 𝐺 ∥ ((𝐹𝑄𝐺) · 𝐺))) |
56 | 54, 55 | syl5ibrcom 236 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹 = ((𝐹𝑄𝐺) · 𝐺) → 𝐺 ∥ 𝐹)) |
57 | 51, 56 | impbid 201 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |