hdmapoc

Description: Express our constructed orthocomplement (polarity) in terms of the Hilbert space definition of orthocomplement. Lines 24 and 25 in Holland95 p. 14. (Contributed by NM, 17-Jun-2015)

	Ref	Expression
Hypotheses	hdmapoc.h	$⊢ H = LHyp (K)$
	hdmapoc.u	$⊢ U = DVecH (K) (W)$
	hdmapoc.v	$⊢ V = {Base}_{U}$
	hdmapoc.r	$⊢ R = Scalar (U)$
	hdmapoc.z	$⊢ \underset{˙}{0} = 0_{R}$
	hdmapoc.o	$⊢ O = ocH (K) (W)$
	hdmapoc.s	$⊢ S = HDMap (K) (W)$
	hdmapoc.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmapoc.x	$⊢ φ \to X \subseteq V$
Assertion	hdmapoc	$⊢ φ \to O (X) = \{y \in V \| \forall z \in X S (z) (y) = \underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		hdmapoc.h	$⊢ H = LHyp (K)$
2		hdmapoc.u	$⊢ U = DVecH (K) (W)$
3		hdmapoc.v	$⊢ V = {Base}_{U}$
4		hdmapoc.r	$⊢ R = Scalar (U)$
5		hdmapoc.z	$⊢ \underset{˙}{0} = 0_{R}$
6		hdmapoc.o	$⊢ O = ocH (K) (W)$
7		hdmapoc.s	$⊢ S = HDMap (K) (W)$
8		hdmapoc.k	$⊢ φ \to (K \in HL \land W \in H)$
9		hdmapoc.x	$⊢ φ \to X \subseteq V$
10	1 2 3 6	dochssv	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to O (X) \subseteq V$
11	8 9 10	syl2anc	$⊢ φ \to O (X) \subseteq V$
12	11	sseld	$⊢ φ \to (y \in O (X) \to y \in V)$
13	12	pm4.71rd	$⊢ φ \to (y \in O (X) \leftrightarrow (y \in V \land y \in O (X)))$
14		eqid	$⊢ LSubSp (U) = LSubSp (U)$
15		eqid	$⊢ LSpan (U) = LSpan (U)$
16	1 2 8	dvhlmod	$⊢ φ \to U \in LMod$
17	16	adantr	$⊢ (φ \land y \in V) \to U \in LMod$
18	1 2 3 14 6	dochlss	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to O (X) \in LSubSp (U)$
19	8 9 18	syl2anc	$⊢ φ \to O (X) \in LSubSp (U)$
20	19	adantr	$⊢ (φ \land y \in V) \to O (X) \in LSubSp (U)$
21		simpr	$⊢ (φ \land y \in V) \to y \in V$
22	3 14 15 17 20 21	ellspsn5b	$⊢ (φ \land y \in V) \to (y \in O (X) \leftrightarrow LSpan (U) (\{y\}) \subseteq O (X))$
23		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
24	8	adantr	$⊢ (φ \land y \in V) \to (K \in HL \land W \in H)$
25	1 2 3 15 23	dihlsprn	$⊢ ((K \in HL \land W \in H) \land y \in V) \to LSpan (U) (\{y\}) \in ran DIsoH (K) (W)$
26	24 21 25	syl2anc	$⊢ (φ \land y \in V) \to LSpan (U) (\{y\}) \in ran DIsoH (K) (W)$
27	1 23 2 3 6	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to O (X) \in ran DIsoH (K) (W)$
28	8 9 27	syl2anc	$⊢ φ \to O (X) \in ran DIsoH (K) (W)$
29	28	adantr	$⊢ (φ \land y \in V) \to O (X) \in ran DIsoH (K) (W)$
30	1 23 6 24 26 29	dochord	$⊢ (φ \land y \in V) \to (LSpan (U) (\{y\}) \subseteq O (X) \leftrightarrow O (O (X)) \subseteq O (LSpan (U) (\{y\})))$
31	21	snssd	$⊢ (φ \land y \in V) \to \{y\} \subseteq V$
32	1 2 6 3 15 24 31	dochocsp	$⊢ (φ \land y \in V) \to O (LSpan (U) (\{y\})) = O (\{y\})$
33	32	sseq2d	$⊢ (φ \land y \in V) \to (O (O (X)) \subseteq O (LSpan (U) (\{y\})) \leftrightarrow O (O (X)) \subseteq O (\{y\}))$
34	9	adantr	$⊢ (φ \land y \in V) \to X \subseteq V$
35	1 23 2 3 6	dochcl	$⊢ ((K \in HL \land W \in H) \land \{y\} \subseteq V) \to O (\{y\}) \in ran DIsoH (K) (W)$
36	24 31 35	syl2anc	$⊢ (φ \land y \in V) \to O (\{y\}) \in ran DIsoH (K) (W)$
37	1 2 3 23 6 24 34 36	dochsscl	$⊢ (φ \land y \in V) \to (X \subseteq O (\{y\}) \leftrightarrow O (O (X)) \subseteq O (\{y\}))$
38	33 37	bitr4d	$⊢ (φ \land y \in V) \to (O (O (X)) \subseteq O (LSpan (U) (\{y\})) \leftrightarrow X \subseteq O (\{y\}))$
39	22 30 38	3bitrd	$⊢ (φ \land y \in V) \to (y \in O (X) \leftrightarrow X \subseteq O (\{y\}))$
40		dfss3	$⊢ X \subseteq O (\{y\}) \leftrightarrow \forall z \in X z \in O (\{y\})$
41	39 40	bitrdi	$⊢ (φ \land y \in V) \to (y \in O (X) \leftrightarrow \forall z \in X z \in O (\{y\}))$
42	8	ad2antrr	$⊢ ((φ \land y \in V) \land z \in X) \to (K \in HL \land W \in H)$
43	34	sselda	$⊢ ((φ \land y \in V) \land z \in X) \to z \in V$
44		simplr	$⊢ ((φ \land y \in V) \land z \in X) \to y \in V$
45	1 6 2 3 4 5 7 42 43 44	hdmapellkr	$⊢ ((φ \land y \in V) \land z \in X) \to (S (z) (y) = \underset{˙}{0} \leftrightarrow y \in O (\{z\}))$
46	1 6 2 3 42 44 43	dochsncom	$⊢ ((φ \land y \in V) \land z \in X) \to (y \in O (\{z\}) \leftrightarrow z \in O (\{y\}))$
47	45 46	bitrd	$⊢ ((φ \land y \in V) \land z \in X) \to (S (z) (y) = \underset{˙}{0} \leftrightarrow z \in O (\{y\}))$
48	47	ralbidva	$⊢ (φ \land y \in V) \to (\forall z \in X S (z) (y) = \underset{˙}{0} \leftrightarrow \forall z \in X z \in O (\{y\}))$
49	41 48	bitr4d	$⊢ (φ \land y \in V) \to (y \in O (X) \leftrightarrow \forall z \in X S (z) (y) = \underset{˙}{0})$
50	49	pm5.32da	$⊢ φ \to ((y \in V \land y \in O (X)) \leftrightarrow (y \in V \land \forall z \in X S (z) (y) = \underset{˙}{0}))$
51	13 50	bitrd	$⊢ φ \to (y \in O (X) \leftrightarrow (y \in V \land \forall z \in X S (z) (y) = \underset{˙}{0}))$
52	51	eqabdv	$⊢ φ \to O (X) = \{y \| (y \in V \land \forall z \in X S (z) (y) = \underset{˙}{0})\}$
53		df-rab	$⊢ \{y \in V \| \forall z \in X S (z) (y) = \underset{˙}{0}\} = \{y \| (y \in V \land \forall z \in X S (z) (y) = \underset{˙}{0})\}$
54	52 53	eqtr4di	$⊢ φ \to O (X) = \{y \in V \| \forall z \in X S (z) (y) = \underset{˙}{0}\}$

Metamath Proof Explorer

Theorem hdmapoc

Proof