Metamath Proof Explorer

Theorem dvdsq1p

Description: Divisibility in a polynomial ring is witnessed by the quotient. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses dvdsq1p.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
dvdsq1p.d ⊢ ∥ = ( ∥r ‘ 𝑃 )
dvdsq1p.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
dvdsq1p.c ⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
dvdsq1p.t ⊢ · = ( .r ‘ 𝑃 )
dvdsq1p.q ⊢ 𝑄 = ( quot1p ‘ 𝑅 )
Assertion dvdsq1p ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐺 ∥ 𝐹 ↔ 𝐹 = ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 dvdsq1p.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 dvdsq1p.d ⊢ ∥ = ( ∥r ‘ 𝑃 )
3 dvdsq1p.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 dvdsq1p.c ⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
5 dvdsq1p.t ⊢ · = ( .r ‘ 𝑃 )
6 dvdsq1p.q ⊢ 𝑄 = ( quot1p ‘ 𝑅 )
7 1 3 4 uc1pcl ⊢ ( 𝐺 ∈ 𝐶 → 𝐺 ∈ 𝐵 )
8 7 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝐺 ∈ 𝐵 )
9 3 2 5 dvdsr2 ⊢ ( 𝐺 ∈ 𝐵 → ( 𝐺 ∥ 𝐹 ↔ ∃ 𝑞 ∈ 𝐵 ( 𝑞 · 𝐺 ) = 𝐹 ) )
10 8 9 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐺 ∥ 𝐹 ↔ ∃ 𝑞 ∈ 𝐵 ( 𝑞 · 𝐺 ) = 𝐹 ) )
11 eqcom ⊢ ( ( 𝑞 · 𝐺 ) = 𝐹 ↔ 𝐹 = ( 𝑞 · 𝐺 ) )
12 simprr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → 𝐹 = ( 𝑞 · 𝐺 ) )
13 simprl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → 𝑞 ∈ 𝐵 )
14 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → 𝑅 ∈ Ring )
15 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
16 14 15 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → 𝑃 ∈ Ring )
17 ringgrp ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
18 16 17 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → 𝑃 ∈ Grp )
19 simpl2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
20 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → 𝑞 ∈ 𝐵 )
21 8 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
22 3 5 ringcl ⊢ ( ( 𝑃 ∈ Ring ∧ 𝑞 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑞 · 𝐺 ) ∈ 𝐵 )
23 16 20 21 22 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → ( 𝑞 · 𝐺 ) ∈ 𝐵 )
24 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
25 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
26 3 24 25 grpsubeq0 ⊢ ( ( 𝑃 ∈ Grp ∧ 𝐹 ∈ 𝐵 ∧ ( 𝑞 · 𝐺 ) ∈ 𝐵 ) → ( ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑞 · 𝐺 ) ) = ( 0g ‘ 𝑃 ) ↔ 𝐹 = ( 𝑞 · 𝐺 ) ) )
27 18 19 23 26 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑞 · 𝐺 ) ) = ( 0g ‘ 𝑃 ) ↔ 𝐹 = ( 𝑞 · 𝐺 ) ) )
28 27 biimprd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → ( 𝐹 = ( 𝑞 · 𝐺 ) → ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑞 · 𝐺 ) ) = ( 0g ‘ 𝑃 ) ) )
29 28 impr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑞 · 𝐺 ) ) = ( 0g ‘ 𝑃 ) )
30 29 fveq2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑞 · 𝐺 ) ) ) = ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) )
31 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → 𝑅 ∈ Ring )
32 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
33 32 1 24 deg1z ⊢ ( 𝑅 ∈ Ring → ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
34 31 33 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
35 30 34 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑞 · 𝐺 ) ) ) = -∞ )
36 32 4 uc1pdeg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐶 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) ∈ ℕ0 )
37 36 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) ∈ ℕ0 )
38 37 nn0red ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) ∈ ℝ )
39 38 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) ∈ ℝ )
40 39 mnfltd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → -∞ < ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) )
41 35 40 eqbrtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑞 · 𝐺 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) )
42 6 1 3 32 25 5 4 q1peqb ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝑞 ∈ 𝐵 ∧ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑞 · 𝐺 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) ) ↔ ( 𝐹 𝑄 𝐺 ) = 𝑞 ) )
43 42 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → ( ( 𝑞 ∈ 𝐵 ∧ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝐹 ( -g ‘ 𝑃 ) ( 𝑞 · 𝐺 ) ) ) < ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) ) ↔ ( 𝐹 𝑄 𝐺 ) = 𝑞 ) )
44 13 41 43 mpbi2and ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → ( 𝐹 𝑄 𝐺 ) = 𝑞 )
45 44 oveq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) = ( 𝑞 · 𝐺 ) )
46 12 45 eqtr4d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝐹 = ( 𝑞 · 𝐺 ) ) ) → 𝐹 = ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) )
47 46 expr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → ( 𝐹 = ( 𝑞 · 𝐺 ) → 𝐹 = ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
48 11 47 biimtrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝑞 · 𝐺 ) = 𝐹 → 𝐹 = ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
49 48 rexlimdva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ∃ 𝑞 ∈ 𝐵 ( 𝑞 · 𝐺 ) = 𝐹 → 𝐹 = ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
50 10 49 sylbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐺 ∥ 𝐹 → 𝐹 = ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
51 6 1 3 4 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐹 𝑄 𝐺 ) ∈ 𝐵 )
52 3 2 5 dvdsrmul ⊢ ( ( 𝐺 ∈ 𝐵 ∧ ( 𝐹 𝑄 𝐺 ) ∈ 𝐵 ) → 𝐺 ∥ ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) )
53 8 51 52 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝐺 ∥ ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) )
54 breq2 ⊢ ( 𝐹 = ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) → ( 𝐺 ∥ 𝐹 ↔ 𝐺 ∥ ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )
55 53 54 syl5ibrcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐹 = ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) → 𝐺 ∥ 𝐹 ) )
56 50 55 impbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐺 ∥ 𝐹 ↔ 𝐹 = ( ( 𝐹 𝑄 𝐺 ) · 𝐺 ) ) )