dochocss

Description: Double negative law for orthocomplement of an arbitrary set of vectors. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	dochss.h	$⊢ H = LHyp (K)$
	dochss.u	$⊢ U = DVecH (K) (W)$
	dochss.v	$⊢ V = {Base}_{U}$
	dochss.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
Assertion	dochocss	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$

Proof

Step	Hyp	Ref	Expression
1		dochss.h	$⊢ H = LHyp (K)$
2		dochss.u	$⊢ U = DVecH (K) (W)$
3		dochss.v	$⊢ V = {Base}_{U}$
4		dochss.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
5		ssintub	$⊢ X \subseteq ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}$
6		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
7	1 6 2 3 4	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
8		eqid	$⊢ oc (K) = oc (K)$
9	8 1 6 4	dochvalr	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (X))))$
10	7 9	syldan	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (X))))$
11	8 1 6 2 3 4	dochval2	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) = DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})))$
12	11	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to {DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (X)) = {DIsoH (K) (W)}^{-1} (DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}))))$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14		eqid	$⊢ LSubSp (U) = LSubSp (U)$
15	13 1 6 2 14	dihf11	$⊢ (K \in HL \land W \in H) \to DIsoH (K) (W) : {Base}_{K} \underset{1-1}{⟶} LSubSp (U)$
16	15	adantr	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to DIsoH (K) (W) : {Base}_{K} \underset{1-1}{⟶} LSubSp (U)$
17		f1f1orn	$⊢ DIsoH (K) (W) : {Base}_{K} \underset{1-1}{⟶} LSubSp (U) \to DIsoH (K) (W) : {Base}_{K} \underset{1-1 onto}{⟶} ran DIsoH (K) (W)$
18	16 17	syl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to DIsoH (K) (W) : {Base}_{K} \underset{1-1 onto}{⟶} ran DIsoH (K) (W)$
19		hlop	$⊢ K \in HL \to K \in OP$
20	19	ad2antrr	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to K \in OP$
21		simpl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to (K \in HL \land W \in H)$
22		ssrab2	$⊢ \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \subseteq ran DIsoH (K) (W)$
23	22	a1i	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \subseteq ran DIsoH (K) (W)$
24		eqid	$⊢ 1. (K) = 1. (K)$
25	24 1 6 2 3	dih1	$⊢ (K \in HL \land W \in H) \to DIsoH (K) (W) (1. (K)) = V$
26	25	adantr	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to DIsoH (K) (W) (1. (K)) = V$
27		f1fn	$⊢ DIsoH (K) (W) : {Base}_{K} \underset{1-1}{⟶} LSubSp (U) \to DIsoH (K) (W) Fn {Base}_{K}$
28	16 27	syl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to DIsoH (K) (W) Fn {Base}_{K}$
29	13 24	op1cl	$⊢ K \in OP \to 1. (K) \in {Base}_{K}$
30	20 29	syl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to 1. (K) \in {Base}_{K}$
31		fnfvelrn	$⊢ (DIsoH (K) (W) Fn {Base}_{K} \land 1. (K) \in {Base}_{K}) \to DIsoH (K) (W) (1. (K)) \in ran DIsoH (K) (W)$
32	28 30 31	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to DIsoH (K) (W) (1. (K)) \in ran DIsoH (K) (W)$
33	26 32	eqeltrrd	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to V \in ran DIsoH (K) (W)$
34		simpr	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to X \subseteq V$
35		sseq2	$⊢ z = V \to (X \subseteq z \leftrightarrow X \subseteq V)$
36	35	elrab	$⊢ V \in \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \leftrightarrow (V \in ran DIsoH (K) (W) \land X \subseteq V)$
37	33 34 36	sylanbrc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to V \in \{z \in ran DIsoH (K) (W) \| X \subseteq z\}$
38	37	ne0d	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \neq \emptyset$
39	1 6	dihintcl	$⊢ ((K \in HL \land W \in H) \land (\{z \in ran DIsoH (K) (W) \| X \subseteq z\} \subseteq ran DIsoH (K) (W) \land \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \neq \emptyset)) \to ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \in ran DIsoH (K) (W)$
40	21 23 38 39	syl12anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \in ran DIsoH (K) (W)$
41		f1ocnvdm	$⊢ (DIsoH (K) (W) : {Base}_{K} \underset{1-1 onto}{⟶} ran DIsoH (K) (W) \land ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \in ran DIsoH (K) (W)) \to {DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}) \in {Base}_{K}$
42	18 40 41	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to {DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}) \in {Base}_{K}$
43	13 8	opoccl	$⊢ (K \in OP \land {DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}) \in {Base}_{K}) \to oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})) \in {Base}_{K}$
44	20 42 43	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})) \in {Base}_{K}$
45		f1ocnvfv1	$⊢ (DIsoH (K) (W) : {Base}_{K} \underset{1-1 onto}{⟶} ran DIsoH (K) (W) \land oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})) \in {Base}_{K}) \to {DIsoH (K) (W)}^{-1} (DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})))) = oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}))$
46	18 44 45	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to {DIsoH (K) (W)}^{-1} (DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})))) = oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}))$
47	12 46	eqtrd	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to {DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (X)) = oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}))$
48	47	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (X))) = oc (K) (oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})))$
49	13 8	opococ	$⊢ (K \in OP \land {DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}) \in {Base}_{K}) \to oc (K) (oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}))) = {DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})$
50	20 42 49	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to oc (K) (oc (K) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}))) = {DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})$
51	48 50	eqtrd	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (X))) = {DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})$
52	51	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (X)))) = DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}))$
53		f1ocnvfv2	$⊢ (DIsoH (K) (W) : {Base}_{K} \underset{1-1 onto}{⟶} ran DIsoH (K) (W) \land ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\} \in ran DIsoH (K) (W)) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})) = ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}$
54	18 40 53	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\})) = ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\}$
55	10 52 54	3eqtrrd	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to ⋂ \{z \in ran DIsoH (K) (W) \| X \subseteq z\} = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
56	5 55	sseqtrid	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$

Metamath Proof Explorer

Theorem dochocss

Proof