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	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑆 ⊕ 𝑄 ) )