lclkrlem1

Description: The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014)

	Ref	Expression
Hypotheses	lclkrlem1.h	$⊢ H = LHyp (K)$
	lclkrlem1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lclkrlem1.u	$⊢ U = DVecH (K) (W)$
	lclkrlem1.f	$⊢ F = LFnl (U)$
	lclkrlem1.l	$⊢ L = LKer (U)$
	lclkrlem1.d	$⊢ D = LDual (U)$
	lclkrlem1.r	$⊢ R = Scalar (U)$
	lclkrlem1.b	$⊢ B = {Base}_{R}$
	lclkrlem1.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	lclkrlem1.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
	lclkrlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
	lclkrlem1.x	$⊢ φ \to X \in B$
	lclkrlem1.g	$⊢ φ \to G \in C$
Assertion	lclkrlem1	$⊢ φ \to X \underset{˙}{\cdot} G \in C$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem1.h	$⊢ H = LHyp (K)$
2		lclkrlem1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lclkrlem1.u	$⊢ U = DVecH (K) (W)$
4		lclkrlem1.f	$⊢ F = LFnl (U)$
5		lclkrlem1.l	$⊢ L = LKer (U)$
6		lclkrlem1.d	$⊢ D = LDual (U)$
7		lclkrlem1.r	$⊢ R = Scalar (U)$
8		lclkrlem1.b	$⊢ B = {Base}_{R}$
9		lclkrlem1.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
10		lclkrlem1.c	$⊢ C = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
11		lclkrlem1.k	$⊢ φ \to (K \in HL \land W \in H)$
12		lclkrlem1.x	$⊢ φ \to X \in B$
13		lclkrlem1.g	$⊢ φ \to G \in C$
14	1 3 11	dvhlmod	$⊢ φ \to U \in LMod$
15	10	lcfl1lem	$⊢ G \in C \leftrightarrow (G \in F \land \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G))$
16	13 15	sylib	$⊢ φ \to (G \in F \land \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G))$
17	16	simpld	$⊢ φ \to G \in F$
18	4 7 8 6 9 14 12 17	ldualvscl	$⊢ φ \to X \underset{˙}{\cdot} G \in F$
19		eqid	$⊢ {Base}_{U} = {Base}_{U}$
20	1 3 2 19 11	dochoc1	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} ({Base}_{U})) = {Base}_{U}$
21	20	adantr	$⊢ (φ \land X = 0_{R}) \to \underset{˙}{⊥} (\underset{˙}{⊥} ({Base}_{U})) = {Base}_{U}$
22		fvoveq1	$⊢ X = 0_{R} \to L (X \underset{˙}{\cdot} G) = L (0_{R} \underset{˙}{\cdot} G)$
23	6 14	lduallmod	$⊢ φ \to D \in LMod$
24		eqid	$⊢ {Base}_{D} = {Base}_{D}$
25	4 6 24 14 17	ldualelvbase	$⊢ φ \to G \in {Base}_{D}$
26		eqid	$⊢ Scalar (D) = Scalar (D)$
27		eqid	$⊢ 0_{Scalar (D)} = 0_{Scalar (D)}$
28		eqid	$⊢ 0_{D} = 0_{D}$
29	24 26 9 27 28	lmod0vs	$⊢ (D \in LMod \land G \in {Base}_{D}) \to 0_{Scalar (D)} \underset{˙}{\cdot} G = 0_{D}$
30	23 25 29	syl2anc	$⊢ φ \to 0_{Scalar (D)} \underset{˙}{\cdot} G = 0_{D}$
31		eqid	$⊢ 0_{R} = 0_{R}$
32	7 31 6 26 27 14	ldual0	$⊢ φ \to 0_{Scalar (D)} = 0_{R}$
33	32	oveq1d	$⊢ φ \to 0_{Scalar (D)} \underset{˙}{\cdot} G = 0_{R} \underset{˙}{\cdot} G$
34	19 7 31 6 28 14	ldual0v	$⊢ φ \to 0_{D} = {Base}_{U} \times \{0_{R}\}$
35	30 33 34	3eqtr3d	$⊢ φ \to 0_{R} \underset{˙}{\cdot} G = {Base}_{U} \times \{0_{R}\}$
36	35	fveq2d	$⊢ φ \to L (0_{R} \underset{˙}{\cdot} G) = L ({Base}_{U} \times \{0_{R}\})$
37		eqid	$⊢ {Base}_{U} \times \{0_{R}\} = {Base}_{U} \times \{0_{R}\}$
38	7 31 19 4	lfl0f	$⊢ U \in LMod \to {Base}_{U} \times \{0_{R}\} \in F$
39	7 31 19 4 5	lkr0f	$⊢ (U \in LMod \land {Base}_{U} \times \{0_{R}\} \in F) \to (L ({Base}_{U} \times \{0_{R}\}) = {Base}_{U} \leftrightarrow {Base}_{U} \times \{0_{R}\} = {Base}_{U} \times \{0_{R}\})$
40	14 38 39	syl2anc2	$⊢ φ \to (L ({Base}_{U} \times \{0_{R}\}) = {Base}_{U} \leftrightarrow {Base}_{U} \times \{0_{R}\} = {Base}_{U} \times \{0_{R}\})$
41	37 40	mpbiri	$⊢ φ \to L ({Base}_{U} \times \{0_{R}\}) = {Base}_{U}$
42	36 41	eqtrd	$⊢ φ \to L (0_{R} \underset{˙}{\cdot} G) = {Base}_{U}$
43	22 42	sylan9eqr	$⊢ (φ \land X = 0_{R}) \to L (X \underset{˙}{\cdot} G) = {Base}_{U}$
44	43	fveq2d	$⊢ (φ \land X = 0_{R}) \to \underset{˙}{⊥} (L (X \underset{˙}{\cdot} G)) = \underset{˙}{⊥} ({Base}_{U})$
45	44	fveq2d	$⊢ (φ \land X = 0_{R}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (X \underset{˙}{\cdot} G))) = \underset{˙}{⊥} (\underset{˙}{⊥} ({Base}_{U}))$
46	21 45 43	3eqtr4d	$⊢ (φ \land X = 0_{R}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (X \underset{˙}{\cdot} G))) = L (X \underset{˙}{\cdot} G)$
47	16	simprd	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
48	47	adantr	$⊢ (φ \land X \neq 0_{R}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
49	1 3 11	dvhlvec	$⊢ φ \to U \in LVec$
50	49	adantr	$⊢ (φ \land X \neq 0_{R}) \to U \in LVec$
51	17	adantr	$⊢ (φ \land X \neq 0_{R}) \to G \in F$
52	12	adantr	$⊢ (φ \land X \neq 0_{R}) \to X \in B$
53		simpr	$⊢ (φ \land X \neq 0_{R}) \to X \neq 0_{R}$
54	7 8 31 4 5 6 9 50 51 52 53	ldualkrsc	$⊢ (φ \land X \neq 0_{R}) \to L (X \underset{˙}{\cdot} G) = L (G)$
55	54	fveq2d	$⊢ (φ \land X \neq 0_{R}) \to \underset{˙}{⊥} (L (X \underset{˙}{\cdot} G)) = \underset{˙}{⊥} (L (G))$
56	55	fveq2d	$⊢ (φ \land X \neq 0_{R}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (X \underset{˙}{\cdot} G))) = \underset{˙}{⊥} (\underset{˙}{⊥} (L (G)))$
57	48 56 54	3eqtr4d	$⊢ (φ \land X \neq 0_{R}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (X \underset{˙}{\cdot} G))) = L (X \underset{˙}{\cdot} G)$
58	46 57	pm2.61dane	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (X \underset{˙}{\cdot} G))) = L (X \underset{˙}{\cdot} G)$
59	10	lcfl1lem	$⊢ X \underset{˙}{\cdot} G \in C \leftrightarrow (X \underset{˙}{\cdot} G \in F \land \underset{˙}{⊥} (\underset{˙}{⊥} (L (X \underset{˙}{\cdot} G))) = L (X \underset{˙}{\cdot} G))$
60	18 58 59	sylanbrc	$⊢ φ \to X \underset{˙}{\cdot} G \in C$

Metamath Proof Explorer

Theorem lclkrlem1

Proof