lkrscss

Description: The kernel of a scalar product of a functional includes the kernel of the functional. (The inclusion is proper for the zero product and equality otherwise.) (Contributed by NM, 9-Oct-2014)

	Ref	Expression
Hypotheses	lkrsc.v	$⊢ V = {Base}_{W}$
	lkrsc.d	$⊢ D = Scalar (W)$
	lkrsc.k	$⊢ K = {Base}_{D}$
	lkrsc.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	lkrsc.f	$⊢ F = LFnl (W)$
	lkrsc.l	$⊢ L = LKer (W)$
	lkrsc.w	$⊢ φ \to W \in LVec$
	lkrsc.g	$⊢ φ \to G \in F$
	lkrsc.r	$⊢ φ \to R \in K$
Assertion	lkrscss	$⊢ φ \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\}))$

Proof

Step	Hyp	Ref	Expression
1		lkrsc.v	$⊢ V = {Base}_{W}$
2		lkrsc.d	$⊢ D = Scalar (W)$
3		lkrsc.k	$⊢ K = {Base}_{D}$
4		lkrsc.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
5		lkrsc.f	$⊢ F = LFnl (W)$
6		lkrsc.l	$⊢ L = LKer (W)$
7		lkrsc.w	$⊢ φ \to W \in LVec$
8		lkrsc.g	$⊢ φ \to G \in F$
9		lkrsc.r	$⊢ φ \to R \in K$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	7 10	syl	$⊢ φ \to W \in LMod$
12	1 5 6 11 8	lkrssv	$⊢ φ \to L (G) \subseteq V$
13		eqid	$⊢ 0_{D} = 0_{D}$
14	1 2 5 3 4 13 11 8	lfl0sc	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\}) = V \times \{0_{D}\}$
15	14	fveq2d	$⊢ φ \to L (G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\})) = L (V \times \{0_{D}\})$
16		eqid	$⊢ V \times \{0_{D}\} = V \times \{0_{D}\}$
17	2 13 1 5	lfl0f	$⊢ W \in LMod \to V \times \{0_{D}\} \in F$
18	2 13 1 5 6	lkr0f	$⊢ (W \in LMod \land V \times \{0_{D}\} \in F) \to (L (V \times \{0_{D}\}) = V \leftrightarrow V \times \{0_{D}\} = V \times \{0_{D}\})$
19	11 17 18	syl2anc2	$⊢ φ \to (L (V \times \{0_{D}\}) = V \leftrightarrow V \times \{0_{D}\} = V \times \{0_{D}\})$
20	16 19	mpbiri	$⊢ φ \to L (V \times \{0_{D}\}) = V$
21	15 20	eqtr2d	$⊢ φ \to V = L (G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\}))$
22	12 21	sseqtrd	$⊢ φ \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\}))$
23	22	adantr	$⊢ (φ \land R = 0_{D}) \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\}))$
24		sneq	$⊢ R = 0_{D} \to \{R\} = \{0_{D}\}$
25	24	xpeq2d	$⊢ R = 0_{D} \to V \times \{R\} = V \times \{0_{D}\}$
26	25	oveq2d	$⊢ R = 0_{D} \to G {\underset{˙}{\cdot}}_{f} (V \times \{R\}) = G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\})$
27	26	fveq2d	$⊢ R = 0_{D} \to L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) = L (G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\}))$
28	27	adantl	$⊢ (φ \land R = 0_{D}) \to L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) = L (G {\underset{˙}{\cdot}}_{f} (V \times \{0_{D}\}))$
29	23 28	sseqtrrd	$⊢ (φ \land R = 0_{D}) \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\}))$
30	7	adantr	$⊢ (φ \land R \neq 0_{D}) \to W \in LVec$
31	8	adantr	$⊢ (φ \land R \neq 0_{D}) \to G \in F$
32	9	adantr	$⊢ (φ \land R \neq 0_{D}) \to R \in K$
33		simpr	$⊢ (φ \land R \neq 0_{D}) \to R \neq 0_{D}$
34	1 2 3 4 5 6 30 31 32 13 33	lkrsc	$⊢ (φ \land R \neq 0_{D}) \to L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) = L (G)$
35		eqimss2	$⊢ L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) = L (G) \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\}))$
36	34 35	syl	$⊢ (φ \land R \neq 0_{D}) \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\}))$
37	29 36	pm2.61dane	$⊢ φ \to L (G) \subseteq L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\}))$

Metamath Proof Explorer

Theorem lkrscss

Proof