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