Metamath Proof Explorer

Theorem hgmapfnN

Description: Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hgmapfn.h ⊢ H = LHyp ⁡ K
hgmapfn.u ⊢ U = DVecH ⁡ K ⁡ W
hgmapfn.r ⊢ R = Scalar ⁡ U
hgmapfn.b ⊢ B = Base R
hgmapfn.g ⊢ G = HGMap ⁡ K ⁡ W
hgmapfn.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion hgmapfnN ⊢ φ → G Fn B

Proof

Step Hyp Ref Expression
1 hgmapfn.h ⊢ H = LHyp ⁡ K
2 hgmapfn.u ⊢ U = DVecH ⁡ K ⁡ W
3 hgmapfn.r ⊢ R = Scalar ⁡ U
4 hgmapfn.b ⊢ B = Base R
5 hgmapfn.g ⊢ G = HGMap ⁡ K ⁡ W
6 hgmapfn.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 riotaex ⊢ ι j ∈ B | ∀ x ∈ Base U HDMap ⁡ K ⁡ W ⁡ k ⋅ U x = j ⋅ LCDual ⁡ K ⁡ W HDMap ⁡ K ⁡ W ⁡ x ∈ V
8 eqid ⊢ k ∈ B ⟼ ι j ∈ B | ∀ x ∈ Base U HDMap ⁡ K ⁡ W ⁡ k ⋅ U x = j ⋅ LCDual ⁡ K ⁡ W HDMap ⁡ K ⁡ W ⁡ x = k ∈ B ⟼ ι j ∈ B | ∀ x ∈ Base U HDMap ⁡ K ⁡ W ⁡ k ⋅ U x = j ⋅ LCDual ⁡ K ⁡ W HDMap ⁡ K ⁡ W ⁡ x
9 7 8 fnmpti ⊢ k ∈ B ⟼ ι j ∈ B | ∀ x ∈ Base U HDMap ⁡ K ⁡ W ⁡ k ⋅ U x = j ⋅ LCDual ⁡ K ⁡ W HDMap ⁡ K ⁡ W ⁡ x Fn B
10 eqid ⊢ Base U = Base U
11 eqid ⊢ ⋅ U = ⋅ U
12 eqid ⊢ LCDual ⁡ K ⁡ W = LCDual ⁡ K ⁡ W
13 eqid ⊢ ⋅ LCDual ⁡ K ⁡ W = ⋅ LCDual ⁡ K ⁡ W
14 eqid ⊢ HDMap ⁡ K ⁡ W = HDMap ⁡ K ⁡ W
15 1 2 10 11 3 4 12 13 14 5 6 hgmapfval ⊢ φ → G = k ∈ B ⟼ ι j ∈ B | ∀ x ∈ Base U HDMap ⁡ K ⁡ W ⁡ k ⋅ U x = j ⋅ LCDual ⁡ K ⁡ W HDMap ⁡ K ⁡ W ⁡ x
16 15 fneq1d ⊢ φ → G Fn B ↔ k ∈ B ⟼ ι j ∈ B | ∀ x ∈ Base U HDMap ⁡ K ⁡ W ⁡ k ⋅ U x = j ⋅ LCDual ⁡ K ⁡ W HDMap ⁡ K ⁡ W ⁡ x Fn B
17 9 16 mpbiri ⊢ φ → G Fn B