Metamath Proof Explorer


Theorem q1pcl

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

Ref Expression
Hypotheses q1pcl.q 𝑄 = ( quot1p𝑅 )
q1pcl.p 𝑃 = ( Poly1𝑅 )
q1pcl.b 𝐵 = ( Base ‘ 𝑃 )
q1pcl.c 𝐶 = ( Unic1p𝑅 )
Assertion q1pcl ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐶 ) → ( 𝐹 𝑄 𝐺 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 q1pcl.q 𝑄 = ( quot1p𝑅 )
2 q1pcl.p 𝑃 = ( Poly1𝑅 )
3 q1pcl.b 𝐵 = ( Base ‘ 𝑃 )
4 q1pcl.c 𝐶 = ( Unic1p𝑅 )
5 eqid ( 𝐹 𝑄 𝐺 ) = ( 𝐹 𝑄 𝐺 )
6 eqid ( deg1𝑅 ) = ( deg1𝑅 )
7 eqid ( -g𝑃 ) = ( -g𝑃 )
8 eqid ( .r𝑃 ) = ( .r𝑃 )
9 1 2 3 6 7 8 4 q1peqb ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐶 ) → ( ( ( 𝐹 𝑄 𝐺 ) ∈ 𝐵 ∧ ( ( deg1𝑅 ) ‘ ( 𝐹 ( -g𝑃 ) ( ( 𝐹 𝑄 𝐺 ) ( .r𝑃 ) 𝐺 ) ) ) < ( ( deg1𝑅 ) ‘ 𝐺 ) ) ↔ ( 𝐹 𝑄 𝐺 ) = ( 𝐹 𝑄 𝐺 ) ) )
10 5 9 mpbiri ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐶 ) → ( ( 𝐹 𝑄 𝐺 ) ∈ 𝐵 ∧ ( ( deg1𝑅 ) ‘ ( 𝐹 ( -g𝑃 ) ( ( 𝐹 𝑄 𝐺 ) ( .r𝑃 ) 𝐺 ) ) ) < ( ( deg1𝑅 ) ‘ 𝐺 ) ) )
11 10 simpld ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐶 ) → ( 𝐹 𝑄 𝐺 ) ∈ 𝐵 )