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 𝐻 = ( LHyp ‘ 𝐾 )
dochss.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochss.v 𝑉 = ( Base ‘ 𝑈 )
dochss.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dochocss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → 𝑋 ⊆ ( ‘ ( 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 dochss.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dochss.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dochss.v 𝑉 = ( Base ‘ 𝑈 )
4 dochss.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
5 ssintub 𝑋 { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 }
6 eqid ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7 1 6 2 3 4 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
8 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
9 8 1 6 4 dochvalr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ‘ ( 𝑋 ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ) ) ) ) )
10 7 9 syldan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ‘ ( 𝑋 ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ) ) ) ) )
11 8 1 6 2 3 4 dochval2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) ) )
12 11 fveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) ) ) )
13 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
15 13 1 6 2 14 dihf11 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1→ ( LSubSp ‘ 𝑈 ) )
16 15 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1→ ( LSubSp ‘ 𝑈 ) )
17 f1f1orn ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1→ ( LSubSp ‘ 𝑈 ) → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
18 16 17 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
19 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
20 19 ad2antrr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → 𝐾 ∈ OP )
21 simpl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
22 ssrab2 { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ⊆ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
23 22 a1i ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ⊆ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
24 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
25 24 1 6 2 3 dih1 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1. ‘ 𝐾 ) ) = 𝑉 )
26 25 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1. ‘ 𝐾 ) ) = 𝑉 )
27 f1fn ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1→ ( LSubSp ‘ 𝑈 ) → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) Fn ( Base ‘ 𝐾 ) )
28 16 27 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) Fn ( Base ‘ 𝐾 ) )
29 13 24 op1cl ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
30 20 29 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
31 fnfvelrn ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) Fn ( Base ‘ 𝐾 ) ∧ ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1. ‘ 𝐾 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
32 28 30 31 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 1. ‘ 𝐾 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
33 26 32 eqeltrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → 𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
34 simpr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → 𝑋𝑉 )
35 sseq2 ( 𝑧 = 𝑉 → ( 𝑋𝑧𝑋𝑉 ) )
36 35 elrab ( 𝑉 ∈ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ↔ ( 𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑋𝑉 ) )
37 33 34 36 sylanbrc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → 𝑉 ∈ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } )
38 37 ne0d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ≠ ∅ )
39 1 6 dihintcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ⊆ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∧ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ≠ ∅ ) ) → { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
40 21 23 38 39 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
41 f1ocnvdm ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∧ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ∈ ( Base ‘ 𝐾 ) )
42 18 40 41 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ∈ ( Base ‘ 𝐾 ) )
43 13 8 opoccl ( ( 𝐾 ∈ OP ∧ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) ∈ ( Base ‘ 𝐾 ) )
44 20 42 43 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) ∈ ( Base ‘ 𝐾 ) )
45 f1ocnvfv1 ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) )
46 18 44 45 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) )
47 12 46 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) )
48 47 fveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) ) )
49 13 8 opococ ( ( 𝐾 ∈ OP ∧ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) )
50 20 42 49 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) )
51 48 50 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) )
52 51 fveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ) ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) )
53 f1ocnvfv2 ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) : ( Base ‘ 𝐾 ) –1-1-onto→ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∧ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) = { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } )
54 18 40 53 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } ) ) = { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } )
55 10 52 54 3eqtrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → { 𝑧 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∣ 𝑋𝑧 } = ( ‘ ( 𝑋 ) ) )
56 5 55 sseqtrid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → 𝑋 ⊆ ( ‘ ( 𝑋 ) ) )