Step |
Hyp |
Ref |
Expression |
1 |
|
nvvop.1 |
⊢ 𝑊 = ( 1st ‘ 𝑈 ) |
2 |
|
nvvop.2 |
⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) |
3 |
|
nvvop.4 |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
4 |
|
vcrel |
⊢ Rel CVecOLD |
5 |
|
nvss |
⊢ NrmCVec ⊆ ( CVecOLD × V ) |
6 |
|
eqid |
⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 ) |
7 |
1 6
|
nvop2 |
⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = 〈 𝑊 , ( normCV ‘ 𝑈 ) 〉 ) |
8 |
7
|
eleq1d |
⊢ ( 𝑈 ∈ NrmCVec → ( 𝑈 ∈ NrmCVec ↔ 〈 𝑊 , ( normCV ‘ 𝑈 ) 〉 ∈ NrmCVec ) ) |
9 |
8
|
ibi |
⊢ ( 𝑈 ∈ NrmCVec → 〈 𝑊 , ( normCV ‘ 𝑈 ) 〉 ∈ NrmCVec ) |
10 |
5 9
|
sselid |
⊢ ( 𝑈 ∈ NrmCVec → 〈 𝑊 , ( normCV ‘ 𝑈 ) 〉 ∈ ( CVecOLD × V ) ) |
11 |
|
opelxp1 |
⊢ ( 〈 𝑊 , ( normCV ‘ 𝑈 ) 〉 ∈ ( CVecOLD × V ) → 𝑊 ∈ CVecOLD ) |
12 |
10 11
|
syl |
⊢ ( 𝑈 ∈ NrmCVec → 𝑊 ∈ CVecOLD ) |
13 |
|
1st2nd |
⊢ ( ( Rel CVecOLD ∧ 𝑊 ∈ CVecOLD ) → 𝑊 = 〈 ( 1st ‘ 𝑊 ) , ( 2nd ‘ 𝑊 ) 〉 ) |
14 |
4 12 13
|
sylancr |
⊢ ( 𝑈 ∈ NrmCVec → 𝑊 = 〈 ( 1st ‘ 𝑊 ) , ( 2nd ‘ 𝑊 ) 〉 ) |
15 |
2
|
vafval |
⊢ 𝐺 = ( 1st ‘ ( 1st ‘ 𝑈 ) ) |
16 |
1
|
fveq2i |
⊢ ( 1st ‘ 𝑊 ) = ( 1st ‘ ( 1st ‘ 𝑈 ) ) |
17 |
15 16
|
eqtr4i |
⊢ 𝐺 = ( 1st ‘ 𝑊 ) |
18 |
3
|
smfval |
⊢ 𝑆 = ( 2nd ‘ ( 1st ‘ 𝑈 ) ) |
19 |
1
|
fveq2i |
⊢ ( 2nd ‘ 𝑊 ) = ( 2nd ‘ ( 1st ‘ 𝑈 ) ) |
20 |
18 19
|
eqtr4i |
⊢ 𝑆 = ( 2nd ‘ 𝑊 ) |
21 |
17 20
|
opeq12i |
⊢ 〈 𝐺 , 𝑆 〉 = 〈 ( 1st ‘ 𝑊 ) , ( 2nd ‘ 𝑊 ) 〉 |
22 |
14 21
|
eqtr4di |
⊢ ( 𝑈 ∈ NrmCVec → 𝑊 = 〈 𝐺 , 𝑆 〉 ) |