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 = Base U
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 = Base U
5 dochcl.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
6 eqid ⊢ Base K = Base K
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 ∈ Base K | 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 ∈ Base K | X ⊆ I ⁡ y ⊆ Base K
15 6 7 clatglbcl ⊢ K ∈ CLat ∧ y ∈ Base K | X ⊆ I ⁡ y ⊆ Base K → glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ∈ Base K
16 13 14 15 sylancl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ∈ Base K
17 6 8 opoccl ⊢ K ∈ OP ∧ glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ∈ Base K → oc ⁡ K ⁡ glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ∈ Base K
18 11 16 17 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → oc ⁡ K ⁡ glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ∈ Base K
19 6 1 2 dihcl ⊢ K ∈ HL ∧ W ∈ H ∧ oc ⁡ K ⁡ glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ∈ Base K → I ⁡ oc ⁡ K ⁡ glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ∈ ran ⁡ I
20 18 19 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → I ⁡ oc ⁡ K ⁡ glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ∈ ran ⁡ I
21 9 20 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ∈ ran ⁡ I