Step |
Hyp |
Ref |
Expression |
1 |
|
ipcl.1 |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
2 |
|
ipcl.7 |
⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 ) |
3 |
|
fveq2 |
⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = ( ∗ ‘ 0 ) ) |
4 |
|
cj0 |
⊢ ( ∗ ‘ 0 ) = 0 |
5 |
3 4
|
eqtrdi |
⊢ ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = 0 ) |
6 |
1 2
|
dipcj |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = ( 𝐵 𝑃 𝐴 ) ) |
7 |
6
|
eqeq1d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = 0 ↔ ( 𝐵 𝑃 𝐴 ) = 0 ) ) |
8 |
5 7
|
syl5ib |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑃 𝐵 ) = 0 → ( 𝐵 𝑃 𝐴 ) = 0 ) ) |
9 |
|
fveq2 |
⊢ ( ( 𝐵 𝑃 𝐴 ) = 0 → ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = ( ∗ ‘ 0 ) ) |
10 |
9 4
|
eqtrdi |
⊢ ( ( 𝐵 𝑃 𝐴 ) = 0 → ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = 0 ) |
11 |
1 2
|
dipcj |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = ( 𝐴 𝑃 𝐵 ) ) |
12 |
11
|
3com23 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = ( 𝐴 𝑃 𝐵 ) ) |
13 |
12
|
eqeq1d |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = 0 ↔ ( 𝐴 𝑃 𝐵 ) = 0 ) ) |
14 |
10 13
|
syl5ib |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐵 𝑃 𝐴 ) = 0 → ( 𝐴 𝑃 𝐵 ) = 0 ) ) |
15 |
8 14
|
impbid |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑃 𝐵 ) = 0 ↔ ( 𝐵 𝑃 𝐴 ) = 0 ) ) |