Metamath Proof Explorer

Theorem quotval

Description: Value of the quotient function. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Hypothesis quotval.1 ⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
Assertion quotval ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 quotval.1 ⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
2 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
3 2 sseli ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
4 2 sseli ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
5 eldifsn ⊢ ( 𝐺 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↔ ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) )
6 oveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∘f · 𝑞 ) = ( 𝐺 ∘f · 𝑞 ) )
7 oveq12 ⊢ ( ( 𝑓 = 𝐹 ∧ ( 𝑔 ∘f · 𝑞 ) = ( 𝐺 ∘f · 𝑞 ) ) → ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) ) )
8 6 7 sylan2 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) ) )
9 8 1 eqtr4di ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) = 𝑅 )
10 9 sbceq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ↔ [ 𝑅 / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ) )
11 1 ovexi ⊢ 𝑅 ∈ V
12 eqeq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 = 0𝑝 ↔ 𝑅 = 0𝑝 ) )
13 fveq2 ⊢ ( 𝑟 = 𝑅 → ( deg ‘ 𝑟 ) = ( deg ‘ 𝑅 ) )
14 13 breq1d ⊢ ( 𝑟 = 𝑅 → ( ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ↔ ( deg ‘ 𝑅 ) < ( deg ‘ 𝑔 ) ) )
15 12 14 orbi12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝑔 ) ) ) )
16 11 15 sbcie ⊢ ( [ 𝑅 / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝑔 ) ) )
17 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
18 17 fveq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( deg ‘ 𝑔 ) = ( deg ‘ 𝐺 ) )
19 18 breq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( deg ‘ 𝑅 ) < ( deg ‘ 𝑔 ) ↔ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )
20 19 orbi2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝑔 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
21 16 20 bitrid ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( [ 𝑅 / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
22 10 21 bitrd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ↔ ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
23 22 riotabidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
24 df-quot ⊢ quot = ( 𝑓 ∈ ( Poly ‘ ℂ ) , 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↦ ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) [ ( 𝑓 ∘f − ( 𝑔 ∘f · 𝑞 ) ) / 𝑟 ] ( 𝑟 = 0𝑝 ∨ ( deg ‘ 𝑟 ) < ( deg ‘ 𝑔 ) ) ) )
25 riotaex ⊢ ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) ∈ V
26 23 24 25 ovmpoa ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
27 5 26 sylan2br ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
28 27 3impb ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
29 4 28 syl3an2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )
30 3 29 syl3an1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 quot 𝐺 ) = ( ℩ 𝑞 ∈ ( Poly ‘ ℂ ) ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) ) )