Step |
Hyp |
Ref |
Expression |
1 |
|
ipass.1 |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
2 |
|
ipass.4 |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
3 |
|
ipass.7 |
⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 ) |
4 |
|
3anrot |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) |
5 |
1 2 3
|
dipass |
⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐵 𝑆 𝐶 ) 𝑃 𝐴 ) = ( 𝐵 · ( 𝐶 𝑃 𝐴 ) ) ) |
6 |
4 5
|
sylan2b |
⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐵 𝑆 𝐶 ) 𝑃 𝐴 ) = ( 𝐵 · ( 𝐶 𝑃 𝐴 ) ) ) |
7 |
6
|
fveq2d |
⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ∗ ‘ ( ( 𝐵 𝑆 𝐶 ) 𝑃 𝐴 ) ) = ( ∗ ‘ ( 𝐵 · ( 𝐶 𝑃 𝐴 ) ) ) ) |
8 |
|
phnv |
⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec ) |
9 |
|
simpl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → 𝑈 ∈ NrmCVec ) |
10 |
1 2
|
nvscl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝑆 𝐶 ) ∈ 𝑋 ) |
11 |
10
|
3adant3r1 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝑆 𝐶 ) ∈ 𝑋 ) |
12 |
|
simpr1 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 ) |
13 |
1 3
|
dipcj |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐵 𝑆 𝐶 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ∗ ‘ ( ( 𝐵 𝑆 𝐶 ) 𝑃 𝐴 ) ) = ( 𝐴 𝑃 ( 𝐵 𝑆 𝐶 ) ) ) |
14 |
9 11 12 13
|
syl3anc |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ∗ ‘ ( ( 𝐵 𝑆 𝐶 ) 𝑃 𝐴 ) ) = ( 𝐴 𝑃 ( 𝐵 𝑆 𝐶 ) ) ) |
15 |
8 14
|
sylan |
⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ∗ ‘ ( ( 𝐵 𝑆 𝐶 ) 𝑃 𝐴 ) ) = ( 𝐴 𝑃 ( 𝐵 𝑆 𝐶 ) ) ) |
16 |
|
simpr2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ ℂ ) |
17 |
1 3
|
dipcl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐶 𝑃 𝐴 ) ∈ ℂ ) |
18 |
17
|
3com23 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐶 𝑃 𝐴 ) ∈ ℂ ) |
19 |
18
|
3adant3r2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐶 𝑃 𝐴 ) ∈ ℂ ) |
20 |
16 19
|
cjmuld |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ∗ ‘ ( 𝐵 · ( 𝐶 𝑃 𝐴 ) ) ) = ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ ( 𝐶 𝑃 𝐴 ) ) ) ) |
21 |
1 3
|
dipcj |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐶 𝑃 𝐴 ) ) = ( 𝐴 𝑃 𝐶 ) ) |
22 |
21
|
3com23 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐶 𝑃 𝐴 ) ) = ( 𝐴 𝑃 𝐶 ) ) |
23 |
22
|
3adant3r2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ∗ ‘ ( 𝐶 𝑃 𝐴 ) ) = ( 𝐴 𝑃 𝐶 ) ) |
24 |
23
|
oveq2d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ∗ ‘ 𝐵 ) · ( ∗ ‘ ( 𝐶 𝑃 𝐴 ) ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐴 𝑃 𝐶 ) ) ) |
25 |
20 24
|
eqtrd |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ∗ ‘ ( 𝐵 · ( 𝐶 𝑃 𝐴 ) ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐴 𝑃 𝐶 ) ) ) |
26 |
8 25
|
sylan |
⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ∗ ‘ ( 𝐵 · ( 𝐶 𝑃 𝐴 ) ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐴 𝑃 𝐶 ) ) ) |
27 |
7 15 26
|
3eqtr3d |
⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑃 ( 𝐵 𝑆 𝐶 ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐴 𝑃 𝐶 ) ) ) |