This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0vfval

Description: Value of the function for the zero vector on a normed complex vector space. (Contributed by NM, 24-Apr-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses 0vfval.2 ⊢ G = + v ⁡ U
0vfval.5 ⊢ Z = 0 vec ⁡ U
Assertion 0vfval ⊢ U ∈ V → Z = GId ⁡ G

Proof

Step Hyp Ref Expression
1 0vfval.2 ⊢ G = + v ⁡ U
2 0vfval.5 ⊢ Z = 0 vec ⁡ U
3 elex ⊢ U ∈ V → U ∈ V
4 fo1st ⊢ 1 st : V ⟶ onto V
5 fofn ⊢ 1 st : V ⟶ onto V → 1 st Fn V
6 4 5 ax-mp ⊢ 1 st Fn V
7 ssv ⊢ ran ⁡ 1 st ⊆ V
8 fnco ⊢ 1 st Fn V ∧ 1 st Fn V ∧ ran ⁡ 1 st ⊆ V → 1 st ∘ 1 st Fn V
9 6 6 7 8 mp3an ⊢ 1 st ∘ 1 st Fn V
10 df-va ⊢ + v = 1 st ∘ 1 st
11 10 fneq1i ⊢ + v Fn V ↔ 1 st ∘ 1 st Fn V
12 9 11 mpbir ⊢ + v Fn V
13 fvco2 ⊢ + v Fn V ∧ U ∈ V → GId ∘ + v ⁡ U = GId ⁡ + v ⁡ U
14 12 13 mpan ⊢ U ∈ V → GId ∘ + v ⁡ U = GId ⁡ + v ⁡ U
15 df-0v ⊢ 0 vec = GId ∘ + v
16 15 fveq1i ⊢ 0 vec ⁡ U = GId ∘ + v ⁡ U
17 2 16 eqtri ⊢ Z = GId ∘ + v ⁡ U
18 1 fveq2i ⊢ GId ⁡ G = GId ⁡ + v ⁡ U
19 14 17 18 3eqtr4g ⊢ U ∈ V → Z = GId ⁡ G
20 3 19 syl ⊢ U ∈ V → Z = GId ⁡ G