Metamath Proof Explorer

Theorem dochcl

Description: Closure of subspace orthocomplement for DVecH vector space. (Contributed by NM, 9-Mar-2014)

Ref Expression
Hypotheses dochcl.h ⊢H=LHyp⁡K
dochcl.i ⊢I=DIsoH⁡K⁡W
dochcl.u ⊢U=DVecH⁡K⁡W
dochcl.v ⊢V=BaseU
dochcl.o ⊢⊥˙=ocH⁡K⁡W
Assertion dochcl ⊢K∈HL∧W∈H∧X⊆V→⊥˙⁡X∈ran⁡I

Proof

Step Hyp Ref Expression
1 dochcl.h ⊢H=LHyp⁡K
2 dochcl.i ⊢I=DIsoH⁡K⁡W
3 dochcl.u ⊢U=DVecH⁡K⁡W
4 dochcl.v ⊢V=BaseU
5 dochcl.o ⊢⊥˙=ocH⁡K⁡W
6 eqid ⊢BaseK=BaseK
7 eqid ⊢glb⁡K=glb⁡K
8 eqid ⊢oc⁡K=oc⁡K
9 6 7 8 1 2 3 4 5 dochval ⊢K∈HL∧W∈H∧X⊆V→⊥˙⁡X=I⁡oc⁡K⁡glb⁡K⁡y∈BaseK|X⊆I⁡y
10 hlop ⊢K∈HL→K∈OP
11 10 ad2antrr ⊢K∈HL∧W∈H∧X⊆V→K∈OP
12 hlclat ⊢K∈HL→K∈CLat
13 12 ad2antrr ⊢K∈HL∧W∈H∧X⊆V→K∈CLat
14 ssrab2 ⊢y∈BaseK|X⊆I⁡y⊆BaseK
15 6 7 clatglbcl ⊢K∈CLat∧y∈BaseK|X⊆I⁡y⊆BaseK→glb⁡K⁡y∈BaseK|X⊆I⁡y∈BaseK
16 13 14 15 sylancl ⊢K∈HL∧W∈H∧X⊆V→glb⁡K⁡y∈BaseK|X⊆I⁡y∈BaseK
17 6 8 opoccl ⊢K∈OP∧glb⁡K⁡y∈BaseK|X⊆I⁡y∈BaseK→oc⁡K⁡glb⁡K⁡y∈BaseK|X⊆I⁡y∈BaseK
18 11 16 17 syl2anc ⊢K∈HL∧W∈H∧X⊆V→oc⁡K⁡glb⁡K⁡y∈BaseK|X⊆I⁡y∈BaseK
19 6 1 2 dihcl ⊢K∈HL∧W∈H∧oc⁡K⁡glb⁡K⁡y∈BaseK|X⊆I⁡y∈BaseK→I⁡oc⁡K⁡glb⁡K⁡y∈BaseK|X⊆I⁡y∈ran⁡I
20 18 19 syldan ⊢K∈HL∧W∈H∧X⊆V→I⁡oc⁡K⁡glb⁡K⁡y∈BaseK|X⊆I⁡y∈ran⁡I
21 9 20 eqeltrd ⊢K∈HL∧W∈H∧X⊆V→⊥˙⁡X∈ran⁡I