Step |
Hyp |
Ref |
Expression |
1 |
|
nvmval.1 |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
2 |
|
nvmval.2 |
⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) |
3 |
|
nvmval.4 |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
4 |
|
nvmval.3 |
⊢ 𝑀 = ( −𝑣 ‘ 𝑈 ) |
5 |
1 2 3 4
|
nvmval |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) |
6 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
7 |
1 3
|
nvscl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) |
8 |
6 7
|
mp3an2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) |
9 |
8
|
3adant2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) |
10 |
1 2
|
nvcom |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) = ( ( - 1 𝑆 𝐵 ) 𝐺 𝐴 ) ) |
11 |
9 10
|
syld3an3 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) = ( ( - 1 𝑆 𝐵 ) 𝐺 𝐴 ) ) |
12 |
5 11
|
eqtrd |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( ( - 1 𝑆 𝐵 ) 𝐺 𝐴 ) ) |