lsatcvat2

Description: A subspace covered by the sum of two distinct atoms is an atom. ( atcvat2i analog.) (Contributed by NM, 10-Jan-2015)

Step	Hyp	Ref	Expression
1		lsatcvat2.s	$⊢ S = LSubSp (W)$
2		lsatcvat2.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lsatcvat2.a	$⊢ A = LSAtoms (W)$
4		lsatcvat2.c	$⊢ C = ⋖_{L} (W)$
5		lsatcvat2.w	$⊢ φ \to W \in LVec$
6		lsatcvat2.u	$⊢ φ \to U \in S$
7		lsatcvat2.q	$⊢ φ \to Q \in A$
8		lsatcvat2.r	$⊢ φ \to R \in A$
9		lsatcvat2.n	$⊢ φ \to Q \neq R$
10		lsatcvat2.l	$⊢ φ \to U C (Q \underset{˙}{\oplus} R)$
11		eqid	$⊢ 0_{W} = 0_{W}$
12	11 2 1 3 4 5 6 7 8 10	lsatcv1	$⊢ φ \to (U = \{0_{W}\} \leftrightarrow Q = R)$
13	12	necon3bid	$⊢ φ \to (U \neq \{0_{W}\} \leftrightarrow Q \neq R)$
14	9 13	mpbird	$⊢ φ \to U \neq \{0_{W}\}$
15		lveclmod	$⊢ W \in LVec \to W \in LMod$
16	5 15	syl	$⊢ φ \to W \in LMod$
17	1 3 16 7	lsatlssel	$⊢ φ \to Q \in S$
18	1 3 16 8	lsatlssel	$⊢ φ \to R \in S$
19	1 2	lsmcl	$⊢ (W \in LMod \land Q \in S \land R \in S) \to Q \underset{˙}{\oplus} R \in S$
20	16 17 18 19	syl3anc	$⊢ φ \to Q \underset{˙}{\oplus} R \in S$
21	1 4 5 6 20 10	lcvpss	$⊢ φ \to U \subset Q \underset{˙}{\oplus} R$
22	11 1 2 3 5 6 7 8 14 21	lsatcvat	$⊢ φ \to U \in A$

Metamath Proof Explorer