lkrsc

Description: The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (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$
	lkrsc.o	$⊢ \underset{˙}{0} = 0_{D}$
	lkrsc.e	$⊢ φ \to R \neq \underset{˙}{0}$
Assertion	lkrsc	$⊢ φ \to L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) = L (G)$

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		lkrsc.o	$⊢ \underset{˙}{0} = 0_{D}$
11		lkrsc.e	$⊢ φ \to R \neq \underset{˙}{0}$
12	1	fvexi	$⊢ V \in V$
13	12	a1i	$⊢ φ \to V \in V$
14	2 3 1 5	lflf	$⊢ (W \in LVec \land G \in F) \to G : V ⟶ K$
15	7 8 14	syl2anc	$⊢ φ \to G : V ⟶ K$
16	15	ffnd	$⊢ φ \to G Fn V$
17		eqidd	$⊢ (φ \land v \in V) \to G (v) = G (v)$
18	13 9 16 17	ofc2	$⊢ (φ \land v \in V) \to (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (v) = G (v) \underset{˙}{\cdot} R$
19	18	eqeq1d	$⊢ (φ \land v \in V) \to ((G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (v) = \underset{˙}{0} \leftrightarrow G (v) \underset{˙}{\cdot} R = \underset{˙}{0})$
20	2	lvecdrng	$⊢ W \in LVec \to D \in DivRing$
21	7 20	syl	$⊢ φ \to D \in DivRing$
22	21	adantr	$⊢ (φ \land v \in V) \to D \in DivRing$
23	7	adantr	$⊢ (φ \land v \in V) \to W \in LVec$
24	8	adantr	$⊢ (φ \land v \in V) \to G \in F$
25		simpr	$⊢ (φ \land v \in V) \to v \in V$
26	2 3 1 5	lflcl	$⊢ (W \in LVec \land G \in F \land v \in V) \to G (v) \in K$
27	23 24 25 26	syl3anc	$⊢ (φ \land v \in V) \to G (v) \in K$
28	9	adantr	$⊢ (φ \land v \in V) \to R \in K$
29	11	adantr	$⊢ (φ \land v \in V) \to R \neq \underset{˙}{0}$
30	3 10 4 22 27 28 29	drngmuleq0	$⊢ (φ \land v \in V) \to (G (v) \underset{˙}{\cdot} R = \underset{˙}{0} \leftrightarrow G (v) = \underset{˙}{0})$
31	19 30	bitrd	$⊢ (φ \land v \in V) \to ((G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (v) = \underset{˙}{0} \leftrightarrow G (v) = \underset{˙}{0})$
32	31	pm5.32da	$⊢ φ \to ((v \in V \land (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (v) = \underset{˙}{0}) \leftrightarrow (v \in V \land G (v) = \underset{˙}{0}))$
33		lveclmod	$⊢ W \in LVec \to W \in LMod$
34	7 33	syl	$⊢ φ \to W \in LMod$
35	1 2 3 4 5 34 8 9	lflvscl	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{R\}) \in F$
36	1 2 10 5 6	ellkr	$⊢ (W \in LVec \land G {\underset{˙}{\cdot}}_{f} (V \times \{R\}) \in F) \to (v \in L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) \leftrightarrow (v \in V \land (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (v) = \underset{˙}{0}))$
37	7 35 36	syl2anc	$⊢ φ \to (v \in L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) \leftrightarrow (v \in V \land (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (v) = \underset{˙}{0}))$
38	1 2 10 5 6	ellkr	$⊢ (W \in LVec \land G \in F) \to (v \in L (G) \leftrightarrow (v \in V \land G (v) = \underset{˙}{0}))$
39	7 8 38	syl2anc	$⊢ φ \to (v \in L (G) \leftrightarrow (v \in V \land G (v) = \underset{˙}{0}))$
40	32 37 39	3bitr4d	$⊢ φ \to (v \in L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) \leftrightarrow v \in L (G))$
41	40	eqrdv	$⊢ φ \to L (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) = L (G)$

Metamath Proof Explorer

Theorem lkrsc

Proof