Metamath Proof Explorer

Theorem dochval

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 dochval ⊢K∈Y∧W∈H∧X⊆V→N⁡X=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 5 6 7 8 dochfval ⊢K∈Y∧W∈H→N=x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y
10 9 adantr ⊢K∈Y∧W∈H∧X⊆V→N=x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y
11 10 fveq1d ⊢K∈Y∧W∈H∧X⊆V→N⁡X=x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y⁡X
12 7 fvexi ⊢V∈V
13 12 elpw2 ⊢X∈𝒫V↔X⊆V
14 13 biimpri ⊢X⊆V→X∈𝒫V
15 14 adantl ⊢K∈Y∧W∈H∧X⊆V→X∈𝒫V
16 fvex ⊢I⁡⊥˙⁡G⁡y∈B|X⊆I⁡y∈V
17 sseq1 ⊢x=X→x⊆I⁡y↔X⊆I⁡y
18 17 rabbidv ⊢x=X→y∈B|x⊆I⁡y=y∈B|X⊆I⁡y
19 18 fveq2d ⊢x=X→G⁡y∈B|x⊆I⁡y=G⁡y∈B|X⊆I⁡y
20 19 fveq2d ⊢x=X→⊥˙⁡G⁡y∈B|x⊆I⁡y=⊥˙⁡G⁡y∈B|X⊆I⁡y
21 20 fveq2d ⊢x=X→I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y=I⁡⊥˙⁡G⁡y∈B|X⊆I⁡y
22 eqid ⊢x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y=x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y
23 21 22 fvmptg ⊢X∈𝒫V∧I⁡⊥˙⁡G⁡y∈B|X⊆I⁡y∈V→x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y⁡X=I⁡⊥˙⁡G⁡y∈B|X⊆I⁡y
24 15 16 23 sylancl ⊢K∈Y∧W∈H∧X⊆V→x∈𝒫V⟼I⁡⊥˙⁡G⁡y∈B|x⊆I⁡y⁡X=I⁡⊥˙⁡G⁡y∈B|X⊆I⁡y
25 11 24 eqtrd ⊢K∈Y∧W∈H∧X⊆V→N⁡X=I⁡⊥˙⁡G⁡y∈B|X⊆I⁡y