Metamath Proof Explorer

Theorem dochffval

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
Assertion dochffval ⊢K∈V→ocH⁡K=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡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 elex ⊢K∈V→K∈V
6 fveq2 ⊢k=K→LHyp⁡k=LHyp⁡K
7 6 4 eqtr4di ⊢k=K→LHyp⁡k=H
8 fveq2 ⊢k=K→DVecH⁡k=DVecH⁡K
9 8 fveq1d ⊢k=K→DVecH⁡k⁡w=DVecH⁡K⁡w
10 9 fveq2d ⊢k=K→BaseDVecH⁡k⁡w=BaseDVecH⁡K⁡w
11 10 pweqd ⊢k=K→𝒫BaseDVecH⁡k⁡w=𝒫BaseDVecH⁡K⁡w
12 fveq2 ⊢k=K→DIsoH⁡k=DIsoH⁡K
13 12 fveq1d ⊢k=K→DIsoH⁡k⁡w=DIsoH⁡K⁡w
14 fveq2 ⊢k=K→oc⁡k=oc⁡K
15 14 3 eqtr4di ⊢k=K→oc⁡k=⊥˙
16 fveq2 ⊢k=K→glb⁡k=glb⁡K
17 16 2 eqtr4di ⊢k=K→glb⁡k=G
18 fveq2 ⊢k=K→Basek=BaseK
19 18 1 eqtr4di ⊢k=K→Basek=B
20 13 fveq1d ⊢k=K→DIsoH⁡k⁡w⁡y=DIsoH⁡K⁡w⁡y
21 20 sseq2d ⊢k=K→x⊆DIsoH⁡k⁡w⁡y↔x⊆DIsoH⁡K⁡w⁡y
22 19 21 rabeqbidv ⊢k=K→y∈Basek|x⊆DIsoH⁡k⁡w⁡y=y∈B|x⊆DIsoH⁡K⁡w⁡y
23 17 22 fveq12d ⊢k=K→glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y=G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y
24 15 23 fveq12d ⊢k=K→oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y=⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y
25 13 24 fveq12d ⊢k=K→DIsoH⁡k⁡w⁡oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y=DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y
26 11 25 mpteq12dv ⊢k=K→x∈𝒫BaseDVecH⁡k⁡w⟼DIsoH⁡k⁡w⁡oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y=x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y
27 7 26 mpteq12dv ⊢k=K→w∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w⟼DIsoH⁡k⁡w⁡oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y
28 df-doch ⊢ocH=k∈V⟼w∈LHyp⁡k⟼x∈𝒫BaseDVecH⁡k⁡w⟼DIsoH⁡k⁡w⁡oc⁡k⁡glb⁡k⁡y∈Basek|x⊆DIsoH⁡k⁡w⁡y
29 27 28 4 mptfvmpt ⊢K∈V→ocH⁡K=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y
30 5 29 syl ⊢K∈V→ocH⁡K=w∈H⟼x∈𝒫BaseDVecH⁡K⁡w⟼DIsoH⁡K⁡w⁡⊥˙⁡G⁡y∈B|x⊆DIsoH⁡K⁡w⁡y