Metamath Proof Explorer

Theorem 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 ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
Assertion dochocss ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ 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 ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
5 ssintub ⊢ X ⊆ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
6 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
7 1 6 2 3 4 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W
8 eqid ⊢ oc ⁡ K = oc ⁡ K
9 8 1 6 4 dochvalr ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⊥ ˙ ⁡ X
10 7 9 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⊥ ˙ ⁡ X
11 8 1 6 2 3 4 dochval2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X = DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
12 11 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W -1 ⁡ ⊥ ˙ ⁡ X = DIsoH ⁡ K ⁡ W -1 ⁡ DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
13 eqid ⊢ Base K = Base K
14 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
15 13 1 6 2 14 dihf11 ⊢ K ∈ HL ∧ W ∈ H → DIsoH ⁡ K ⁡ W : Base K ⟶ 1-1 LSubSp ⁡ U
16 15 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W : Base K ⟶ 1-1 LSubSp ⁡ U
17 f1f1orn ⊢ DIsoH ⁡ K ⁡ W : Base K ⟶ 1-1 LSubSp ⁡ U → DIsoH ⁡ K ⁡ W : Base K ⟶ 1-1 onto ran ⁡ DIsoH ⁡ K ⁡ W
18 16 17 syl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W : Base K ⟶ 1-1 onto ran ⁡ DIsoH ⁡ K ⁡ W
19 hlop ⊢ K ∈ HL → K ∈ OP
20 19 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → K ∈ OP
21 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → K ∈ HL ∧ W ∈ H
22 ssrab2 ⊢ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ⊆ ran ⁡ DIsoH ⁡ K ⁡ W
23 22 a1i ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ⊆ ran ⁡ DIsoH ⁡ K ⁡ W
24 eqid ⊢ 1. ⁡ K = 1. ⁡ K
25 24 1 6 2 3 dih1 ⊢ K ∈ HL ∧ W ∈ H → DIsoH ⁡ K ⁡ W ⁡ 1. ⁡ K = V
26 25 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W ⁡ 1. ⁡ K = V
27 f1fn ⊢ DIsoH ⁡ K ⁡ W : Base K ⟶ 1-1 LSubSp ⁡ U → DIsoH ⁡ K ⁡ W Fn Base K
28 16 27 syl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W Fn Base K
29 13 24 op1cl ⊢ K ∈ OP → 1. ⁡ K ∈ Base K
30 20 29 syl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → 1. ⁡ K ∈ Base K
31 fnfvelrn ⊢ DIsoH ⁡ K ⁡ W Fn Base K ∧ 1. ⁡ K ∈ Base K → DIsoH ⁡ K ⁡ W ⁡ 1. ⁡ K ∈ ran ⁡ DIsoH ⁡ K ⁡ W
32 28 30 31 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W ⁡ 1. ⁡ K ∈ ran ⁡ DIsoH ⁡ K ⁡ W
33 26 32 eqeltrrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → V ∈ ran ⁡ DIsoH ⁡ K ⁡ W
34 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → X ⊆ V
35 sseq2 ⊢ z = V → X ⊆ z ↔ X ⊆ V
36 35 elrab ⊢ V ∈ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ↔ V ∈ ran ⁡ DIsoH ⁡ K ⁡ W ∧ X ⊆ V
37 33 34 36 sylanbrc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → V ∈ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
38 37 ne0d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ≠ ∅
39 1 6 dihintcl ⊢ K ∈ HL ∧ W ∈ H ∧ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ⊆ ran ⁡ DIsoH ⁡ K ⁡ W ∧ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ≠ ∅ → ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W
40 21 23 38 39 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W
41 f1ocnvdm ⊢ DIsoH ⁡ K ⁡ W : Base K ⟶ 1-1 onto ran ⁡ DIsoH ⁡ K ⁡ W ∧ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W → DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ Base K
42 18 40 41 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ Base K
43 13 8 opoccl ⊢ K ∈ OP ∧ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ Base K → oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ Base K
44 20 42 43 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ Base K
45 f1ocnvfv1 ⊢ DIsoH ⁡ K ⁡ W : Base K ⟶ 1-1 onto ran ⁡ DIsoH ⁡ K ⁡ W ∧ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ Base K → DIsoH ⁡ K ⁡ W -1 ⁡ DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z = oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
46 18 44 45 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W -1 ⁡ DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z = oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
47 12 46 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W -1 ⁡ ⊥ ˙ ⁡ X = oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
48 47 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⊥ ˙ ⁡ X = oc ⁡ K ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
49 13 8 opococ ⊢ K ∈ OP ∧ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ Base K → oc ⁡ K ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z = DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
50 20 42 49 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → oc ⁡ K ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z = DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
51 48 50 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⊥ ˙ ⁡ X = DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
52 51 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⊥ ˙ ⁡ X = DIsoH ⁡ K ⁡ W ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
53 f1ocnvfv2 ⊢ DIsoH ⁡ K ⁡ W : Base K ⟶ 1-1 onto ran ⁡ DIsoH ⁡ K ⁡ W ∧ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W → DIsoH ⁡ K ⁡ W ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z = ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
54 18 40 53 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → DIsoH ⁡ K ⁡ W ⁡ DIsoH ⁡ K ⁡ W -1 ⁡ ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z = ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z
55 10 52 54 3eqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⋂ z ∈ ran ⁡ DIsoH ⁡ K ⁡ W | X ⊆ z = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
56 5 55 sseqtrid ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X