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

Metamath Proof Explorer

Theorem ressasclcl

Description: Closure of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 22-Jun-2025)

Ref Expression
Hypotheses ressasclcl.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
ressasclcl.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
ressasclcl.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
ressasclcl.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
ressasclcl.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
ressasclcl.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
ressasclcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
Assertion ressasclcl ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ressasclcl.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
2 ressasclcl.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
3 ressasclcl.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
4 ressasclcl.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
5 ressasclcl.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
6 ressasclcl.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
7 ressasclcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
8 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
9 8 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ ( Base ‘ 𝑆 ) )
10 2 8 ressbas2 ⊢ ( 𝑅 ⊆ ( Base ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) )
11 6 9 10 3syl ⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
12 2 subrgcrng ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
13 5 6 12 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ CRing )
14 1 ply1sca ⊢ ( 𝑈 ∈ CRing → 𝑈 = ( Scalar ‘ 𝑊 ) )
15 13 14 syl ⊢ ( 𝜑 → 𝑈 = ( Scalar ‘ 𝑊 ) )
16 15 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
17 11 16 eqtrd ⊢ ( 𝜑 → 𝑅 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
18 7 17 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
19 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
20 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
21 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
22 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
23 3 19 20 21 22 asclval ⊢ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
24 18 23 syl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
25 13 crngringd ⊢ ( 𝜑 → 𝑈 ∈ Ring )
26 1 ply1lmod ⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ LMod )
27 25 26 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
28 1 ply1ring ⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ Ring )
29 4 22 ringidcl ⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
30 25 28 29 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
31 4 19 21 20 27 18 30 lmodvscld ⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ 𝐵 )
32 24 31 eqeltrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 )