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 ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐷 ‘ ( 𝐹 − ( 𝑋 · 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) ↔ ( 𝐹 𝑄 𝐺 ) = 𝑋 ) )