Metamath Proof Explorer

Theorem dochfval

Description: Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014)

Ref Expression
Hypotheses dochval.b ⊢B=BaseK
dochval.g ⊢G=glb⁡K
dochval.o ⊢⊥˙=oc⁡K
dochval.h ⊢H=LHyp⁡K
dochval.i ⊢I=DIsoH⁡K⁡W
dochval.u ⊢U=DVecH⁡K⁡W
dochval.v ⊢V=BaseU
dochval.n ⊢N=ocH⁡K⁡W
Assertion dochfval ⊢K∈X∧W∈H→N=x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y

Proof

Step Hyp Ref Expression
1 dochval.b ⊢B=BaseK
2 dochval.g ⊢G=glb⁡K
3 dochval.o ⊢⊥˙=oc⁡K
4 dochval.h ⊢H=LHyp⁡K
5 dochval.i ⊢I=DIsoH⁡K⁡W
6 dochval.u ⊢U=DVecH⁡K⁡W
7 dochval.v ⊢V=BaseU
8 dochval.n ⊢N=ocH⁡K⁡W
9 1 2 3 4 dochffval ⊢K∈X→ocH⁡K=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y
10 9 fveq1d ⊢K∈X→ocH⁡K⁡W=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y⁡W
11 8 10 eqtrid ⊢K∈X→N=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y⁡W
12 fveq2 ⊢w=W→DVecH⁡K⁡w=DVecH⁡K⁡W
13 12 6 eqtr4di ⊢w=W→DVecH⁡K⁡w=U
14 13 fveq2d ⊢w=W→BaseDVecH⁡K⁡w=BaseU
15 14 7 eqtr4di ⊢w=W→BaseDVecH⁡K⁡w=V
16 15 pweqd ⊢w=W→𝒫BaseDVecH⁡K⁡w=𝒫V
17 fveq2 ⊢w=W→DIsoH⁡K⁡w=DIsoH⁡K⁡W
18 17 5 eqtr4di ⊢w=W→DIsoH⁡K⁡w=I
19 18 fveq1d ⊢w=W→DIsoH⁡K⁡w⁡y=I⁡y
20 19 sseq2d ⊢w=W→x⊆DIsoH⁡K⁡w⁡y↔x⊆I⁡y
21 20 rabbidv ⊢w=W→y∈B|x⊆DIsoH⁡K⁡w⁡y=y∈B|x⊆I⁡y
22 21 fveq2d ⊢w=W→G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y=G⁡y∈B|x⊆I⁡y
23 22 fveq2d ⊢w=W→⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y=⊥˙⁡G⁡y∈B|x⊆I⁡y
24 18 23 fveq12d ⊢w=W→DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y=I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y
25 16 24 mpteq12dv ⊢w=W→x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y=x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y
26 eqid ⊢w∈H⟼x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y
27 7 fvexi ⊢V∈V
28 27 pwex ⊢𝒫V∈V
29 28 mptex ⊢x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y∈V
30 25 26 29 fvmpt ⊢W∈H→w∈H⟼x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y⁡W=x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y
31 11 30 sylan9eq ⊢K∈X∧W∈H→N=x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y