Metamath Proof Explorer

Theorem mapdffval

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

Ref Expression
Hypothesis mapdval.h ⊢H=LHyp⁡K
Assertion 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

Proof

Step Hyp Ref Expression
1 mapdval.h ⊢H=LHyp⁡K
2 elex ⊢K∈X→K∈V
3 fveq2 ⊢k=K→LHyp⁡k=LHyp⁡K
4 3 1 eqtr4di ⊢k=K→LHyp⁡k=H
5 fveq2 ⊢k=K→DVecH⁡k=DVecH⁡K
6 5 fveq1d ⊢k=K→DVecH⁡k⁡w=DVecH⁡K⁡w
7 6 fveq2d ⊢k=K→LSubSp⁡DVecH⁡k⁡w=LSubSp⁡DVecH⁡K⁡w
8 6 fveq2d ⊢k=K→LFnl⁡DVecH⁡k⁡w=LFnl⁡DVecH⁡K⁡w
9 fveq2 ⊢k=K→ocH⁡k=ocH⁡K
10 9 fveq1d ⊢k=K→ocH⁡k⁡w=ocH⁡K⁡w
11 6 fveq2d ⊢k=K→LKer⁡DVecH⁡k⁡w=LKer⁡DVecH⁡K⁡w
12 11 fveq1d ⊢k=K→LKer⁡DVecH⁡k⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f
13 10 12 fveq12d ⊢k=K→ocH⁡k⁡w⁡LKer⁡DVecH⁡k⁡w⁡f=ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f
14 10 13 fveq12d ⊢k=K→ocH⁡k⁡w⁡ocH⁡k⁡w⁡LKer⁡DVecH⁡k⁡w⁡f=ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f
15 14 12 eqeq12d ⊢k=K→ocH⁡k⁡w⁡ocH⁡k⁡w⁡LKer⁡DVecH⁡k⁡w⁡f=LKer⁡DVecH⁡k⁡w⁡f↔ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f
16 13 sseq1d ⊢k=K→ocH⁡k⁡w⁡LKer⁡DVecH⁡k⁡w⁡f⊆s↔ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f⊆s
17 15 16 anbi12d ⊢k=K→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↔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
18 8 17 rabeqbidv ⊢k=K→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∈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
19 7 18 mpteq12dv ⊢k=K→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∈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
20 4 19 mpteq12dv ⊢k=K→w∈LHyp⁡k⟼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
21 df-mapd ⊢mapd=k∈V⟼w∈LHyp⁡k⟼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
22 20 21 1 mptfvmpt ⊢K∈V→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
23 2 22 syl ⊢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