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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )