Step |
Hyp |
Ref |
Expression |
1 |
|
phop.2 |
⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) |
2 |
|
phop.4 |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
3 |
|
phop.6 |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
4 |
|
phrel |
⊢ Rel CPreHilOLD |
5 |
|
1st2nd |
⊢ ( ( Rel CPreHilOLD ∧ 𝑈 ∈ CPreHilOLD ) → 𝑈 = 〈 ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) 〉 ) |
6 |
4 5
|
mpan |
⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 = 〈 ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) 〉 ) |
7 |
3
|
nmcvfval |
⊢ 𝑁 = ( 2nd ‘ 𝑈 ) |
8 |
7
|
opeq2i |
⊢ 〈 ( 1st ‘ 𝑈 ) , 𝑁 〉 = 〈 ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) 〉 |
9 |
|
phnv |
⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec ) |
10 |
|
eqid |
⊢ ( 1st ‘ 𝑈 ) = ( 1st ‘ 𝑈 ) |
11 |
10
|
nvvc |
⊢ ( 𝑈 ∈ NrmCVec → ( 1st ‘ 𝑈 ) ∈ CVecOLD ) |
12 |
|
vcrel |
⊢ Rel CVecOLD |
13 |
|
1st2nd |
⊢ ( ( Rel CVecOLD ∧ ( 1st ‘ 𝑈 ) ∈ CVecOLD ) → ( 1st ‘ 𝑈 ) = 〈 ( 1st ‘ ( 1st ‘ 𝑈 ) ) , ( 2nd ‘ ( 1st ‘ 𝑈 ) ) 〉 ) |
14 |
12 13
|
mpan |
⊢ ( ( 1st ‘ 𝑈 ) ∈ CVecOLD → ( 1st ‘ 𝑈 ) = 〈 ( 1st ‘ ( 1st ‘ 𝑈 ) ) , ( 2nd ‘ ( 1st ‘ 𝑈 ) ) 〉 ) |
15 |
1
|
vafval |
⊢ 𝐺 = ( 1st ‘ ( 1st ‘ 𝑈 ) ) |
16 |
2
|
smfval |
⊢ 𝑆 = ( 2nd ‘ ( 1st ‘ 𝑈 ) ) |
17 |
15 16
|
opeq12i |
⊢ 〈 𝐺 , 𝑆 〉 = 〈 ( 1st ‘ ( 1st ‘ 𝑈 ) ) , ( 2nd ‘ ( 1st ‘ 𝑈 ) ) 〉 |
18 |
14 17
|
eqtr4di |
⊢ ( ( 1st ‘ 𝑈 ) ∈ CVecOLD → ( 1st ‘ 𝑈 ) = 〈 𝐺 , 𝑆 〉 ) |
19 |
9 11 18
|
3syl |
⊢ ( 𝑈 ∈ CPreHilOLD → ( 1st ‘ 𝑈 ) = 〈 𝐺 , 𝑆 〉 ) |
20 |
19
|
opeq1d |
⊢ ( 𝑈 ∈ CPreHilOLD → 〈 ( 1st ‘ 𝑈 ) , 𝑁 〉 = 〈 〈 𝐺 , 𝑆 〉 , 𝑁 〉 ) |
21 |
8 20
|
eqtr3id |
⊢ ( 𝑈 ∈ CPreHilOLD → 〈 ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) 〉 = 〈 〈 𝐺 , 𝑆 〉 , 𝑁 〉 ) |
22 |
6 21
|
eqtrd |
⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 = 〈 〈 𝐺 , 𝑆 〉 , 𝑁 〉 ) |