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 ⊢BaseDVecH⁡K⁡W=BaseDVecH⁡K⁡W
9 2 7 3 8 dihrnss ⊢K∈HL∧W∈H∧X∈ran⁡I→X⊆BaseDVecH⁡K⁡W
10 5 6 9 syl2anc ⊢φ→X⊆BaseDVecH⁡K⁡W
11 2 3 7 8 4 dochcl ⊢K∈HL∧W∈H∧X⊆BaseDVecH⁡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 ⊢BaseK=BaseK
22 21 2 3 dihcnvcl ⊢K∈HL∧W∈H∧X∈ran⁡I→I-1⁡X∈BaseK
23 5 6 22 syl2anc ⊢φ→I-1⁡X∈BaseK
24 21 1 opoccl ⊢K∈OP∧I-1⁡X∈BaseK→⊥˙⁡I-1⁡X∈BaseK
25 20 23 24 syl2anc ⊢φ→⊥˙⁡I-1⁡X∈BaseK
26 21 2 3 dihcnvcl ⊢K∈HL∧W∈H∧N⁡X∈ran⁡I→I-1⁡N⁡X∈BaseK
27 5 12 26 syl2anc ⊢φ→I-1⁡N⁡X∈BaseK
28 21 2 3 dih11 ⊢K∈HL∧W∈H∧⊥˙⁡I-1⁡X∈BaseK∧I-1⁡N⁡X∈BaseK→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