Theorem ply1asclunit

Description: A nonzero scalar polynomial over a field F is a unit. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	ply1asclunit.1	⊢ 𝑃 = ( Poly1 ‘ 𝐹 )
	ply1asclunit.2	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	ply1asclunit.3	⊢ 𝐵 = ( Base ‘ 𝐹 )
	ply1asclunit.4	⊢ 0 = ( 0g ‘ 𝐹 )
	ply1asclunit.5	⊢ ( 𝜑 → 𝐹 ∈ Field )
	ply1asclunit.6	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	ply1asclunit.7	⊢ ( 𝜑 → 𝑌 ≠ 0 )
Assertion	ply1asclunit	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑌 ) ∈ ( Unit ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1asclunit.1	⊢ 𝑃 = ( Poly1 ‘ 𝐹 )
2		ply1asclunit.2	⊢ 𝐴 = ( algSc ‘ 𝑃 )
3		ply1asclunit.3	⊢ 𝐵 = ( Base ‘ 𝐹 )
4		ply1asclunit.4	⊢ 0 = ( 0g ‘ 𝐹 )
5		ply1asclunit.5	⊢ ( 𝜑 → 𝐹 ∈ Field )
6		ply1asclunit.6	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		ply1asclunit.7	⊢ ( 𝜑 → 𝑌 ≠ 0 )
8	5	fldcrngd	⊢ ( 𝜑 → 𝐹 ∈ CRing )
9	1	ply1assa	⊢ ( 𝐹 ∈ CRing → 𝑃 ∈ AssAlg )
10		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
11	2 10	asclrhm	⊢ ( 𝑃 ∈ AssAlg → 𝐴 ∈ ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
12	8 9 11	3syl	⊢ ( 𝜑 → 𝐴 ∈ ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
13	1	ply1sca	⊢ ( 𝐹 ∈ Field → 𝐹 = ( Scalar ‘ 𝑃 ) )
14	5 13	syl	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑃 ) )
15	14	oveq1d	⊢ ( 𝜑 → ( 𝐹 RingHom 𝑃 ) = ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
16	12 15	eleqtrrd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 RingHom 𝑃 ) )
17	5	flddrngd	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
18		eqid	⊢ ( Unit ‘ 𝐹 ) = ( Unit ‘ 𝐹 )
19	3 18 4	drngunit	⊢ ( 𝐹 ∈ DivRing → ( 𝑌 ∈ ( Unit ‘ 𝐹 ) ↔ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) ) )
20	19	biimpar	⊢ ( ( 𝐹 ∈ DivRing ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) ) → 𝑌 ∈ ( Unit ‘ 𝐹 ) )
21	17 6 7 20	syl12anc	⊢ ( 𝜑 → 𝑌 ∈ ( Unit ‘ 𝐹 ) )
22		elrhmunit	⊢ ( ( 𝐴 ∈ ( 𝐹 RingHom 𝑃 ) ∧ 𝑌 ∈ ( Unit ‘ 𝐹 ) ) → ( 𝐴 ‘ 𝑌 ) ∈ ( Unit ‘ 𝑃 ) )
23	16 21 22	syl2anc	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑌 ) ∈ ( Unit ‘ 𝑃 ) )