Theorem lsatcvat2

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

	Ref	Expression
Hypotheses	lsatcvat2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lsatcvat2.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	lsatcvat2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lsatcvat2.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
	lsatcvat2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lsatcvat2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lsatcvat2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
	lsatcvat2.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
	lsatcvat2.n	⊢ ( 𝜑 → 𝑄 ≠ 𝑅 )
	lsatcvat2.l	⊢ ( 𝜑 → 𝑈 𝐶 ( 𝑄 ⊕ 𝑅 ) )
Assertion	lsatcvat2	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		lsatcvat2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lsatcvat2.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
3		lsatcvat2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4		lsatcvat2.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
5		lsatcvat2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lsatcvat2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7		lsatcvat2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8		lsatcvat2.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
9		lsatcvat2.n	⊢ ( 𝜑 → 𝑄 ≠ 𝑅 )
10		lsatcvat2.l	⊢ ( 𝜑 → 𝑈 𝐶 ( 𝑄 ⊕ 𝑅 ) )
11		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
12	11 2 1 3 4 5 6 7 8 10	lsatcv1	⊢ ( 𝜑 → ( 𝑈 = { ( 0g ‘ 𝑊 ) } ↔ 𝑄 = 𝑅 ) )
13	12	necon3bid	⊢ ( 𝜑 → ( 𝑈 ≠ { ( 0g ‘ 𝑊 ) } ↔ 𝑄 ≠ 𝑅 ) )
14	9 13	mpbird	⊢ ( 𝜑 → 𝑈 ≠ { ( 0g ‘ 𝑊 ) } )
15		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
16	5 15	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
17	1 3 16 7	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
18	1 3 16 8	lsatlssel	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
19	1 2	lsmcl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑄 ∈ 𝑆 ∧ 𝑅 ∈ 𝑆 ) → ( 𝑄 ⊕ 𝑅 ) ∈ 𝑆 )
20	16 17 18 19	syl3anc	⊢ ( 𝜑 → ( 𝑄 ⊕ 𝑅 ) ∈ 𝑆 )
21	1 4 5 6 20 10	lcvpss	⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) )
22	11 1 2 3 5 6 7 8 14 21	lsatcvat	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )