Theorem frlmvscafval

Description: Scalar multiplication in a free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Hypotheses	frlmvscafval.y	⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
	frlmvscafval.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	frlmvscafval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	frlmvscafval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	frlmvscafval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	frlmvscafval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	frlmvscafval.v	⊢ ∙ = ( ·𝑠 ‘ 𝑌 )
	frlmvscafval.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	frlmvscafval	⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		frlmvscafval.y	⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
2		frlmvscafval.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		frlmvscafval.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		frlmvscafval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		frlmvscafval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
6		frlmvscafval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		frlmvscafval.v	⊢ ∙ = ( ·𝑠 ‘ 𝑌 )
8		frlmvscafval.t	⊢ · = ( .r ‘ 𝑅 )
9	1 2	frlmrcl	⊢ ( 𝑋 ∈ 𝐵 → 𝑅 ∈ V )
10	6 9	syl	⊢ ( 𝜑 → 𝑅 ∈ V )
11	1 2	frlmpws	⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
12	10 4 11	syl2anc	⊢ ( 𝜑 → 𝑌 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
13	12	fveq2d	⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
14	2	fvexi	⊢ 𝐵 ∈ V
15		eqid	⊢ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 )
16		eqid	⊢ ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
17	15 16	ressvsca	⊢ ( 𝐵 ∈ V → ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( ·𝑠 ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
18	14 17	ax-mp	⊢ ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( ·𝑠 ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) )
19	13 7 18	3eqtr4g	⊢ ( 𝜑 → ∙ = ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
20	19	oveqd	⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) = ( 𝐴 ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝑋 ) )
21		eqid	⊢ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
22		eqid	⊢ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
23		rlmvsca	⊢ ( .r ‘ 𝑅 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
24	8 23	eqtri	⊢ · = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
25		eqid	⊢ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
26		eqid	⊢ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
27		fvexd	⊢ ( 𝜑 → ( ringLMod ‘ 𝑅 ) ∈ V )
28		rlmsca	⊢ ( 𝑅 ∈ V → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
29	10 28	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
30	29	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
31	3 30	eqtrid	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
32	5 31	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
33	12	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
34	2 33	eqtrid	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) )
35	15 22	ressbasss	⊢ ( Base ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s 𝐵 ) ) ⊆ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
36	34 35	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
37	36 6	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
38	21 22 24 16 25 26 27 4 32 37	pwsvscafval	⊢ ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) 𝑋 ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )
39	20 38	eqtrd	⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )