Metamath Proof Explorer

Theorem mapdval3N

Description: Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdval2.h ⊢ H = LHyp ⁡ K
mapdval2.u ⊢ U = DVecH ⁡ K ⁡ W
mapdval2.s ⊢ S = LSubSp ⁡ U
mapdval2.n ⊢ N = LSpan ⁡ U
mapdval2.f ⊢ F = LFnl ⁡ U
mapdval2.l ⊢ L = LKer ⁡ U
mapdval2.o ⊢ O = ocH ⁡ K ⁡ W
mapdval2.m ⊢ M = mapd ⁡ K ⁡ W
mapdval2.k ⊢ φ → K ∈ HL ∧ W ∈ H
mapdval2.t ⊢ φ → T ∈ S
mapdval2.c ⊢ C = g ∈ F | O ⁡ O ⁡ L ⁡ g = L ⁡ g
Assertion mapdval3N ⊢ φ → M ⁡ T = ⋃ v ∈ T f ∈ C | O ⁡ L ⁡ f = N ⁡ v

Proof

Step Hyp Ref Expression
1 mapdval2.h ⊢ H = LHyp ⁡ K
2 mapdval2.u ⊢ U = DVecH ⁡ K ⁡ W
3 mapdval2.s ⊢ S = LSubSp ⁡ U
4 mapdval2.n ⊢ N = LSpan ⁡ U
5 mapdval2.f ⊢ F = LFnl ⁡ U
6 mapdval2.l ⊢ L = LKer ⁡ U
7 mapdval2.o ⊢ O = ocH ⁡ K ⁡ W
8 mapdval2.m ⊢ M = mapd ⁡ K ⁡ W
9 mapdval2.k ⊢ φ → K ∈ HL ∧ W ∈ H
10 mapdval2.t ⊢ φ → T ∈ S
11 mapdval2.c ⊢ C = g ∈ F | O ⁡ O ⁡ L ⁡ g = L ⁡ g
12 1 2 3 4 5 6 7 8 9 10 11 mapdval2N ⊢ φ → M ⁡ T = f ∈ C | ∃ v ∈ T O ⁡ L ⁡ f = N ⁡ v
13 iunrab ⊢ ⋃ v ∈ T f ∈ C | O ⁡ L ⁡ f = N ⁡ v = f ∈ C | ∃ v ∈ T O ⁡ L ⁡ f = N ⁡ v
14 12 13 eqtr4di ⊢ φ → M ⁡ T = ⋃ v ∈ T f ∈ C | O ⁡ L ⁡ f = N ⁡ v