| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dvdsq1p.p | . . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) | 
| 2 |  | dvdsq1p.b | . . . . . 6
⊢ 𝐵 = (Base‘𝑃) | 
| 3 |  | dvdsq1p.c | . . . . . 6
⊢ 𝐶 =
(Unic1p‘𝑅) | 
| 4 | 1, 2, 3 | uc1pcl 26183 | . . . . 5
⊢ (𝐺 ∈ 𝐶 → 𝐺 ∈ 𝐵) | 
| 5 | 4 | 3ad2ant3 1136 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → 𝐺 ∈ 𝐵) | 
| 6 |  | dvdsq1p.d | . . . . 5
⊢  ∥ =
(∥r‘𝑃) | 
| 7 |  | dvdsq1p.t | . . . . 5
⊢  · =
(.r‘𝑃) | 
| 8 | 2, 6, 7 | dvdsr2 20363 | . . . 4
⊢ (𝐺 ∈ 𝐵 → (𝐺 ∥ 𝐹 ↔ ∃𝑞 ∈ 𝐵 (𝑞 · 𝐺) = 𝐹)) | 
| 9 | 5, 8 | syl 17 | . . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ ∃𝑞 ∈ 𝐵 (𝑞 · 𝐺) = 𝐹)) | 
| 10 |  | eqcom 2744 | . . . . 5
⊢ ((𝑞 · 𝐺) = 𝐹 ↔ 𝐹 = (𝑞 · 𝐺)) | 
| 11 |  | simprr 773 | . . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝐹 = (𝑞 · 𝐺)) | 
| 12 |  | simprl 771 | . . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝑞 ∈ 𝐵) | 
| 13 |  | simpl1 1192 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑅 ∈ Ring) | 
| 14 | 1 | ply1ring 22249 | . . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑃 ∈ Ring) | 
| 16 |  | ringgrp 20235 | . . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) | 
| 17 | 15, 16 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑃 ∈ Grp) | 
| 18 |  | simpl2 1193 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝐹 ∈ 𝐵) | 
| 19 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝑞 ∈ 𝐵) | 
| 20 | 5 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → 𝐺 ∈ 𝐵) | 
| 21 | 2, 7 | ringcl 20247 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Ring ∧ 𝑞 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑞 · 𝐺) ∈ 𝐵) | 
| 22 | 15, 19, 20, 21 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → (𝑞 · 𝐺) ∈ 𝐵) | 
| 23 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(0g‘𝑃) = (0g‘𝑃) | 
| 24 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(-g‘𝑃) = (-g‘𝑃) | 
| 25 | 2, 23, 24 | grpsubeq0 19044 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ (𝑞 · 𝐺) ∈ 𝐵) → ((𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃) ↔ 𝐹 = (𝑞 · 𝐺))) | 
| 26 | 17, 18, 22, 25 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → ((𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃) ↔ 𝐹 = (𝑞 · 𝐺))) | 
| 27 | 26 | biimprd 248 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → (𝐹 = (𝑞 · 𝐺) → (𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃))) | 
| 28 | 27 | impr 454 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (𝐹(-g‘𝑃)(𝑞 · 𝐺)) = (0g‘𝑃)) | 
| 29 | 28 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((deg1‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) = ((deg1‘𝑅)‘(0g‘𝑃))) | 
| 30 |  | simpl1 1192 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝑅 ∈ Ring) | 
| 31 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(deg1‘𝑅) = (deg1‘𝑅) | 
| 32 | 31, 1, 23 | deg1z 26126 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
((deg1‘𝑅)‘(0g‘𝑃)) = -∞) | 
| 33 | 30, 32 | syl 17 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((deg1‘𝑅)‘(0g‘𝑃)) = -∞) | 
| 34 | 29, 33 | eqtrd 2777 | . . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((deg1‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) = -∞) | 
| 35 | 31, 3 | uc1pdeg 26187 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐶) → ((deg1‘𝑅)‘𝐺) ∈
ℕ0) | 
| 36 | 35 | 3adant2 1132 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((deg1‘𝑅)‘𝐺) ∈
ℕ0) | 
| 37 | 36 | nn0red 12588 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((deg1‘𝑅)‘𝐺) ∈ ℝ) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((deg1‘𝑅)‘𝐺) ∈ ℝ) | 
| 39 | 38 | mnfltd 13166 | . . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → -∞ <
((deg1‘𝑅)‘𝐺)) | 
| 40 | 34, 39 | eqbrtrd 5165 | . . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((deg1‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) < ((deg1‘𝑅)‘𝐺)) | 
| 41 |  | dvdsq1p.q | . . . . . . . . . . 11
⊢ 𝑄 =
(quot1p‘𝑅) | 
| 42 | 41, 1, 2, 31, 24, 7, 3 | q1peqb 26195 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → ((𝑞 ∈ 𝐵 ∧ ((deg1‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) < ((deg1‘𝑅)‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑞)) | 
| 43 | 42 | adantr 480 | . . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((𝑞 ∈ 𝐵 ∧ ((deg1‘𝑅)‘(𝐹(-g‘𝑃)(𝑞 · 𝐺))) < ((deg1‘𝑅)‘𝐺)) ↔ (𝐹𝑄𝐺) = 𝑞)) | 
| 44 | 12, 40, 43 | mpbi2and 712 | . . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → (𝐹𝑄𝐺) = 𝑞) | 
| 45 | 44 | oveq1d 7446 | . . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → ((𝐹𝑄𝐺) · 𝐺) = (𝑞 · 𝐺)) | 
| 46 | 11, 45 | eqtr4d 2780 | . . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ (𝑞 ∈ 𝐵 ∧ 𝐹 = (𝑞 · 𝐺))) → 𝐹 = ((𝐹𝑄𝐺) · 𝐺)) | 
| 47 | 46 | expr 456 | . . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → (𝐹 = (𝑞 · 𝐺) → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) | 
| 48 | 10, 47 | biimtrid 242 | . . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) ∧ 𝑞 ∈ 𝐵) → ((𝑞 · 𝐺) = 𝐹 → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) | 
| 49 | 48 | rexlimdva 3155 | . . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (∃𝑞 ∈ 𝐵 (𝑞 · 𝐺) = 𝐹 → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) | 
| 50 | 9, 49 | sylbid 240 | . 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 → 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) | 
| 51 | 41, 1, 2, 3 | q1pcl 26196 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹𝑄𝐺) ∈ 𝐵) | 
| 52 | 2, 6, 7 | dvdsrmul 20364 | . . . 4
⊢ ((𝐺 ∈ 𝐵 ∧ (𝐹𝑄𝐺) ∈ 𝐵) → 𝐺 ∥ ((𝐹𝑄𝐺) · 𝐺)) | 
| 53 | 5, 51, 52 | syl2anc 584 | . . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → 𝐺 ∥ ((𝐹𝑄𝐺) · 𝐺)) | 
| 54 |  | breq2 5147 | . . 3
⊢ (𝐹 = ((𝐹𝑄𝐺) · 𝐺) → (𝐺 ∥ 𝐹 ↔ 𝐺 ∥ ((𝐹𝑄𝐺) · 𝐺))) | 
| 55 | 53, 54 | syl5ibrcom 247 | . 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐹 = ((𝐹𝑄𝐺) · 𝐺) → 𝐺 ∥ 𝐹)) | 
| 56 | 50, 55 | impbid 212 | 1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶) → (𝐺 ∥ 𝐹 ↔ 𝐹 = ((𝐹𝑄𝐺) · 𝐺))) |