Metamath Proof Explorer

Theorem crosspv3i

Description: Value of the third component of the cross product. (Contributed by Jiamin Zhao, 31-Jul-2026)

Ref Expression
Hypotheses crossp.1 ⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) )
crossp.2 ⊢ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) )
Assertion crosspv3i ( ( 𝐴 ⊠ 𝐵 ) ‘ 3 ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) )

Proof

Step Hyp Ref Expression
1 crossp.1 ⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) )
2 crossp.2 ⊢ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) )
3 crosspval ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( 𝐴 ⊠ 𝐵 ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) )
4 1 2 3 mp2an ⊢ ( 𝐴 ⊠ 𝐵 ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) )
5 4 fveq1i ⊢ ( ( 𝐴 ⊠ 𝐵 ) ‘ 3 ) = ( ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) ‘ 3 )
6 3elfz13 ⊢ 3 ∈ ( 1 ... 3 )
7 1 2 crosspcle3i ⊢ ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ∈ ℝ
8 id ⊢ ( 𝑘 = 1 → 𝑘 = 1 )
9 1ne3 ⊢ 1 ≠ 3
10 9 a1i ⊢ ( 𝑘 = 1 → 1 ≠ 3 )
11 8 10 eqnetrd ⊢ ( 𝑘 = 1 → 𝑘 ≠ 3 )
12 11 necon2bi ⊢ ( 𝑘 = 3 → ¬ 𝑘 = 1 )
13 12 iffalsed ⊢ ( 𝑘 = 3 → if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) = if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) )
14 id ⊢ ( 𝑘 = 2 → 𝑘 = 2 )
15 2ne3 ⊢ 2 ≠ 3
16 15 a1i ⊢ ( 𝑘 = 2 → 2 ≠ 3 )
17 14 16 eqnetrd ⊢ ( 𝑘 = 2 → 𝑘 ≠ 3 )
18 17 necon2bi ⊢ ( 𝑘 = 3 → ¬ 𝑘 = 2 )
19 18 iffalsed ⊢ ( 𝑘 = 3 → if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) )
20 13 19 eqtrd ⊢ ( 𝑘 = 3 → if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) )
21 eqid ⊢ ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) )
22 20 21 fvmptg ⊢ ( ( 3 ∈ ( 1 ... 3 ) ∧ ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ∈ ℝ ) → ( ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) ‘ 3 ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) )
23 6 7 22 mp2an ⊢ ( ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) ‘ 3 ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) )
24 5 23 eqtri ⊢ ( ( 𝐴 ⊠ 𝐵 ) ‘ 3 ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) )