Metamath Proof Explorer

Theorem dochvalr

Description: Orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014)

Ref Expression
Hypotheses dochvalr.o ⊢ ⊥ ˙ = oc ⁡ K
dochvalr.h ⊢ H = LHyp ⁡ K
dochvalr.i ⊢ I = DIsoH ⁡ K ⁡ W
dochvalr.n ⊢ N = ocH ⁡ K ⁡ W
Assertion dochvalr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → N ⁡ X = I ⁡ ⊥ ˙ ⁡ I -1 ⁡ X

Proof

Step Hyp Ref Expression
1 dochvalr.o ⊢ ⊥ ˙ = oc ⁡ K
2 dochvalr.h ⊢ H = LHyp ⁡ K
3 dochvalr.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dochvalr.n ⊢ N = ocH ⁡ K ⁡ W
5 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
6 eqid ⊢ Base DVecH ⁡ K ⁡ W = Base DVecH ⁡ K ⁡ W
7 2 5 3 6 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → X ⊆ Base DVecH ⁡ K ⁡ W
8 eqid ⊢ Base K = Base K
9 eqid ⊢ glb ⁡ K = glb ⁡ K
10 8 9 1 2 3 5 6 4 dochval ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ Base DVecH ⁡ K ⁡ W → N ⁡ X = I ⁡ ⊥ ˙ ⁡ glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y
11 7 10 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → N ⁡ X = I ⁡ ⊥ ˙ ⁡ glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y
12 eqid ⊢ ≤ K = ≤ K
13 hllat ⊢ K ∈ HL → K ∈ Lat
14 13 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → K ∈ Lat
15 hlclat ⊢ K ∈ HL → K ∈ CLat
16 15 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → K ∈ CLat
17 ssrab2 ⊢ y ∈ Base K | X ⊆ I ⁡ y ⊆ Base K
18 8 9 clatglbcl ⊢ K ∈ CLat ∧ y ∈ Base K | X ⊆ I ⁡ y ⊆ Base K → glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ∈ Base K
19 16 17 18 sylancl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ∈ Base K
20 8 2 3 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ Base K
21 17 a1i ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → y ∈ Base K | X ⊆ I ⁡ y ⊆ Base K
22 ssid ⊢ X ⊆ X
23 2 3 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I ⁡ I -1 ⁡ X = X
24 22 23 sseqtrrid ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → X ⊆ I ⁡ I -1 ⁡ X
25 fveq2 ⊢ y = I -1 ⁡ X → I ⁡ y = I ⁡ I -1 ⁡ X
26 25 sseq2d ⊢ y = I -1 ⁡ X → X ⊆ I ⁡ y ↔ X ⊆ I ⁡ I -1 ⁡ X
27 26 elrab ⊢ I -1 ⁡ X ∈ y ∈ Base K | X ⊆ I ⁡ y ↔ I -1 ⁡ X ∈ Base K ∧ X ⊆ I ⁡ I -1 ⁡ X
28 20 24 27 sylanbrc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ y ∈ Base K | X ⊆ I ⁡ y
29 8 12 9 clatglble ⊢ K ∈ CLat ∧ y ∈ Base K | X ⊆ I ⁡ y ⊆ Base K ∧ I -1 ⁡ X ∈ y ∈ Base K | X ⊆ I ⁡ y → glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ≤ K I -1 ⁡ X
30 16 21 28 29 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ≤ K I -1 ⁡ X
31 fveq2 ⊢ y = z → I ⁡ y = I ⁡ z
32 31 sseq2d ⊢ y = z → X ⊆ I ⁡ y ↔ X ⊆ I ⁡ z
33 32 elrab ⊢ z ∈ y ∈ Base K | X ⊆ I ⁡ y ↔ z ∈ Base K ∧ X ⊆ I ⁡ z
34 23 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ z ∈ Base K → I ⁡ I -1 ⁡ X = X
35 34 sseq1d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ z ∈ Base K → I ⁡ I -1 ⁡ X ⊆ I ⁡ z ↔ X ⊆ I ⁡ z
36 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ z ∈ Base K → K ∈ HL ∧ W ∈ H
37 20 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ z ∈ Base K → I -1 ⁡ X ∈ Base K
38 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ z ∈ Base K → z ∈ Base K
39 8 12 2 3 dihord ⊢ K ∈ HL ∧ W ∈ H ∧ I -1 ⁡ X ∈ Base K ∧ z ∈ Base K → I ⁡ I -1 ⁡ X ⊆ I ⁡ z ↔ I -1 ⁡ X ≤ K z
40 36 37 38 39 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ z ∈ Base K → I ⁡ I -1 ⁡ X ⊆ I ⁡ z ↔ I -1 ⁡ X ≤ K z
41 35 40 bitr3d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ z ∈ Base K → X ⊆ I ⁡ z ↔ I -1 ⁡ X ≤ K z
42 41 biimpd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ z ∈ Base K → X ⊆ I ⁡ z → I -1 ⁡ X ≤ K z
43 42 expimpd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → z ∈ Base K ∧ X ⊆ I ⁡ z → I -1 ⁡ X ≤ K z
44 33 43 syl5bi ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → z ∈ y ∈ Base K | X ⊆ I ⁡ y → I -1 ⁡ X ≤ K z
45 44 ralrimiv ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → ∀ z ∈ y ∈ Base K | X ⊆ I ⁡ y I -1 ⁡ X ≤ K z
46 8 12 9 clatleglb ⊢ K ∈ CLat ∧ I -1 ⁡ X ∈ Base K ∧ y ∈ Base K | X ⊆ I ⁡ y ⊆ Base K → I -1 ⁡ X ≤ K glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ↔ ∀ z ∈ y ∈ Base K | X ⊆ I ⁡ y I -1 ⁡ X ≤ K z
47 16 20 21 46 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ≤ K glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y ↔ ∀ z ∈ y ∈ Base K | X ⊆ I ⁡ y I -1 ⁡ X ≤ K z
48 45 47 mpbird ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ≤ K glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y
49 8 12 14 19 20 30 48 latasymd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y = I -1 ⁡ X
50 49 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → ⊥ ˙ ⁡ glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y = ⊥ ˙ ⁡ I -1 ⁡ X
51 50 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I ⁡ ⊥ ˙ ⁡ glb ⁡ K ⁡ y ∈ Base K | X ⊆ I ⁡ y = I ⁡ ⊥ ˙ ⁡ I -1 ⁡ X
52 11 51 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → N ⁡ X = I ⁡ ⊥ ˙ ⁡ I -1 ⁡ X