Metamath Proof Explorer


Theorem vafval

Description: Value of the function for the vector addition (group) operation on a normed complex vector space. (Contributed by NM, 23-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis vafval.2 𝐺 = ( +𝑣𝑈 )
Assertion vafval 𝐺 = ( 1st ‘ ( 1st𝑈 ) )

Proof

Step Hyp Ref Expression
1 vafval.2 𝐺 = ( +𝑣𝑈 )
2 df-va +𝑣 = ( 1st ∘ 1st )
3 2 fveq1i ( +𝑣𝑈 ) = ( ( 1st ∘ 1st ) ‘ 𝑈 )
4 fo1st 1st : V –onto→ V
5 fof ( 1st : V –onto→ V → 1st : V ⟶ V )
6 4 5 ax-mp 1st : V ⟶ V
7 fvco3 ( ( 1st : V ⟶ V ∧ 𝑈 ∈ V ) → ( ( 1st ∘ 1st ) ‘ 𝑈 ) = ( 1st ‘ ( 1st𝑈 ) ) )
8 6 7 mpan ( 𝑈 ∈ V → ( ( 1st ∘ 1st ) ‘ 𝑈 ) = ( 1st ‘ ( 1st𝑈 ) ) )
9 3 8 syl5eq ( 𝑈 ∈ V → ( +𝑣𝑈 ) = ( 1st ‘ ( 1st𝑈 ) ) )
10 fvprc ( ¬ 𝑈 ∈ V → ( +𝑣𝑈 ) = ∅ )
11 fvprc ( ¬ 𝑈 ∈ V → ( 1st𝑈 ) = ∅ )
12 11 fveq2d ( ¬ 𝑈 ∈ V → ( 1st ‘ ( 1st𝑈 ) ) = ( 1st ‘ ∅ ) )
13 1st0 ( 1st ‘ ∅ ) = ∅
14 12 13 eqtr2di ( ¬ 𝑈 ∈ V → ∅ = ( 1st ‘ ( 1st𝑈 ) ) )
15 10 14 eqtrd ( ¬ 𝑈 ∈ V → ( +𝑣𝑈 ) = ( 1st ‘ ( 1st𝑈 ) ) )
16 9 15 pm2.61i ( +𝑣𝑈 ) = ( 1st ‘ ( 1st𝑈 ) )
17 1 16 eqtri 𝐺 = ( 1st ‘ ( 1st𝑈 ) )