Metamath Proof Explorer

Theorem mapdfval

Description: Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015)

Ref Expression
Hypotheses mapdval.h ⊢H=LHyp⁡K
mapdval.u ⊢U=DVecH⁡K⁡W
mapdval.s ⊢S=LSubSp⁡U
mapdval.f ⊢F=LFnl⁡U
mapdval.l ⊢L=LKer⁡U
mapdval.o ⊢O=ocH⁡K⁡W
mapdval.m ⊢M=mapd⁡K⁡W
Assertion mapdfval ⊢K∈X∧W∈H→M=s∈S⟼f∈F|O⁡O⁡L⁡f=L⁡f∧O⁡L⁡f⊆s

Proof

Step Hyp Ref Expression
1 mapdval.h ⊢H=LHyp⁡K
2 mapdval.u ⊢U=DVecH⁡K⁡W
3 mapdval.s ⊢S=LSubSp⁡U
4 mapdval.f ⊢F=LFnl⁡U
5 mapdval.l ⊢L=LKer⁡U
6 mapdval.o ⊢O=ocH⁡K⁡W
7 mapdval.m ⊢M=mapd⁡K⁡W
8 1 mapdffval ⊢K∈X→mapd⁡K=w∈H⟼s∈LSubSp⁡DVecH⁡K⁡w⟼f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f∧ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s
9 8 fveq1d ⊢K∈X→mapd⁡K⁡W=w∈H⟼s∈LSubSp⁡DVecH⁡K⁡w⟼f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f∧ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s⁡W
10 7 9 eqtrid ⊢K∈X→M=w∈H⟼s∈LSubSp⁡DVecH⁡K⁡w⟼f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f∧ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s⁡W
11 fveq2 ⊢w=W→DVecH⁡K⁡w=DVecH⁡K⁡W
12 11 2 eqtr4di ⊢w=W→DVecH⁡K⁡w=U
13 12 fveq2d ⊢w=W→LSubSp⁡DVecH⁡K⁡w=LSubSp⁡U
14 13 3 eqtr4di ⊢w=W→LSubSp⁡DVecH⁡K⁡w=S
15 12 fveq2d ⊢w=W→LFnl⁡DVecH⁡K⁡w=LFnl⁡U
16 15 4 eqtr4di ⊢w=W→LFnl⁡DVecH⁡K⁡w=F
17 fveq2 ⊢w=W→ocH⁡K⁡w=ocH⁡K⁡W
18 17 6 eqtr4di ⊢w=W→ocH⁡K⁡w=O
19 12 fveq2d ⊢w=W→LKer⁡DVecH⁡K⁡w=LKer⁡U
20 19 5 eqtr4di ⊢w=W→LKer⁡DVecH⁡K⁡w=L
21 20 fveq1d ⊢w=W→LKer⁡DVecH⁡K⁡w⁡f=L⁡f
22 18 21 fveq12d ⊢w=W→ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=O⁡L⁡f
23 18 22 fveq12d ⊢w=W→ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=O⁡O⁡L⁡f
24 23 21 eqeq12d ⊢w=W→ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f↔O⁡O⁡L⁡f=L⁡f
25 22 sseq1d ⊢w=W→ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s↔O⁡L⁡f⊆s
26 24 25 anbi12d ⊢w=W→ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f∧ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s↔O⁡O⁡L⁡f=L⁡f∧O⁡L⁡f⊆s
27 16 26 rabeqbidv ⊢w=W→f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f∧ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s=f∈F|O⁡O⁡L⁡f=L⁡f∧O⁡L⁡f⊆s
28 14 27 mpteq12dv ⊢w=W→s∈LSubSp⁡DVecH⁡K⁡w⟼f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f∧ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s=s∈S⟼f∈F|O⁡O⁡L⁡f=L⁡f∧O⁡L⁡f⊆s
29 eqid ⊢w∈H⟼s∈LSubSp⁡DVecH⁡K⁡w⟼f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f∧ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s=w∈H⟼s∈LSubSp⁡DVecH⁡K⁡w⟼f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f∧ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s
30 28 29 3 mptfvmpt ⊢W∈H→w∈H⟼s∈LSubSp⁡DVecH⁡K⁡w⟼f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f∧ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s⁡W=s∈S⟼f∈F|O⁡O⁡L⁡f=L⁡f∧O⁡L⁡f⊆s
31 10 30 sylan9eq ⊢K∈X∧W∈H→M=s∈S⟼f∈F|O⁡O⁡L⁡f=L⁡f∧O⁡L⁡f⊆s