lsatexch1

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

	Ref	Expression
Hypotheses	lsatexch1.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsatexch1.a	$⊢ A = LSAtoms (W)$
	lsatexch1.w	$⊢ φ \to W \in LVec$
	lsatexch1.u	$⊢ φ \to Q \in A$
	lsatexch1.q	$⊢ φ \to R \in A$
	lsatexch1.r	$⊢ φ \to S \in A$
	lsatexch1.l	$⊢ φ \to Q \subseteq S \underset{˙}{\oplus} R$
	lsatexch1.z	$⊢ φ \to Q \neq S$
Assertion	lsatexch1	$⊢ φ \to R \subseteq S \underset{˙}{\oplus} Q$

Step	Hyp	Ref	Expression
1		lsatexch1.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
2		lsatexch1.a	$⊢ A = LSAtoms (W)$
3		lsatexch1.w	$⊢ φ \to W \in LVec$
4		lsatexch1.u	$⊢ φ \to Q \in A$
5		lsatexch1.q	$⊢ φ \to R \in A$
6		lsatexch1.r	$⊢ φ \to S \in A$
7		lsatexch1.l	$⊢ φ \to Q \subseteq S \underset{˙}{\oplus} R$
8		lsatexch1.z	$⊢ φ \to Q \neq S$
9		eqid	$⊢ LSubSp (W) = LSubSp (W)$
10		eqid	$⊢ 0_{W} = 0_{W}$
11		lveclmod	$⊢ W \in LVec \to W \in LMod$
12	3 11	syl	$⊢ φ \to W \in LMod$
13	9 2 12 6	lsatlssel	$⊢ φ \to S \in LSubSp (W)$
14	8	necomd	$⊢ φ \to S \neq Q$
15	10 2 3 6 4	lsatnem0	$⊢ φ \to (S \neq Q \leftrightarrow S \cap Q = \{0_{W}\})$
16	14 15	mpbid	$⊢ φ \to S \cap Q = \{0_{W}\}$
17	9 1 10 2 3 13 4 5 7 16	lsatexch	$⊢ φ \to R \subseteq S \underset{˙}{\oplus} Q$

Metamath Proof Explorer