This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )