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	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ 𝑃 )