Description: A vector plus itself is two times the vector. (Contributed by NM, 9-Feb-2008) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nvdi.1 | ⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) | |
nvdi.2 | ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) | ||
nvdi.4 | ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) | ||
Assertion | nv2 | ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐴 ) = ( 2 𝑆 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nvdi.1 | ⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) | |
2 | nvdi.2 | ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) | |
3 | nvdi.4 | ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) | |
4 | eqid | ⊢ ( 1st ‘ 𝑈 ) = ( 1st ‘ 𝑈 ) | |
5 | 4 | nvvc | ⊢ ( 𝑈 ∈ NrmCVec → ( 1st ‘ 𝑈 ) ∈ CVecOLD ) |
6 | 2 | vafval | ⊢ 𝐺 = ( 1st ‘ ( 1st ‘ 𝑈 ) ) |
7 | 3 | smfval | ⊢ 𝑆 = ( 2nd ‘ ( 1st ‘ 𝑈 ) ) |
8 | 1 2 | bafval | ⊢ 𝑋 = ran 𝐺 |
9 | 6 7 8 | vc2OLD | ⊢ ( ( ( 1st ‘ 𝑈 ) ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐴 ) = ( 2 𝑆 𝐴 ) ) |
10 | 5 9 | sylan | ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐴 ) = ( 2 𝑆 𝐴 ) ) |