ldualkrsc

Description: The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 28-Dec-2014)

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

Metamath Proof Explorer