Step |
Hyp |
Ref |
Expression |
1 |
|
cnnvs.6 |
⊢ 𝑈 = 〈 〈 + , · 〉 , abs 〉 |
2 |
|
eqid |
⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 ) |
3 |
2
|
smfval |
⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( 2nd ‘ ( 1st ‘ 𝑈 ) ) |
4 |
1
|
fveq2i |
⊢ ( 1st ‘ 𝑈 ) = ( 1st ‘ 〈 〈 + , · 〉 , abs 〉 ) |
5 |
|
opex |
⊢ 〈 + , · 〉 ∈ V |
6 |
|
absf |
⊢ abs : ℂ ⟶ ℝ |
7 |
|
cnex |
⊢ ℂ ∈ V |
8 |
|
fex |
⊢ ( ( abs : ℂ ⟶ ℝ ∧ ℂ ∈ V ) → abs ∈ V ) |
9 |
6 7 8
|
mp2an |
⊢ abs ∈ V |
10 |
5 9
|
op1st |
⊢ ( 1st ‘ 〈 〈 + , · 〉 , abs 〉 ) = 〈 + , · 〉 |
11 |
4 10
|
eqtri |
⊢ ( 1st ‘ 𝑈 ) = 〈 + , · 〉 |
12 |
11
|
fveq2i |
⊢ ( 2nd ‘ ( 1st ‘ 𝑈 ) ) = ( 2nd ‘ 〈 + , · 〉 ) |
13 |
|
addex |
⊢ + ∈ V |
14 |
|
mulex |
⊢ · ∈ V |
15 |
13 14
|
op2nd |
⊢ ( 2nd ‘ 〈 + , · 〉 ) = · |
16 |
3 12 15
|
3eqtrri |
⊢ · = ( ·𝑠OLD ‘ 𝑈 ) |