Metamath Proof Explorer

Theorem dochvalr3

Description: Orthocomplement of a closed subspace. (Contributed by NM, 15-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 dochvalr3.o ⊢ ⊥ ˙ = oc ⁡ K
2 dochvalr3.h ⊢ H = LHyp ⁡ K
3 dochvalr3.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dochvalr3.n ⊢ N = ocH ⁡ K ⁡ W
5 dochvalr3.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 dochvalr3.x ⊢ φ → X ∈ ran ⁡ I
7 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
8 eqid ⊢ Base DVecH ⁡ K ⁡ W = Base DVecH ⁡ K ⁡ W
9 2 7 3 8 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → X ⊆ Base DVecH ⁡ K ⁡ W
10 5 6 9 syl2anc ⊢ φ → X ⊆ Base DVecH ⁡ K ⁡ W
11 2 3 7 8 4 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ Base DVecH ⁡ K ⁡ W → N ⁡ X ∈ ran ⁡ I
12 5 10 11 syl2anc ⊢ φ → N ⁡ X ∈ ran ⁡ I
13 2 3 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ N ⁡ X ∈ ran ⁡ I → I ⁡ I -1 ⁡ N ⁡ X = N ⁡ X
14 5 12 13 syl2anc ⊢ φ → I ⁡ I -1 ⁡ N ⁡ X = N ⁡ X
15 1 2 3 4 dochvalr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → N ⁡ X = I ⁡ ⊥ ˙ ⁡ I -1 ⁡ X
16 5 6 15 syl2anc ⊢ φ → N ⁡ X = I ⁡ ⊥ ˙ ⁡ I -1 ⁡ X
17 14 16 eqtr2d ⊢ φ → I ⁡ ⊥ ˙ ⁡ I -1 ⁡ X = I ⁡ I -1 ⁡ N ⁡ X
18 5 simpld ⊢ φ → K ∈ HL
19 hlop ⊢ K ∈ HL → K ∈ OP
20 18 19 syl ⊢ φ → K ∈ OP
21 eqid ⊢ Base K = Base K
22 21 2 3 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ Base K
23 5 6 22 syl2anc ⊢ φ → I -1 ⁡ X ∈ Base K
24 21 1 opoccl ⊢ K ∈ OP ∧ I -1 ⁡ X ∈ Base K → ⊥ ˙ ⁡ I -1 ⁡ X ∈ Base K
25 20 23 24 syl2anc ⊢ φ → ⊥ ˙ ⁡ I -1 ⁡ X ∈ Base K
26 21 2 3 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ N ⁡ X ∈ ran ⁡ I → I -1 ⁡ N ⁡ X ∈ Base K
27 5 12 26 syl2anc ⊢ φ → I -1 ⁡ N ⁡ X ∈ Base K
28 21 2 3 dih11 ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ I -1 ⁡ X ∈ Base K ∧ I -1 ⁡ N ⁡ X ∈ Base K → I ⁡ ⊥ ˙ ⁡ I -1 ⁡ X = I ⁡ I -1 ⁡ N ⁡ X ↔ ⊥ ˙ ⁡ I -1 ⁡ X = I -1 ⁡ N ⁡ X
29 5 25 27 28 syl3anc ⊢ φ → I ⁡ ⊥ ˙ ⁡ I -1 ⁡ X = I ⁡ I -1 ⁡ N ⁡ X ↔ ⊥ ˙ ⁡ I -1 ⁡ X = I -1 ⁡ N ⁡ X
30 17 29 mpbid ⊢ φ → ⊥ ˙ ⁡ I -1 ⁡ X = I -1 ⁡ N ⁡ X