Theorem q1pval

Description: Value of the univariate polynomial quotient function. (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 ‘ 𝑃 )
Assertion	q1pval	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 𝑄 𝐺 ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )

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	2 3	elbasfv	⊢ ( 𝐺 ∈ 𝐵 → 𝑅 ∈ V )
8		fveq2	⊢ ( 𝑟 = 𝑅 → ( Poly1 ‘ 𝑟 ) = ( Poly1 ‘ 𝑅 ) )
9	8 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Poly1 ‘ 𝑟 ) = 𝑃 )
10	9	csbeq1d	⊢ ( 𝑟 = 𝑅 → ⦋ ( Poly1 ‘ 𝑟 ) / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ⦋ 𝑃 / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) )
11	2	fvexi	⊢ 𝑃 ∈ V
12	11	a1i	⊢ ( 𝑟 = 𝑅 → 𝑃 ∈ V )
13		fveq2	⊢ ( 𝑝 = 𝑃 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝑃 ) )
14	13	adantl	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → ( Base ‘ 𝑝 ) = ( Base ‘ 𝑃 ) )
15	14 3	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → ( Base ‘ 𝑝 ) = 𝐵 )
16	15	csbeq1d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ⦋ 𝐵 / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) )
17	3	fvexi	⊢ 𝐵 ∈ V
18	17	a1i	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → 𝐵 ∈ V )
19		simpr	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
20		fveq2	⊢ ( 𝑟 = 𝑅 → ( deg1 ‘ 𝑟 ) = ( deg1 ‘ 𝑅 ) )
21	20	ad2antrr	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( deg1 ‘ 𝑟 ) = ( deg1 ‘ 𝑅 ) )
22	21 4	eqtr4di	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( deg1 ‘ 𝑟 ) = 𝐷 )
23		fveq2	⊢ ( 𝑝 = 𝑃 → ( -g ‘ 𝑝 ) = ( -g ‘ 𝑃 ) )
24	23	ad2antlr	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( -g ‘ 𝑝 ) = ( -g ‘ 𝑃 ) )
25	24 5	eqtr4di	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( -g ‘ 𝑝 ) = − )
26		eqidd	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → 𝑓 = 𝑓 )
27		fveq2	⊢ ( 𝑝 = 𝑃 → ( .r ‘ 𝑝 ) = ( .r ‘ 𝑃 ) )
28	27	ad2antlr	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( .r ‘ 𝑝 ) = ( .r ‘ 𝑃 ) )
29	28 6	eqtr4di	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( .r ‘ 𝑝 ) = · )
30	29	oveqd	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) = ( 𝑞 · 𝑔 ) )
31	25 26 30	oveq123d	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) = ( 𝑓 − ( 𝑞 · 𝑔 ) ) )
32	22 31	fveq12d	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) = ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) )
33	22	fveq1d	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) = ( 𝐷 ‘ 𝑔 ) )
34	32 33	breq12d	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ↔ ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) )
35	19 34	riotaeqbidv	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) )
36	19 19 35	mpoeq123dv	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
37	18 36	csbied	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → ⦋ 𝐵 / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
38	16 37	eqtrd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑝 = 𝑃 ) → ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
39	12 38	csbied	⊢ ( 𝑟 = 𝑅 → ⦋ 𝑃 / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
40	10 39	eqtrd	⊢ ( 𝑟 = 𝑅 → ⦋ ( Poly1 ‘ 𝑟 ) / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
41		df-q1p	⊢ quot1p = ( 𝑟 ∈ V ↦ ⦋ ( Poly1 ‘ 𝑟 ) / 𝑝 ⦌ ⦋ ( Base ‘ 𝑝 ) / 𝑏 ⦌ ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( ℩ 𝑞 ∈ 𝑏 ( ( deg1 ‘ 𝑟 ) ‘ ( 𝑓 ( -g ‘ 𝑝 ) ( 𝑞 ( .r ‘ 𝑝 ) 𝑔 ) ) ) < ( ( deg1 ‘ 𝑟 ) ‘ 𝑔 ) ) ) )
42	17 17	mpoex	⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) ∈ V
43	40 41 42	fvmpt	⊢ ( 𝑅 ∈ V → ( quot1p ‘ 𝑅 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
44	1 43	syl5eq	⊢ ( 𝑅 ∈ V → 𝑄 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
45	7 44	syl	⊢ ( 𝐺 ∈ 𝐵 → 𝑄 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
46	45	adantl	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝑄 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) ) )
47		id	⊢ ( 𝑓 = 𝐹 → 𝑓 = 𝐹 )
48		oveq2	⊢ ( 𝑔 = 𝐺 → ( 𝑞 · 𝑔 ) = ( 𝑞 · 𝐺 ) )
49	47 48	oveqan12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 − ( 𝑞 · 𝑔 ) ) = ( 𝐹 − ( 𝑞 · 𝐺 ) ) )
50	49	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) = ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) )
51		fveq2	⊢ ( 𝑔 = 𝐺 → ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ 𝐺 ) )
52	51	adantl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝐷 ‘ 𝑔 ) = ( 𝐷 ‘ 𝐺 ) )
53	50 52	breq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ↔ ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
54	53	riotabidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
55	54	adantl	⊢ ( ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝑓 − ( 𝑞 · 𝑔 ) ) ) < ( 𝐷 ‘ 𝑔 ) ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
56		simpl	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
57		simpr	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
58		riotaex	⊢ ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ∈ V
59	58	a1i	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ∈ V )
60	46 55 56 57 59	ovmpod	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 𝑄 𝐺 ) = ( ℩ 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )