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

Metamath Proof Explorer

Theorem ply1asclunit

Description: A non-zero 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 ‘ 𝑃 ) )