Metamath Proof Explorer

Theorem hdmapfnN

Description: Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmapfn.h ⊢ H = LHyp ⁡ K
hdmapfn.u ⊢ U = DVecH ⁡ K ⁡ W
hdmapfn.v ⊢ V = Base U
hdmapfn.s ⊢ S = HDMap ⁡ K ⁡ W
hdmapfn.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion hdmapfnN ⊢ φ → S Fn V

Proof

Step Hyp Ref Expression
1 hdmapfn.h ⊢ H = LHyp ⁡ K
2 hdmapfn.u ⊢ U = DVecH ⁡ K ⁡ W
3 hdmapfn.v ⊢ V = Base U
4 hdmapfn.s ⊢ S = HDMap ⁡ K ⁡ W
5 hdmapfn.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 riotaex ⊢ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ V ¬ z ∈ LSpan ⁡ U ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∪ LSpan ⁡ U ⁡ t → y = HDMap1 ⁡ K ⁡ W ⁡ z HDMap1 ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W HVMap ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W z t ∈ V
7 eqid ⊢ t ∈ V ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ V ¬ z ∈ LSpan ⁡ U ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∪ LSpan ⁡ U ⁡ t → y = HDMap1 ⁡ K ⁡ W ⁡ z HDMap1 ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W HVMap ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W z t = t ∈ V ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ V ¬ z ∈ LSpan ⁡ U ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∪ LSpan ⁡ U ⁡ t → y = HDMap1 ⁡ K ⁡ W ⁡ z HDMap1 ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W HVMap ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W z t
8 6 7 fnmpti ⊢ t ∈ V ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ V ¬ z ∈ LSpan ⁡ U ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∪ LSpan ⁡ U ⁡ t → y = HDMap1 ⁡ K ⁡ W ⁡ z HDMap1 ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W HVMap ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W z t Fn V
9 eqid ⊢ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
10 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
11 eqid ⊢ LCDual ⁡ K ⁡ W = LCDual ⁡ K ⁡ W
12 eqid ⊢ Base LCDual ⁡ K ⁡ W = Base LCDual ⁡ K ⁡ W
13 eqid ⊢ HVMap ⁡ K ⁡ W = HVMap ⁡ K ⁡ W
14 eqid ⊢ HDMap1 ⁡ K ⁡ W = HDMap1 ⁡ K ⁡ W
15 1 9 2 3 10 11 12 13 14 4 5 hdmapfval ⊢ φ → S = t ∈ V ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ V ¬ z ∈ LSpan ⁡ U ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∪ LSpan ⁡ U ⁡ t → y = HDMap1 ⁡ K ⁡ W ⁡ z HDMap1 ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W HVMap ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W z t
16 15 fneq1d ⊢ φ → S Fn V ↔ t ∈ V ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ V ¬ z ∈ LSpan ⁡ U ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∪ LSpan ⁡ U ⁡ t → y = HDMap1 ⁡ K ⁡ W ⁡ z HDMap1 ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W HVMap ⁡ K ⁡ W ⁡ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W z t Fn V
17 8 16 mpbiri ⊢ φ → S Fn V