lcfrlem5

Description: Lemma for lcfr . The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. TODO: share hypotheses with others. Use more consistent variable names here or elsewhere when possible. (Contributed by NM, 5-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem5.h	$⊢ H = LHyp (K)$
	lcfrlem5.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfrlem5.u	$⊢ U = DVecH (K) (W)$
	lcfrlem5.v	$⊢ V = {Base}_{U}$
	lcfrlem5.f	$⊢ F = LFnl (U)$
	lcfrlem5.l	$⊢ L = LKer (U)$
	lcfrlem5.d	$⊢ D = LDual (U)$
	lcfrlem5.s	$⊢ S = LSubSp (D)$
	lcfrlem5.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrlem5.r	$⊢ φ \to R \in S$
	lcfrlem5.q	$⊢ Q = ⋃_{f \in R} \underset{˙}{⊥} (L (f))$
	lcfrlem5.x	$⊢ φ \to X \in Q$
	lcfrlem5.c	$⊢ C = Scalar (U)$
	lcfrlem5.b	$⊢ B = {Base}_{C}$
	lcfrlem5.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	lcfrlem5.a	$⊢ φ \to A \in B$
Assertion	lcfrlem5	$⊢ φ \to A \underset{˙}{\cdot} X \in Q$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem5.h	$⊢ H = LHyp (K)$
2		lcfrlem5.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfrlem5.u	$⊢ U = DVecH (K) (W)$
4		lcfrlem5.v	$⊢ V = {Base}_{U}$
5		lcfrlem5.f	$⊢ F = LFnl (U)$
6		lcfrlem5.l	$⊢ L = LKer (U)$
7		lcfrlem5.d	$⊢ D = LDual (U)$
8		lcfrlem5.s	$⊢ S = LSubSp (D)$
9		lcfrlem5.k	$⊢ φ \to (K \in HL \land W \in H)$
10		lcfrlem5.r	$⊢ φ \to R \in S$
11		lcfrlem5.q	$⊢ Q = ⋃_{f \in R} \underset{˙}{⊥} (L (f))$
12		lcfrlem5.x	$⊢ φ \to X \in Q$
13		lcfrlem5.c	$⊢ C = Scalar (U)$
14		lcfrlem5.b	$⊢ B = {Base}_{C}$
15		lcfrlem5.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
16		lcfrlem5.a	$⊢ φ \to A \in B$
17	12 11	eleqtrdi	$⊢ φ \to X \in ⋃_{f \in R} \underset{˙}{⊥} (L (f))$
18		eliun	$⊢ X \in ⋃_{f \in R} \underset{˙}{⊥} (L (f)) \leftrightarrow \exists f \in R X \in \underset{˙}{⊥} (L (f))$
19	17 18	sylib	$⊢ φ \to \exists f \in R X \in \underset{˙}{⊥} (L (f))$
20	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
21	20	ad2antrr	$⊢ ((φ \land f \in R) \land X \in \underset{˙}{⊥} (L (f))) \to U \in LMod$
22	9	ad2antrr	$⊢ ((φ \land f \in R) \land X \in \underset{˙}{⊥} (L (f))) \to (K \in HL \land W \in H)$
23		eqid	$⊢ {Base}_{D} = {Base}_{D}$
24	23 8	lssss	$⊢ R \in S \to R \subseteq {Base}_{D}$
25	10 24	syl	$⊢ φ \to R \subseteq {Base}_{D}$
26	5 7 23 20	ldualvbase	$⊢ φ \to {Base}_{D} = F$
27	25 26	sseqtrd	$⊢ φ \to R \subseteq F$
28	27	sselda	$⊢ (φ \land f \in R) \to f \in F$
29	28	adantr	$⊢ ((φ \land f \in R) \land X \in \underset{˙}{⊥} (L (f))) \to f \in F$
30	4 5 6 21 29	lkrssv	$⊢ ((φ \land f \in R) \land X \in \underset{˙}{⊥} (L (f))) \to L (f) \subseteq V$
31		eqid	$⊢ LSubSp (U) = LSubSp (U)$
32	1 3 4 31 2	dochlss	$⊢ ((K \in HL \land W \in H) \land L (f) \subseteq V) \to \underset{˙}{⊥} (L (f)) \in LSubSp (U)$
33	22 30 32	syl2anc	$⊢ ((φ \land f \in R) \land X \in \underset{˙}{⊥} (L (f))) \to \underset{˙}{⊥} (L (f)) \in LSubSp (U)$
34	16	ad2antrr	$⊢ ((φ \land f \in R) \land X \in \underset{˙}{⊥} (L (f))) \to A \in B$
35		simpr	$⊢ ((φ \land f \in R) \land X \in \underset{˙}{⊥} (L (f))) \to X \in \underset{˙}{⊥} (L (f))$
36	13 15 14 31	lssvscl	$⊢ ((U \in LMod \land \underset{˙}{⊥} (L (f)) \in LSubSp (U)) \land (A \in B \land X \in \underset{˙}{⊥} (L (f)))) \to A \underset{˙}{\cdot} X \in \underset{˙}{⊥} (L (f))$
37	21 33 34 35 36	syl22anc	$⊢ ((φ \land f \in R) \land X \in \underset{˙}{⊥} (L (f))) \to A \underset{˙}{\cdot} X \in \underset{˙}{⊥} (L (f))$
38	37	ex	$⊢ (φ \land f \in R) \to (X \in \underset{˙}{⊥} (L (f)) \to A \underset{˙}{\cdot} X \in \underset{˙}{⊥} (L (f)))$
39	38	reximdva	$⊢ φ \to (\exists f \in R X \in \underset{˙}{⊥} (L (f)) \to \exists f \in R A \underset{˙}{\cdot} X \in \underset{˙}{⊥} (L (f)))$
40	19 39	mpd	$⊢ φ \to \exists f \in R A \underset{˙}{\cdot} X \in \underset{˙}{⊥} (L (f))$
41		eliun	$⊢ A \underset{˙}{\cdot} X \in ⋃_{f \in R} \underset{˙}{⊥} (L (f)) \leftrightarrow \exists f \in R A \underset{˙}{\cdot} X \in \underset{˙}{⊥} (L (f))$
42	40 41	sylibr	$⊢ φ \to A \underset{˙}{\cdot} X \in ⋃_{f \in R} \underset{˙}{⊥} (L (f))$
43	42 11	eleqtrrdi	$⊢ φ \to A \underset{˙}{\cdot} X \in Q$

Metamath Proof Explorer

Theorem lcfrlem5

Proof