Step |
Hyp |
Ref |
Expression |
1 |
|
vc0.1 |
⊢ 𝐺 = ( 1st ‘ 𝑊 ) |
2 |
|
vc0.2 |
⊢ 𝑆 = ( 2nd ‘ 𝑊 ) |
3 |
|
vc0.3 |
⊢ 𝑋 = ran 𝐺 |
4 |
|
vc0.4 |
⊢ 𝑍 = ( GId ‘ 𝐺 ) |
5 |
1 3 4
|
vczcl |
⊢ ( 𝑊 ∈ CVecOLD → 𝑍 ∈ 𝑋 ) |
6 |
5
|
anim2i |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑊 ∈ CVecOLD ) → ( 𝐴 ∈ ℂ ∧ 𝑍 ∈ 𝑋 ) ) |
7 |
6
|
ancoms |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝑍 ∈ 𝑋 ) ) |
8 |
|
0cn |
⊢ 0 ∈ ℂ |
9 |
1 2 3
|
vcass |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝑍 ∈ 𝑋 ) ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) ) |
10 |
8 9
|
mp3anr2 |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝑍 ∈ 𝑋 ) ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) ) |
11 |
7 10
|
syldan |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) ) |
12 |
|
mul01 |
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 ) |
13 |
12
|
oveq1d |
⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = ( 0 𝑆 𝑍 ) ) |
14 |
1 2 3 4
|
vc0 |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝑍 ∈ 𝑋 ) → ( 0 𝑆 𝑍 ) = 𝑍 ) |
15 |
5 14
|
mpdan |
⊢ ( 𝑊 ∈ CVecOLD → ( 0 𝑆 𝑍 ) = 𝑍 ) |
16 |
13 15
|
sylan9eqr |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 · 0 ) 𝑆 𝑍 ) = 𝑍 ) |
17 |
15
|
oveq2d |
⊢ ( 𝑊 ∈ CVecOLD → ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) = ( 𝐴 𝑆 𝑍 ) ) |
18 |
17
|
adantr |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝑆 ( 0 𝑆 𝑍 ) ) = ( 𝐴 𝑆 𝑍 ) ) |
19 |
11 16 18
|
3eqtr3rd |
⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ) → ( 𝐴 𝑆 𝑍 ) = 𝑍 ) |