spansnm0i

Description: The meet of different one-dimensional subspaces is the zero subspace. (Contributed by NM, 1-Nov-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	spansnm0.1	$⊢ A \in ℋ$
	spansnm0.2	$⊢ B \in ℋ$
Assertion	spansnm0i	$⊢ \neg A \in span (\{B\}) \to span (\{A\}) \cap span (\{B\}) = 0_{ℋ}$

Step	Hyp	Ref	Expression
1		spansnm0.1	$⊢ A \in ℋ$
2		spansnm0.2	$⊢ B \in ℋ$
3	2	spansnchi	$⊢ span (\{B\}) \in C_{ℋ}$
4	3	chshii	$⊢ span (\{B\}) \in S_{ℋ}$
5		elspansn5	$⊢ span (\{B\}) \in S_{ℋ} \to (((A \in ℋ \land \neg A \in span (\{B\})) \land (x \in span (\{A\}) \land x \in span (\{B\}))) \to x = 0_{ℎ})$
6	4 5	ax-mp	$⊢ ((A \in ℋ \land \neg A \in span (\{B\})) \land (x \in span (\{A\}) \land x \in span (\{B\}))) \to x = 0_{ℎ}$
7	1 6	mpanl1	$⊢ (\neg A \in span (\{B\}) \land (x \in span (\{A\}) \land x \in span (\{B\}))) \to x = 0_{ℎ}$
8	7	ex	$⊢ \neg A \in span (\{B\}) \to ((x \in span (\{A\}) \land x \in span (\{B\})) \to x = 0_{ℎ})$
9		elin	$⊢ x \in (span (\{A\}) \cap span (\{B\})) \leftrightarrow (x \in span (\{A\}) \land x \in span (\{B\}))$
10		elch0	$⊢ x \in 0_{ℋ} \leftrightarrow x = 0_{ℎ}$
11	8 9 10	3imtr4g	$⊢ \neg A \in span (\{B\}) \to (x \in (span (\{A\}) \cap span (\{B\})) \to x \in 0_{ℋ})$
12	11	ssrdv	$⊢ \neg A \in span (\{B\}) \to span (\{A\}) \cap span (\{B\}) \subseteq 0_{ℋ}$
13	1	spansnchi	$⊢ span (\{A\}) \in C_{ℋ}$
14	13 3	chincli	$⊢ span (\{A\}) \cap span (\{B\}) \in C_{ℋ}$
15	14	chle0i	$⊢ span (\{A\}) \cap span (\{B\}) \subseteq 0_{ℋ} \leftrightarrow span (\{A\}) \cap span (\{B\}) = 0_{ℋ}$
16	12 15	sylib	$⊢ \neg A \in span (\{B\}) \to span (\{A\}) \cap span (\{B\}) = 0_{ℋ}$

Metamath Proof Explorer