Step |
Hyp |
Ref |
Expression |
1 |
|
vciOLD.1 |
⊢ 𝐺 = ( 1st ‘ 𝑊 ) |
2 |
|
vciOLD.2 |
⊢ 𝑆 = ( 2nd ‘ 𝑊 ) |
3 |
|
vciOLD.3 |
⊢ 𝑋 = ran 𝐺 |
4 |
1 2 3
|
vcidOLD |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 ) |
5 |
4 4
|
oveq12d |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) = ( 𝐴 𝐺 𝐴 ) ) |
6 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
7 |
6
|
oveq1i |
⊢ ( 2 𝑆 𝐴 ) = ( ( 1 + 1 ) 𝑆 𝐴 ) |
8 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
9 |
1 2 3
|
vcdir |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 1 + 1 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) ) |
10 |
8 9
|
mp3anr1 |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 1 + 1 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) ) |
11 |
8 10
|
mpanr1 |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 + 1 ) 𝑆 𝐴 ) = ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) ) |
12 |
7 11
|
eqtr2id |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 𝑆 𝐴 ) 𝐺 ( 1 𝑆 𝐴 ) ) = ( 2 𝑆 𝐴 ) ) |
13 |
5 12
|
eqtr3d |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐴 ) = ( 2 𝑆 𝐴 ) ) |