lspexchn1

Description: Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch to see if this will shorten proofs. (Contributed by NM, 20-May-2015)

	Ref	Expression
Hypotheses	lspexchn1.v	$⊢ V = {Base}_{W}$
	lspexchn1.n	$⊢ N = LSpan (W)$
	lspexchn1.w	$⊢ φ \to W \in LVec$
	lspexchn1.x	$⊢ φ \to X \in V$
	lspexchn1.y	$⊢ φ \to Y \in V$
	lspexchn1.z	$⊢ φ \to Z \in V$
	lspexchn1.q	$⊢ φ \to \neg Y \in N (\{Z\})$
	lspexchn1.e	$⊢ φ \to \neg X \in N (\{Y, Z\})$
Assertion	lspexchn1	$⊢ φ \to \neg Y \in N (\{X, Z\})$

Proof

Step	Hyp	Ref	Expression
1		lspexchn1.v	$⊢ V = {Base}_{W}$
2		lspexchn1.n	$⊢ N = LSpan (W)$
3		lspexchn1.w	$⊢ φ \to W \in LVec$
4		lspexchn1.x	$⊢ φ \to X \in V$
5		lspexchn1.y	$⊢ φ \to Y \in V$
6		lspexchn1.z	$⊢ φ \to Z \in V$
7		lspexchn1.q	$⊢ φ \to \neg Y \in N (\{Z\})$
8		lspexchn1.e	$⊢ φ \to \neg X \in N (\{Y, Z\})$
9		eqid	$⊢ 0_{W} = 0_{W}$
10	3	adantr	$⊢ (φ \land Y \in N (\{X, Z\})) \to W \in LVec$
11		eqid	$⊢ LSubSp (W) = LSubSp (W)$
12		lveclmod	$⊢ W \in LVec \to W \in LMod$
13	3 12	syl	$⊢ φ \to W \in LMod$
14	1 11 2	lspsncl	$⊢ (W \in LMod \land Z \in V) \to N (\{Z\}) \in LSubSp (W)$
15	13 6 14	syl2anc	$⊢ φ \to N (\{Z\}) \in LSubSp (W)$
16	9 11 13 15 5 7	lssneln0	$⊢ φ \to Y \in (V ∖ \{0_{W}\})$
17	16	adantr	$⊢ (φ \land Y \in N (\{X, Z\})) \to Y \in (V ∖ \{0_{W}\})$
18	4	adantr	$⊢ (φ \land Y \in N (\{X, Z\})) \to X \in V$
19	6	adantr	$⊢ (φ \land Y \in N (\{X, Z\})) \to Z \in V$
20	1 2 13 5 6 7	lspsnne2	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
21	20	adantr	$⊢ (φ \land Y \in N (\{X, Z\})) \to N (\{Y\}) \neq N (\{Z\})$
22		simpr	$⊢ (φ \land Y \in N (\{X, Z\})) \to Y \in N (\{X, Z\})$
23	1 9 2 10 17 18 19 21 22	lspexch	$⊢ (φ \land Y \in N (\{X, Z\})) \to X \in N (\{Y, Z\})$
24	8 23	mtand	$⊢ φ \to \neg Y \in N (\{X, Z\})$

Metamath Proof Explorer

Theorem lspexchn1

Proof