lkrss

Description: The kernel of a scalar product of a functional includes the kernel of the functional. (Contributed by NM, 27-Jan-2015)

	Ref	Expression
Hypotheses	lkrss.r	$⊢ R = Scalar (W)$
	lkrss.k	$⊢ K = {Base}_{R}$
	lkrss.f	$⊢ F = LFnl (W)$
	lkrss.l	$⊢ L = LKer (W)$
	lkrss.d	$⊢ D = LDual (W)$
	lkrss.s	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	lkrss.w	$⊢ φ \to W \in LVec$
	lkrss.g	$⊢ φ \to G \in F$
	lkrss.x	$⊢ φ \to X \in K$
Assertion	lkrss	$⊢ φ \to L (G) \subseteq L (X \underset{˙}{\cdot} G)$

Step	Hyp	Ref	Expression
1		lkrss.r	$⊢ R = Scalar (W)$
2		lkrss.k	$⊢ K = {Base}_{R}$
3		lkrss.f	$⊢ F = LFnl (W)$
4		lkrss.l	$⊢ L = LKer (W)$
5		lkrss.d	$⊢ D = LDual (W)$
6		lkrss.s	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
7		lkrss.w	$⊢ φ \to W \in LVec$
8		lkrss.g	$⊢ φ \to G \in F$
9		lkrss.x	$⊢ φ \to X \in K$
10		eqid	$⊢ {Base}_{W} = {Base}_{W}$
11		eqid	$⊢ \cdot_{R} = \cdot_{R}$
12	10 1 2 11 3 4 7 8 9	lkrscss	$⊢ φ \to L (G) \subseteq L (G {\cdot_{R}}_{f} ({Base}_{W} \times \{X\}))$
13	3 10 1 2 11 5 6 7 9 8	ldualvs	$⊢ φ \to X \underset{˙}{\cdot} G = G {\cdot_{R}}_{f} ({Base}_{W} \times \{X\})$
14	13	fveq2d	$⊢ φ \to L (X \underset{˙}{\cdot} G) = L (G {\cdot_{R}}_{f} ({Base}_{W} \times \{X\}))$
15	12 14	sseqtrrd	$⊢ φ \to L (G) \subseteq L (X \underset{˙}{\cdot} G)$

Metamath Proof Explorer