This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem q1peqb

Description: Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses q1pval.q ⊢ 𝑄 = ( quot1p ‘ 𝑅 )
q1pval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
q1pval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
q1pval.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
q1pval.m ⊢ − = ( -g ‘ 𝑃 )
q1pval.t ⊢ · = ( .r ‘ 𝑃 )
q1peqb.c ⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
Assertion q1peqb ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( 𝐹 𝑄 𝐺 ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 q1pval.q ⊢ 𝑄 = ( quot1p ‘ 𝑅 )
2 q1pval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 q1pval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 q1pval.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
5 q1pval.m ⊢ − = ( -g ‘ 𝑃 )
6 q1pval.t ⊢ · = ( .r ‘ 𝑃 )
7 q1peqb.c ⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
8 elex ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ V )
9 8 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → 𝑋 ∈ V )
10 9 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) → 𝑋 ∈ V ) )
11 ovex ⊢ ( 𝐹 𝑄 𝐺 ) ∈ V
12 eleq1 ⊢ ( ( 𝐹 𝑄 𝐺 ) = 𝑋 → ( ( 𝐹 𝑄 𝐺 ) ∈ V ↔ 𝑋 ∈ V ) )
13 11 12 mpbii ⊢ ( ( 𝐹 𝑄 𝐺 ) = 𝑋 → 𝑋 ∈ V )
14 13 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝐹 𝑄 𝐺 ) = 𝑋 → 𝑋 ∈ V ) )
15 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑋 ∈ V ) → 𝑋 ∈ V )
16 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
17 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝑅 ∈ Ring )
18 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝐹 ∈ 𝐵 )
19 2 3 7 uc1pcl ⊢ ( 𝐺 ∈ 𝐶 → 𝐺 ∈ 𝐵 )
20 19 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝐺 ∈ 𝐵 )
21 2 16 7 uc1pn0 ⊢ ( 𝐺 ∈ 𝐶 → 𝐺 ≠ ( 0g ‘ 𝑃 ) )
22 21 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → 𝐺 ≠ ( 0g ‘ 𝑃 ) )
23 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
24 4 23 7 uc1pldg ⊢ ( 𝐺 ∈ 𝐶 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( Unit ‘ 𝑅 ) )
25 24 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ ( Unit ‘ 𝑅 ) )
26 2 4 3 5 16 6 17 18 20 22 25 23 ply1divalg2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
27 df-reu ⊢ ( ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ∃! 𝑞 ( 𝑞 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
28 26 27 sylib ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ∃! 𝑞 ( 𝑞 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
29 28 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑋 ∈ V ) → ∃! 𝑞 ( 𝑞 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
30 eleq1 ⊢ ( 𝑞 = 𝑋 → ( 𝑞 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵 ) )
31 oveq1 ⊢ ( 𝑞 = 𝑋 → ( 𝑞 · 𝐺 ) = ( 𝑋 · 𝐺 ) )
32 31 oveq2d ⊢ ( 𝑞 = 𝑋 → ( 𝐹 − ( 𝑞 · 𝐺 ) ) = ( 𝐹 − ( 𝑋 · 𝐺 ) ) )
33 32 fveq2d ⊢ ( 𝑞 = 𝑋 → ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) = ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) )
34 33 breq1d ⊢ ( 𝑞 = 𝑋 → ( ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
35 30 34 anbi12d ⊢ ( 𝑞 = 𝑋 → ( ( 𝑞 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
36 35 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑋 ∈ V ) ∧ 𝑞 = 𝑋 ) → ( ( 𝑞 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
37 15 29 36 iota2d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑋 ∈ V ) → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( ℩ 𝑞 ( 𝑞 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) = 𝑋 ) )
38 1 2 3 4 5 6 q1pval ⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 𝑄 𝐺 ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
39 18 20 38 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐹 𝑄 𝐺 ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
40 df-riota ⊢ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) = ( ℩ 𝑞 ( 𝑞 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
41 39 40 eqtrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝐹 𝑄 𝐺 ) = ( ℩ 𝑞 ( 𝑞 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
42 41 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑋 ∈ V ) → ( 𝐹 𝑄 𝐺 ) = ( ℩ 𝑞 ( 𝑞 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) )
43 42 eqeq1d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑋 ∈ V ) → ( ( 𝐹 𝑄 𝐺 ) = 𝑋 ↔ ( ℩ 𝑞 ( 𝑞 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ) = 𝑋 ) )
44 37 43 bitr4d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) ∧ 𝑋 ∈ V ) → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( 𝐹 𝑄 𝐺 ) = 𝑋 ) )
45 44 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( 𝑋 ∈ V → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( 𝐹 𝑄 𝐺 ) = 𝑋 ) ) )
46 10 14 45 pm5.21ndd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( 𝐹 𝑄 𝐺 ) = 𝑋 ) )