Theorem lfl0sc

Description: The (right vector space) scalar product of a functional with zero is the zero functional. Note that the first occurrence of ( V X. { .0. } ) represents the zero scalar, and the second is the zero functional. (Contributed by NM, 7-Oct-2014)

	Ref	Expression
Hypotheses	lfl0sc.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lfl0sc.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	lfl0sc.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lfl0sc.k	⊢ 𝐾 = ( Base ‘ 𝐷 )
	lfl0sc.t	⊢ · = ( .r ‘ 𝐷 )
	lfl0sc.o	⊢ 0 = ( 0g ‘ 𝐷 )
	lfl0sc.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lfl0sc.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lfl0sc	⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 0 } ) ) = ( 𝑉 × { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		lfl0sc.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lfl0sc.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3		lfl0sc.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4		lfl0sc.k	⊢ 𝐾 = ( Base ‘ 𝐷 )
5		lfl0sc.t	⊢ · = ( .r ‘ 𝐷 )
6		lfl0sc.o	⊢ 0 = ( 0g ‘ 𝐷 )
7		lfl0sc.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
8		lfl0sc.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9	1	fvexi	⊢ 𝑉 ∈ V
10	9	a1i	⊢ ( 𝜑 → 𝑉 ∈ V )
11	2 4 1 3	lflf	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
12	7 8 11	syl2anc	⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
13	2	lmodring	⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Ring )
14	7 13	syl	⊢ ( 𝜑 → 𝐷 ∈ Ring )
15	4 6	ring0cl	⊢ ( 𝐷 ∈ Ring → 0 ∈ 𝐾 )
16	14 15	syl	⊢ ( 𝜑 → 0 ∈ 𝐾 )
17	4 5 6	ringrz	⊢ ( ( 𝐷 ∈ Ring ∧ 𝑘 ∈ 𝐾 ) → ( 𝑘 · 0 ) = 0 )
18	14 17	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝑘 · 0 ) = 0 )
19	10 12 16 16 18	caofid1	⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 0 } ) ) = ( 𝑉 × { 0 } ) )