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

Metamath Proof Explorer

Theorem asclply1subcl

Description: Closure of the algebra scalar injection function in a polynomial on a subring. (Contributed by Thierry Arnoux, 5-Feb-2025)

Ref Expression
Hypotheses asclply1subcl.1 ⊢ 𝐴 = ( algSc ‘ 𝑉 )
asclply1subcl.2 ⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
asclply1subcl.3 ⊢ 𝑉 = ( Poly1 ‘ 𝑅 )
asclply1subcl.4 ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
asclply1subcl.5 ⊢ 𝑃 = ( Base ‘ 𝑊 )
asclply1subcl.6 ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
asclply1subcl.7 ⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
Assertion asclply1subcl ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 asclply1subcl.1 ⊢ 𝐴 = ( algSc ‘ 𝑉 )
2 asclply1subcl.2 ⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
3 asclply1subcl.3 ⊢ 𝑉 = ( Poly1 ‘ 𝑅 )
4 asclply1subcl.4 ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
5 asclply1subcl.5 ⊢ 𝑃 = ( Base ‘ 𝑊 )
6 asclply1subcl.6 ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7 asclply1subcl.7 ⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 8 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
10 6 9 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
11 10 7 sseldd ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝑅 ) )
12 subrgrcl ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
13 3 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑉 ) )
14 6 12 13 3syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑉 ) )
15 14 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑉 ) ) )
16 11 15 eleqtrd ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) )
17 eqid ⊢ ( Scalar ‘ 𝑉 ) = ( Scalar ‘ 𝑉 )
18 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑉 ) ) = ( Base ‘ ( Scalar ‘ 𝑉 ) )
19 eqid ⊢ ( ·𝑠 ‘ 𝑉 ) = ( ·𝑠 ‘ 𝑉 )
20 eqid ⊢ ( 1r ‘ 𝑉 ) = ( 1r ‘ 𝑉 )
21 1 17 18 19 20 asclval ⊢ ( 𝑍 ∈ ( Base ‘ ( Scalar ‘ 𝑉 ) ) → ( 𝐴 ‘ 𝑍 ) = ( 𝑍 ( ·𝑠 ‘ 𝑉 ) ( 1r ‘ 𝑉 ) ) )
22 16 21 syl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) = ( 𝑍 ( ·𝑠 ‘ 𝑉 ) ( 1r ‘ 𝑉 ) ) )
23 3 2 4 5 subrgply1 ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑃 ∈ ( SubRing ‘ 𝑉 ) )
24 eqid ⊢ ( 𝑉 ↾s 𝑃 ) = ( 𝑉 ↾s 𝑃 )
25 24 19 ressvsca ⊢ ( 𝑃 ∈ ( SubRing ‘ 𝑉 ) → ( ·𝑠 ‘ 𝑉 ) = ( ·𝑠 ‘ ( 𝑉 ↾s 𝑃 ) ) )
26 6 23 25 3syl ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑉 ) = ( ·𝑠 ‘ ( 𝑉 ↾s 𝑃 ) ) )
27 26 oveqd ⊢ ( 𝜑 → ( 𝑍 ( ·𝑠 ‘ 𝑉 ) ( 1r ‘ 𝑉 ) ) = ( 𝑍 ( ·𝑠 ‘ ( 𝑉 ↾s 𝑃 ) ) ( 1r ‘ 𝑉 ) ) )
28 id ⊢ ( 𝜑 → 𝜑 )
29 20 subrg1cl ⊢ ( 𝑃 ∈ ( SubRing ‘ 𝑉 ) → ( 1r ‘ 𝑉 ) ∈ 𝑃 )
30 6 23 29 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝑉 ) ∈ 𝑃 )
31 3 2 4 5 6 24 ressply1vsca ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ 𝑆 ∧ ( 1r ‘ 𝑉 ) ∈ 𝑃 ) ) → ( 𝑍 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑉 ) ) = ( 𝑍 ( ·𝑠 ‘ ( 𝑉 ↾s 𝑃 ) ) ( 1r ‘ 𝑉 ) ) )
32 28 7 30 31 syl12anc ⊢ ( 𝜑 → ( 𝑍 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑉 ) ) = ( 𝑍 ( ·𝑠 ‘ ( 𝑉 ↾s 𝑃 ) ) ( 1r ‘ 𝑉 ) ) )
33 27 32 eqtr4d ⊢ ( 𝜑 → ( 𝑍 ( ·𝑠 ‘ 𝑉 ) ( 1r ‘ 𝑉 ) ) = ( 𝑍 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑉 ) ) )
34 2 subrgring ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑈 ∈ Ring )
35 4 ply1lmod ⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ LMod )
36 6 34 35 3syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
37 2 8 ressbas2 ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑅 ) → 𝑆 = ( Base ‘ 𝑈 ) )
38 6 9 37 3syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝑈 ) )
39 7 38 eleqtrd ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝑈 ) )
40 2 ovexi ⊢ 𝑈 ∈ V
41 4 ply1sca ⊢ ( 𝑈 ∈ V → 𝑈 = ( Scalar ‘ 𝑊 ) )
42 40 41 ax-mp ⊢ 𝑈 = ( Scalar ‘ 𝑊 )
43 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
44 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
45 5 42 43 44 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ ( Base ‘ 𝑈 ) ∧ ( 1r ‘ 𝑉 ) ∈ 𝑃 ) → ( 𝑍 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑉 ) ) ∈ 𝑃 )
46 36 39 30 45 syl3anc ⊢ ( 𝜑 → ( 𝑍 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑉 ) ) ∈ 𝑃 )
47 33 46 eqeltrd ⊢ ( 𝜑 → ( 𝑍 ( ·𝑠 ‘ 𝑉 ) ( 1r ‘ 𝑉 ) ) ∈ 𝑃 )
48 22 47 eqeltrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ 𝑃 )