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	|- V = ( Base ` W )
	lfl0sc.d	|- D = ( Scalar ` W )
	lfl0sc.f	|- F = ( LFnl ` W )
	lfl0sc.k	|- K = ( Base ` D )
	lfl0sc.t	|- .x. = ( .r ` D )
	lfl0sc.o	|- .0. = ( 0g ` D )
	lfl0sc.w	|- ( ph -> W e. LMod )
	lfl0sc.g	|- ( ph -> G e. F )
Assertion	lfl0sc	|- ( ph -> ( G oF .x. ( V X. { .0. } ) ) = ( V X. { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		lfl0sc.v	|- V = ( Base ` W )
2		lfl0sc.d	|- D = ( Scalar ` W )
3		lfl0sc.f	|- F = ( LFnl ` W )
4		lfl0sc.k	|- K = ( Base ` D )
5		lfl0sc.t	|- .x. = ( .r ` D )
6		lfl0sc.o	|- .0. = ( 0g ` D )
7		lfl0sc.w	|- ( ph -> W e. LMod )
8		lfl0sc.g	|- ( ph -> G e. F )
9	1	fvexi	|- V e. _V
10	9	a1i	|- ( ph -> V e. _V )
11	2 4 1 3	lflf	|- ( ( W e. LMod /\ G e. F ) -> G : V --> K )
12	7 8 11	syl2anc	|- ( ph -> G : V --> K )
13	2	lmodring	|- ( W e. LMod -> D e. Ring )
14	7 13	syl	|- ( ph -> D e. Ring )
15	4 6	ring0cl	|- ( D e. Ring -> .0. e. K )
16	14 15	syl	|- ( ph -> .0. e. K )
17	4 5 6	ringrz	|- ( ( D e. Ring /\ k e. K ) -> ( k .x. .0. ) = .0. )
18	14 17	sylan	|- ( ( ph /\ k e. K ) -> ( k .x. .0. ) = .0. )
19	10 12 16 16 18	caofid1	|- ( ph -> ( G oF .x. ( V X. { .0. } ) ) = ( V X. { .0. } ) )