Step |
Hyp |
Ref |
Expression |
1 |
|
nvop.2 |
⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) |
2 |
|
nvop.4 |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
3 |
|
nvop.6 |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
4 |
|
nvrel |
⊢ Rel NrmCVec |
5 |
|
1st2nd |
⊢ ( ( Rel NrmCVec ∧ 𝑈 ∈ NrmCVec ) → 𝑈 = 〈 ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) 〉 ) |
6 |
4 5
|
mpan |
⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = 〈 ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) 〉 ) |
7 |
3
|
nmcvfval |
⊢ 𝑁 = ( 2nd ‘ 𝑈 ) |
8 |
7
|
opeq2i |
⊢ 〈 ( 1st ‘ 𝑈 ) , 𝑁 〉 = 〈 ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) 〉 |
9 |
|
eqid |
⊢ ( 1st ‘ 𝑈 ) = ( 1st ‘ 𝑈 ) |
10 |
9 1 2
|
nvvop |
⊢ ( 𝑈 ∈ NrmCVec → ( 1st ‘ 𝑈 ) = 〈 𝐺 , 𝑆 〉 ) |
11 |
10
|
opeq1d |
⊢ ( 𝑈 ∈ NrmCVec → 〈 ( 1st ‘ 𝑈 ) , 𝑁 〉 = 〈 〈 𝐺 , 𝑆 〉 , 𝑁 〉 ) |
12 |
8 11
|
eqtr3id |
⊢ ( 𝑈 ∈ NrmCVec → 〈 ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) 〉 = 〈 〈 𝐺 , 𝑆 〉 , 𝑁 〉 ) |
13 |
6 12
|
eqtrd |
⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = 〈 〈 𝐺 , 𝑆 〉 , 𝑁 〉 ) |