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

Metamath Proof Explorer

Theorem mon1puc1p

Description: Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015)

		Ref	Expression
	Hypotheses	mon1puc1p.c	⊢ 𝐶 = ( Unic_1p ‘ 𝑅 )
		mon1puc1p.m	⊢ 𝑀 = ( Monic_1p ‘ 𝑅 )
	Assertion	mon1puc1p	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀 ) → 𝑋 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mon1puc1p.c	⊢ 𝐶 = ( Unic_1p ‘ 𝑅 )
2		mon1puc1p.m	⊢ 𝑀 = ( Monic_1p ‘ 𝑅 )
3		eqid	⊢ ( Poly₁ ‘ 𝑅 ) = ( Poly₁ ‘ 𝑅 )
4		eqid	⊢ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) = ( Base ‘ ( Poly₁ ‘ 𝑅 ) )
5	3 4 2	mon1pcl	⊢ ( 𝑋 ∈ 𝑀 → 𝑋 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
6	5	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀 ) → 𝑋 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
7		eqid	⊢ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) = ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) )
8	3 7 2	mon1pn0	⊢ ( 𝑋 ∈ 𝑀 → 𝑋 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
9	8	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀 ) → 𝑋 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) )
10		eqid	⊢ ( deg₁ ‘ 𝑅 ) = ( deg₁ ‘ 𝑅 )
11		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
12	10 11 2	mon1pldg	⊢ ( 𝑋 ∈ 𝑀 → ( ( coe₁ ‘ 𝑋 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑋 ) ) = ( 1_r ‘ 𝑅 ) )
13	12	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀 ) → ( ( coe₁ ‘ 𝑋 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑋 ) ) = ( 1_r ‘ 𝑅 ) )
14		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
15	14 11	1unit	⊢ ( 𝑅 ∈ Ring → ( 1_r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
16	15	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀 ) → ( 1_r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
17	13 16	eqeltrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀 ) → ( ( coe₁ ‘ 𝑋 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑋 ) ) ∈ ( Unit ‘ 𝑅 ) )
18	3 4 7 10 1 14	isuc1p	⊢ ( 𝑋 ∈ 𝐶 ↔ ( 𝑋 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ 𝑋 ≠ ( 0_g ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ ( ( coe₁ ‘ 𝑋 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑋 ) ) ∈ ( Unit ‘ 𝑅 ) ) )
19	6 9 17 18	syl3anbrc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑀 ) → 𝑋 ∈ 𝐶 )