obselocv

Description: A basis element is in the orthocomplement of a subset of the basis iff it is not in the subset. (Contributed by Mario Carneiro, 23-Oct-2015)

		Ref	Expression
	Hypothesis	obselocv.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	Assertion	obselocv	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to (A \in \underset{˙}{⊥} (C) \leftrightarrow \neg A \in C)$

Proof

Step	Hyp	Ref	Expression
1		obselocv.o	$⊢ \underset{˙}{⊥} = ocv (W)$
2		eqid	$⊢ 0_{W} = 0_{W}$
3	2	obsne0	$⊢ (B \in OBasis (W) \land A \in B) \to A \neq 0_{W}$
4	3	3adant2	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to A \neq 0_{W}$
5		elin	$⊢ A \in (C \cap \underset{˙}{⊥} (C)) \leftrightarrow (A \in C \land A \in \underset{˙}{⊥} (C))$
6		obsrcl	$⊢ B \in OBasis (W) \to W \in PreHil$
7	6	3ad2ant1	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to W \in PreHil$
8		phllmod	$⊢ W \in PreHil \to W \in LMod$
9	7 8	syl	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to W \in LMod$
10		simp2	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to C \subseteq B$
11		eqid	$⊢ {Base}_{W} = {Base}_{W}$
12	11	obsss	$⊢ B \in OBasis (W) \to B \subseteq {Base}_{W}$
13	12	3ad2ant1	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to B \subseteq {Base}_{W}$
14	10 13	sstrd	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to C \subseteq {Base}_{W}$
15		eqid	$⊢ LSpan (W) = LSpan (W)$
16	11 15	lspssid	$⊢ (W \in LMod \land C \subseteq {Base}_{W}) \to C \subseteq LSpan (W) (C)$
17	9 14 16	syl2anc	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to C \subseteq LSpan (W) (C)$
18	17	ssrind	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to C \cap \underset{˙}{⊥} (C) \subseteq LSpan (W) (C) \cap \underset{˙}{⊥} (C)$
19	11 1 15	ocvlsp	$⊢ (W \in PreHil \land C \subseteq {Base}_{W}) \to \underset{˙}{⊥} (LSpan (W) (C)) = \underset{˙}{⊥} (C)$
20	7 14 19	syl2anc	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to \underset{˙}{⊥} (LSpan (W) (C)) = \underset{˙}{⊥} (C)$
21	20	ineq2d	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to LSpan (W) (C) \cap \underset{˙}{⊥} (LSpan (W) (C)) = LSpan (W) (C) \cap \underset{˙}{⊥} (C)$
22		eqid	$⊢ LSubSp (W) = LSubSp (W)$
23	11 22 15	lspcl	$⊢ (W \in LMod \land C \subseteq {Base}_{W}) \to LSpan (W) (C) \in LSubSp (W)$
24	9 14 23	syl2anc	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to LSpan (W) (C) \in LSubSp (W)$
25	1 22 2	ocvin	$⊢ (W \in PreHil \land LSpan (W) (C) \in LSubSp (W)) \to LSpan (W) (C) \cap \underset{˙}{⊥} (LSpan (W) (C)) = \{0_{W}\}$
26	7 24 25	syl2anc	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to LSpan (W) (C) \cap \underset{˙}{⊥} (LSpan (W) (C)) = \{0_{W}\}$
27	21 26	eqtr3d	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to LSpan (W) (C) \cap \underset{˙}{⊥} (C) = \{0_{W}\}$
28	18 27	sseqtrd	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to C \cap \underset{˙}{⊥} (C) \subseteq \{0_{W}\}$
29	28	sseld	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to (A \in (C \cap \underset{˙}{⊥} (C)) \to A \in \{0_{W}\})$
30	5 29	biimtrrid	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to ((A \in C \land A \in \underset{˙}{⊥} (C)) \to A \in \{0_{W}\})$
31		elsni	$⊢ A \in \{0_{W}\} \to A = 0_{W}$
32	30 31	syl6	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to ((A \in C \land A \in \underset{˙}{⊥} (C)) \to A = 0_{W})$
33	32	necon3ad	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to (A \neq 0_{W} \to \neg (A \in C \land A \in \underset{˙}{⊥} (C)))$
34	4 33	mpd	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to \neg (A \in C \land A \in \underset{˙}{⊥} (C))$
35		imnan	$⊢ (A \in C \to \neg A \in \underset{˙}{⊥} (C)) \leftrightarrow \neg (A \in C \land A \in \underset{˙}{⊥} (C))$
36	34 35	sylibr	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to (A \in C \to \neg A \in \underset{˙}{⊥} (C))$
37	36	con2d	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to (A \in \underset{˙}{⊥} (C) \to \neg A \in C)$
38		simpr	$⊢ ((B \in OBasis (W) \land C \subseteq B \land A \in B) \land x \in C) \to x \in C$
39		eleq1	$⊢ A = x \to (A \in C \leftrightarrow x \in C)$
40	38 39	syl5ibrcom	$⊢ ((B \in OBasis (W) \land C \subseteq B \land A \in B) \land x \in C) \to (A = x \to A \in C)$
41	40	con3d	$⊢ ((B \in OBasis (W) \land C \subseteq B \land A \in B) \land x \in C) \to (\neg A \in C \to \neg A = x)$
42		simpl1	$⊢ ((B \in OBasis (W) \land C \subseteq B \land A \in B) \land x \in C) \to B \in OBasis (W)$
43		simpl3	$⊢ ((B \in OBasis (W) \land C \subseteq B \land A \in B) \land x \in C) \to A \in B$
44	10	sselda	$⊢ ((B \in OBasis (W) \land C \subseteq B \land A \in B) \land x \in C) \to x \in B$
45		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
46		eqid	$⊢ Scalar (W) = Scalar (W)$
47		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
48		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
49	11 45 46 47 48	obsip	$⊢ (B \in OBasis (W) \land A \in B \land x \in B) \to A \cdot_{𝑖} (W) x = if (A = x, 1_{Scalar (W)}, 0_{Scalar (W)})$
50	42 43 44 49	syl3anc	$⊢ ((B \in OBasis (W) \land C \subseteq B \land A \in B) \land x \in C) \to A \cdot_{𝑖} (W) x = if (A = x, 1_{Scalar (W)}, 0_{Scalar (W)})$
51		iffalse	$⊢ \neg A = x \to if (A = x, 1_{Scalar (W)}, 0_{Scalar (W)}) = 0_{Scalar (W)}$
52	51	eqeq2d	$⊢ \neg A = x \to (A \cdot_{𝑖} (W) x = if (A = x, 1_{Scalar (W)}, 0_{Scalar (W)}) \leftrightarrow A \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
53	50 52	syl5ibcom	$⊢ ((B \in OBasis (W) \land C \subseteq B \land A \in B) \land x \in C) \to (\neg A = x \to A \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
54	41 53	syld	$⊢ ((B \in OBasis (W) \land C \subseteq B \land A \in B) \land x \in C) \to (\neg A \in C \to A \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
55	54	ralrimdva	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to (\neg A \in C \to \forall x \in C A \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
56		simp3	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to A \in B$
57	13 56	sseldd	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to A \in {Base}_{W}$
58	11 45 46 48 1	elocv	$⊢ A \in \underset{˙}{⊥} (C) \leftrightarrow (C \subseteq {Base}_{W} \land A \in {Base}_{W} \land \forall x \in C A \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
59		df-3an	$⊢ (C \subseteq {Base}_{W} \land A \in {Base}_{W} \land \forall x \in C A \cdot_{𝑖} (W) x = 0_{Scalar (W)}) \leftrightarrow ((C \subseteq {Base}_{W} \land A \in {Base}_{W}) \land \forall x \in C A \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
60	58 59	bitri	$⊢ A \in \underset{˙}{⊥} (C) \leftrightarrow ((C \subseteq {Base}_{W} \land A \in {Base}_{W}) \land \forall x \in C A \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
61	60	baib	$⊢ (C \subseteq {Base}_{W} \land A \in {Base}_{W}) \to (A \in \underset{˙}{⊥} (C) \leftrightarrow \forall x \in C A \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
62	14 57 61	syl2anc	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to (A \in \underset{˙}{⊥} (C) \leftrightarrow \forall x \in C A \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
63	55 62	sylibrd	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to (\neg A \in C \to A \in \underset{˙}{⊥} (C))$
64	37 63	impbid	$⊢ (B \in OBasis (W) \land C \subseteq B \land A \in B) \to (A \in \underset{˙}{⊥} (C) \leftrightarrow \neg A \in C)$

Metamath Proof Explorer

Theorem obselocv

Proof