lcvp

Description: Covering property of Definition 7.4 of MaedaMaeda p. 31 and its converse. ( cvp analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lcvp.s	$⊢ S = LSubSp (W)$
	lcvp.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lcvp.o	$⊢ \underset{˙}{0} = 0_{W}$
	lcvp.a	$⊢ A = LSAtoms (W)$
	lcvp.c	$⊢ C = ⋖_{L} (W)$
	lcvp.w	$⊢ φ \to W \in LVec$
	lcvp.u	$⊢ φ \to U \in S$
	lcvp.q	$⊢ φ \to Q \in A$
Assertion	lcvp	$⊢ φ \to (U \cap Q = \{\underset{˙}{0}\} \leftrightarrow U C (U \underset{˙}{\oplus} Q))$

Step	Hyp	Ref	Expression
1		lcvp.s	$⊢ S = LSubSp (W)$
2		lcvp.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lcvp.o	$⊢ \underset{˙}{0} = 0_{W}$
4		lcvp.a	$⊢ A = LSAtoms (W)$
5		lcvp.c	$⊢ C = ⋖_{L} (W)$
6		lcvp.w	$⊢ φ \to W \in LVec$
7		lcvp.u	$⊢ φ \to U \in S$
8		lcvp.q	$⊢ φ \to Q \in A$
9		lveclmod	$⊢ W \in LVec \to W \in LMod$
10	6 9	syl	$⊢ φ \to W \in LMod$
11	1 4 10 8	lsatlssel	$⊢ φ \to Q \in S$
12	1	lssincl	$⊢ (W \in LMod \land U \in S \land Q \in S) \to U \cap Q \in S$
13	10 7 11 12	syl3anc	$⊢ φ \to U \cap Q \in S$
14	3 1 4 5 6 13 8	lsatcveq0	$⊢ φ \to ((U \cap Q) C Q \leftrightarrow U \cap Q = \{\underset{˙}{0}\})$
15	1 2 5 10 7 11	lcvexch	$⊢ φ \to ((U \cap Q) C Q \leftrightarrow U C (U \underset{˙}{\oplus} Q))$
16	14 15	bitr3d	$⊢ φ \to (U \cap Q = \{\underset{˙}{0}\} \leftrightarrow U C (U \underset{˙}{\oplus} Q))$

Metamath Proof Explorer