lclkrslem2

Description: The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. (Contributed by NM, 28-Jan-2015)

	Ref	Expression
Hypotheses	lclkrslem1.h	$⊢ H = LHyp (K)$
	lclkrslem1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lclkrslem1.u	$⊢ U = DVecH (K) (W)$
	lclkrslem1.s	$⊢ S = LSubSp (U)$
	lclkrslem1.f	$⊢ F = LFnl (U)$
	lclkrslem1.l	$⊢ L = LKer (U)$
	lclkrslem1.d	$⊢ D = LDual (U)$
	lclkrslem1.r	$⊢ R = Scalar (U)$
	lclkrslem1.b	$⊢ B = {Base}_{R}$
	lclkrslem1.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	lclkrslem1.c	$⊢ C = \{f \in F \| (\underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f) \land \underset{˙}{⊥} (L (f)) \subseteq Q)\}$
	lclkrslem1.k	$⊢ φ \to (K \in HL \land W \in H)$
	lclkrslem1.q	$⊢ φ \to Q \in S$
	lclkrslem1.g	$⊢ φ \to G \in C$
	lclkrslem2.p	$⊢ \underset{˙}{+} = +_{D}$
	lclkrslem2.e	$⊢ φ \to E \in C$
Assertion	lclkrslem2	$⊢ φ \to E \underset{˙}{+} G \in C$

Proof

