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 syl5eq ⊢ 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