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

Metamath Proof Explorer

Theorem lsatexch1

Description: The atom exch1ange property. ( hlatexch1 analog.) (Contributed by NM, 14-Jan-2015)

Ref Expression
Hypotheses lsatexch1.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsatexch1.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatexch1.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsatexch1.u ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
lsatexch1.q ⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
lsatexch1.r ⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
lsatexch1.l ⊢ ( 𝜑 → 𝑄 ⊆ ( 𝑆 ⊕ 𝑅 ) )
lsatexch1.z ⊢ ( 𝜑 → 𝑄 ≠ 𝑆 )
Assertion lsatexch1 ( 𝜑 → 𝑅 ⊆ ( 𝑆 ⊕ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 lsatexch1.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
2 lsatexch1.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lsatexch1.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
4 lsatexch1.u ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
5 lsatexch1.q ⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
6 lsatexch1.r ⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
7 lsatexch1.l ⊢ ( 𝜑 → 𝑄 ⊆ ( 𝑆 ⊕ 𝑅 ) )
8 lsatexch1.z ⊢ ( 𝜑 → 𝑄 ≠ 𝑆 )
9 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
10 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
11 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
12 3 11 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
13 9 2 12 6 lsatlssel ⊢ ( 𝜑 → 𝑆 ∈ ( LSubSp ‘ 𝑊 ) )
14 8 necomd ⊢ ( 𝜑 → 𝑆 ≠ 𝑄 )
15 10 2 3 6 4 lsatnem0 ⊢ ( 𝜑 → ( 𝑆 ≠ 𝑄 ↔ ( 𝑆 ∩ 𝑄 ) = { ( 0g ‘ 𝑊 ) } ) )
16 14 15 mpbid ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑄 ) = { ( 0g ‘ 𝑊 ) } )
17 9 1 10 2 3 13 4 5 7 16 lsatexch ⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑆 ⊕ 𝑄 ) )