Theorem psrascl

Description: Value of the scalar injection into the power series algebra. (Contributed by SN, 18-May-2025)

	Ref	Expression
Hypotheses	psrascl.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrascl.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	psrascl.z	⊢ 0 = ( 0g ‘ 𝑅 )
	psrascl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	psrascl.a	⊢ 𝐴 = ( algSc ‘ 𝑆 )
	psrascl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	psrascl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	psrascl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
Assertion	psrascl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psrascl.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrascl.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3		psrascl.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		psrascl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5		psrascl.a	⊢ 𝐴 = ( algSc ‘ 𝑆 )
6		psrascl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7		psrascl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		psrascl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
9	1 6 7	psrsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) )
10	9	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
11	4 10	eqtrid	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
12	8 11	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
13		eqid	⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
14		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
15		eqid	⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
16		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
17	5 13 14 15 16	asclval	⊢ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
18	12 17	syl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
19		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
20		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
21	1 6 7	psrring	⊢ ( 𝜑 → 𝑆 ∈ Ring )
22	19 16	ringidcl	⊢ ( 𝑆 ∈ Ring → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
23	21 22	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
24	1 15 4 19 20 2 8 23	psrvsca	⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = ( ( 𝐷 × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) ( 1r ‘ 𝑆 ) ) )
25		fnconstg	⊢ ( 𝑋 ∈ 𝐾 → ( 𝐷 × { 𝑋 } ) Fn 𝐷 )
26	8 25	syl	⊢ ( 𝜑 → ( 𝐷 × { 𝑋 } ) Fn 𝐷 )
27	1 4 2 19 23	psrelbas	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) : 𝐷 ⟶ 𝐾 )
28	27	ffnd	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) Fn 𝐷 )
29		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V )
30	2 29	rabexd	⊢ ( 𝜑 → 𝐷 ∈ V )
31		inidm	⊢ ( 𝐷 ∩ 𝐷 ) = 𝐷
32		fvconst2g	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐷 × { 𝑋 } ) ‘ 𝑦 ) = 𝑋 )
33	8 32	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐷 × { 𝑋 } ) ‘ 𝑦 ) = 𝑋 )
34		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
35	1 6 7 2 3 34 16	psr1	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 1r ‘ 𝑆 ) = ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) )
37	36	fveq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 1r ‘ 𝑆 ) ‘ 𝑦 ) = ( ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ‘ 𝑦 ) )
38		eqeq1	⊢ ( 𝑑 = 𝑦 → ( 𝑑 = ( 𝐼 × { 0 } ) ↔ 𝑦 = ( 𝐼 × { 0 } ) ) )
39	38	ifbid	⊢ ( 𝑑 = 𝑦 → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) )
40		eqid	⊢ ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) = ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) )
41		fvex	⊢ ( 1r ‘ 𝑅 ) ∈ V
42	3	fvexi	⊢ 0 ∈ V
43	41 42	ifex	⊢ if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ∈ V
44	39 40 43	fvmpt	⊢ ( 𝑦 ∈ 𝐷 → ( ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ‘ 𝑦 ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) )
45	44	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ‘ 𝑦 ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) )
46	37 45	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 1r ‘ 𝑆 ) ‘ 𝑦 ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) )
47	26 28 30 30 31 33 46	offval	⊢ ( 𝜑 → ( ( 𝐷 × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) ( 1r ‘ 𝑆 ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) )
48		ovif2	⊢ ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 𝑋 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) , ( 𝑋 ( .r ‘ 𝑅 ) 0 ) )
49	4 20 34 7 8	ringridmd	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑋 )
50	4 20 3 7 8	ringrzd	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) 0 ) = 0 )
51	49 50	ifeq12d	⊢ ( 𝜑 → if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 𝑋 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) , ( 𝑋 ( .r ‘ 𝑅 ) 0 ) ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) )
52	48 51	eqtrid	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) )
53	52	mpteq2dv	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )
54	47 53	eqtrd	⊢ ( 𝜑 → ( ( 𝐷 × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) ( 1r ‘ 𝑆 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )
55	18 24 54	3eqtrd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )