ocvin

Description: An orthocomplement has trivial intersection with the original subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	ocv2ss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	ocvin.l	$⊢ L = LSubSp (W)$
	ocvin.z	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	ocvin	$⊢ (W \in PreHil \land S \in L) \to S \cap \underset{˙}{⊥} (S) = \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		ocv2ss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
2		ocvin.l	$⊢ L = LSubSp (W)$
3		ocvin.z	$⊢ \underset{˙}{0} = 0_{W}$
4		eqid	$⊢ {Base}_{W} = {Base}_{W}$
5		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
6		eqid	$⊢ Scalar (W) = Scalar (W)$
7		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
8	4 5 6 7 1	ocvi	$⊢ (x \in \underset{˙}{⊥} (S) \land x \in S) \to x \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
9	8	ancoms	$⊢ (x \in S \land x \in \underset{˙}{⊥} (S)) \to x \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
10	9	adantl	$⊢ ((W \in PreHil \land S \in L) \land (x \in S \land x \in \underset{˙}{⊥} (S))) \to x \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
11		simpll	$⊢ ((W \in PreHil \land S \in L) \land (x \in S \land x \in \underset{˙}{⊥} (S))) \to W \in PreHil$
12	4 2	lssel	$⊢ (S \in L \land x \in S) \to x \in {Base}_{W}$
13	12	ad2ant2lr	$⊢ ((W \in PreHil \land S \in L) \land (x \in S \land x \in \underset{˙}{⊥} (S))) \to x \in {Base}_{W}$
14	6 5 4 7 3	ipeq0	$⊢ (W \in PreHil \land x \in {Base}_{W}) \to (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \leftrightarrow x = \underset{˙}{0})$
15	11 13 14	syl2anc	$⊢ ((W \in PreHil \land S \in L) \land (x \in S \land x \in \underset{˙}{⊥} (S))) \to (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \leftrightarrow x = \underset{˙}{0})$
16	10 15	mpbid	$⊢ ((W \in PreHil \land S \in L) \land (x \in S \land x \in \underset{˙}{⊥} (S))) \to x = \underset{˙}{0}$
17	16	ex	$⊢ (W \in PreHil \land S \in L) \to ((x \in S \land x \in \underset{˙}{⊥} (S)) \to x = \underset{˙}{0})$
18		elin	$⊢ x \in (S \cap \underset{˙}{⊥} (S)) \leftrightarrow (x \in S \land x \in \underset{˙}{⊥} (S))$
19		velsn	$⊢ x \in \{\underset{˙}{0}\} \leftrightarrow x = \underset{˙}{0}$
20	17 18 19	3imtr4g	$⊢ (W \in PreHil \land S \in L) \to (x \in (S \cap \underset{˙}{⊥} (S)) \to x \in \{\underset{˙}{0}\})$
21	20	ssrdv	$⊢ (W \in PreHil \land S \in L) \to S \cap \underset{˙}{⊥} (S) \subseteq \{\underset{˙}{0}\}$
22		phllmod	$⊢ W \in PreHil \to W \in LMod$
23	4 2	lssss	$⊢ S \in L \to S \subseteq {Base}_{W}$
24	4 1 2	ocvlss	$⊢ (W \in PreHil \land S \subseteq {Base}_{W}) \to \underset{˙}{⊥} (S) \in L$
25	23 24	sylan2	$⊢ (W \in PreHil \land S \in L) \to \underset{˙}{⊥} (S) \in L$
26	2	lssincl	$⊢ (W \in LMod \land S \in L \land \underset{˙}{⊥} (S) \in L) \to S \cap \underset{˙}{⊥} (S) \in L$
27	22 26	syl3an1	$⊢ (W \in PreHil \land S \in L \land \underset{˙}{⊥} (S) \in L) \to S \cap \underset{˙}{⊥} (S) \in L$
28	25 27	mpd3an3	$⊢ (W \in PreHil \land S \in L) \to S \cap \underset{˙}{⊥} (S) \in L$
29	3 2	lss0ss	$⊢ (W \in LMod \land S \cap \underset{˙}{⊥} (S) \in L) \to \{\underset{˙}{0}\} \subseteq S \cap \underset{˙}{⊥} (S)$
30	22 28 29	syl2an2r	$⊢ (W \in PreHil \land S \in L) \to \{\underset{˙}{0}\} \subseteq S \cap \underset{˙}{⊥} (S)$
31	21 30	eqssd	$⊢ (W \in PreHil \land S \in L) \to S \cap \underset{˙}{⊥} (S) = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem ocvin

Proof