Step	Hyp	Ref	Expression
1		lclkrslem1.h	$⊢ H = LHyp (K)$
2		lclkrslem1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lclkrslem1.u	$⊢ U = DVecH (K) (W)$
4		lclkrslem1.s	$⊢ S = LSubSp (U)$
5		lclkrslem1.f	$⊢ F = LFnl (U)$
6		lclkrslem1.l	$⊢ L = LKer (U)$
7		lclkrslem1.d	$⊢ D = LDual (U)$
8		lclkrslem1.r	$⊢ R = Scalar (U)$
9		lclkrslem1.b	$⊢ B = {Base}_{R}$
10		lclkrslem1.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
11		lclkrslem1.c	$⊢ C = \{f \in F \| (\underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f) \land \underset{˙}{⊥} (L (f)) \subseteq Q)\}$
12		lclkrslem1.k	$⊢ φ \to (K \in HL \land W \in H)$
13		lclkrslem1.q	$⊢ φ \to Q \in S$
14		lclkrslem1.g	$⊢ φ \to G \in C$
15		lclkrslem2.p	$⊢ \underset{˙}{+} = +_{D}$
16		lclkrslem2.e	$⊢ φ \to E \in C$
17		eqid	$⊢ \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} = \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
18	11 17	lcfls1c	$⊢ E \in C \leftrightarrow (E \in \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} \land \underset{˙}{⊥} (L (E)) \subseteq Q)$
19	18	simplbi	$⊢ E \in C \to E \in \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
20	16 19	syl	$⊢ φ \to E \in \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
21	11 17	lcfls1c	$⊢ G \in C \leftrightarrow (G \in \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} \land \underset{˙}{⊥} (L (G)) \subseteq Q)$
22	21	simplbi	$⊢ G \in C \to G \in \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
23	14 22	syl	$⊢ φ \to G \in \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
24	1 2 3 5 6 7 15 17 12 20 23	lclkrlem2	$⊢ φ \to E \underset{˙}{+} G \in \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\}$
25		eqid	$⊢ {Base}_{U} = {Base}_{U}$
26	1 3 12	dvhlmod	$⊢ φ \to U \in LMod$
27	11	lcfls1lem	$⊢ E \in C \leftrightarrow (E \in F \land \underset{˙}{⊥} (\underset{˙}{⊥} (L (E))) = L (E) \land \underset{˙}{⊥} (L (E)) \subseteq Q)$
28	16 27	sylib	$⊢ φ \to (E \in F \land \underset{˙}{⊥} (\underset{˙}{⊥} (L (E))) = L (E) \land \underset{˙}{⊥} (L (E)) \subseteq Q)$
29	28	simp1d	$⊢ φ \to E \in F$
30	11	lcfls1lem	$⊢ G \in C \leftrightarrow (G \in F \land \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G) \land \underset{˙}{⊥} (L (G)) \subseteq Q)$
31	14 30	sylib	$⊢ φ \to (G \in F \land \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G) \land \underset{˙}{⊥} (L (G)) \subseteq Q)$
32	31	simp1d	$⊢ φ \to G \in F$
33	5 7 15 26 29 32	ldualvaddcl	$⊢ φ \to E \underset{˙}{+} G \in F$
34	25 5 6 26 33	lkrssv	$⊢ φ \to L (E \underset{˙}{+} G) \subseteq {Base}_{U}$
35	5 6 7 15 26 29 32	lkrin	$⊢ φ \to L (E) \cap L (G) \subseteq L (E \underset{˙}{+} G)$
36	1 3 25 2	dochss	$⊢ ((K \in HL \land W \in H) \land L (E \underset{˙}{+} G) \subseteq {Base}_{U} \land L (E) \cap L (G) \subseteq L (E \underset{˙}{+} G)) \to \underset{˙}{⊥} (L (E \underset{˙}{+} G)) \subseteq \underset{˙}{⊥} (L (E) \cap L (G))$
37	12 34 35 36	syl3anc	$⊢ φ \to \underset{˙}{⊥} (L (E \underset{˙}{+} G)) \subseteq \underset{˙}{⊥} (L (E) \cap L (G))$
38		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
39		eqid	$⊢ joinH (K) (W) = joinH (K) (W)$
40	28	simp2d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (E))) = L (E)$
41	1 38 2 3 5 6 12 29	lcfl5a	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (L (E))) = L (E) \leftrightarrow L (E) \in ran DIsoH (K) (W))$
42	40 41	mpbid	$⊢ φ \to L (E) \in ran DIsoH (K) (W)$
43	31	simp2d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G)$
44	1 38 2 3 5 6 12 32	lcfl5a	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (L (G))) = L (G) \leftrightarrow L (G) \in ran DIsoH (K) (W))$
45	43 44	mpbid	$⊢ φ \to L (G) \in ran DIsoH (K) (W)$
46	1 38 3 25 2 39 12 42 45	dochdmm1	$⊢ φ \to \underset{˙}{⊥} (L (E) \cap L (G)) = \underset{˙}{⊥} (L (E)) joinH (K) (W) \underset{˙}{⊥} (L (G))$
47		eqid	$⊢ LSSum (U) = LSSum (U)$
48	25 5 6 26 29	lkrssv	$⊢ φ \to L (E) \subseteq {Base}_{U}$
49	1 38 3 25 2	dochcl	$⊢ ((K \in HL \land W \in H) \land L (E) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (L (E)) \in ran DIsoH (K) (W)$
50	12 48 49	syl2anc	$⊢ φ \to \underset{˙}{⊥} (L (E)) \in ran DIsoH (K) (W)$
51	1 38 2 3 47 5 6 12 50 32	dochkrsm	$⊢ φ \to \underset{˙}{⊥} (L (E)) LSSum (U) \underset{˙}{⊥} (L (G)) \in ran DIsoH (K) (W)$
52	1 3 25 4 2	dochlss	$⊢ ((K \in HL \land W \in H) \land L (E) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (L (E)) \in S$
53	12 48 52	syl2anc	$⊢ φ \to \underset{˙}{⊥} (L (E)) \in S$
54	25 5 6 26 32	lkrssv	$⊢ φ \to L (G) \subseteq {Base}_{U}$
55	1 3 25 4 2	dochlss	$⊢ ((K \in HL \land W \in H) \land L (G) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (L (G)) \in S$
56	12 54 55	syl2anc	$⊢ φ \to \underset{˙}{⊥} (L (G)) \in S$
57	1 3 25 4 47 38 39 12 53 56	djhlsmcl	$⊢ φ \to (\underset{˙}{⊥} (L (E)) LSSum (U) \underset{˙}{⊥} (L (G)) \in ran DIsoH (K) (W) \leftrightarrow \underset{˙}{⊥} (L (E)) LSSum (U) \underset{˙}{⊥} (L (G)) = \underset{˙}{⊥} (L (E)) joinH (K) (W) \underset{˙}{⊥} (L (G)))$
58	51 57	mpbid	$⊢ φ \to \underset{˙}{⊥} (L (E)) LSSum (U) \underset{˙}{⊥} (L (G)) = \underset{˙}{⊥} (L (E)) joinH (K) (W) \underset{˙}{⊥} (L (G))$
59	46 58	eqtr4d	$⊢ φ \to \underset{˙}{⊥} (L (E) \cap L (G)) = \underset{˙}{⊥} (L (E)) LSSum (U) \underset{˙}{⊥} (L (G))$
60	28	simp3d	$⊢ φ \to \underset{˙}{⊥} (L (E)) \subseteq Q$
61	31	simp3d	$⊢ φ \to \underset{˙}{⊥} (L (G)) \subseteq Q$
62	4	lsssssubg	$⊢ U \in LMod \to S \subseteq SubGrp (U)$
63	26 62	syl	$⊢ φ \to S \subseteq SubGrp (U)$
64	63 53	sseldd	$⊢ φ \to \underset{˙}{⊥} (L (E)) \in SubGrp (U)$
65	63 56	sseldd	$⊢ φ \to \underset{˙}{⊥} (L (G)) \in SubGrp (U)$
66	63 13	sseldd	$⊢ φ \to Q \in SubGrp (U)$
67	47	lsmlub	$⊢ (\underset{˙}{⊥} (L (E)) \in SubGrp (U) \land \underset{˙}{⊥} (L (G)) \in SubGrp (U) \land Q \in SubGrp (U)) \to ((\underset{˙}{⊥} (L (E)) \subseteq Q \land \underset{˙}{⊥} (L (G)) \subseteq Q) \leftrightarrow \underset{˙}{⊥} (L (E)) LSSum (U) \underset{˙}{⊥} (L (G)) \subseteq Q)$
68	64 65 66 67	syl3anc	$⊢ φ \to ((\underset{˙}{⊥} (L (E)) \subseteq Q \land \underset{˙}{⊥} (L (G)) \subseteq Q) \leftrightarrow \underset{˙}{⊥} (L (E)) LSSum (U) \underset{˙}{⊥} (L (G)) \subseteq Q)$
69	60 61 68	mpbi2and	$⊢ φ \to \underset{˙}{⊥} (L (E)) LSSum (U) \underset{˙}{⊥} (L (G)) \subseteq Q$
70	59 69	eqsstrd	$⊢ φ \to \underset{˙}{⊥} (L (E) \cap L (G)) \subseteq Q$
71	37 70	sstrd	$⊢ φ \to \underset{˙}{⊥} (L (E \underset{˙}{+} G)) \subseteq Q$
72	11 17	lcfls1c	$⊢ E \underset{˙}{+} G \in C \leftrightarrow (E \underset{˙}{+} G \in \{f \in F \| \underset{˙}{⊥} (\underset{˙}{⊥} (L (f))) = L (f)\} \land \underset{˙}{⊥} (L (E \underset{˙}{+} G)) \subseteq Q)$
73	24 71 72	sylanbrc	$⊢ φ \to E \underset{˙}{+} G \in C$

Metamath Proof Explorer

Theorem lclkrslem2

Proof