Metamath Proof Explorer

Theorem crosspcli

Description: Closure of the cross product: the cross product of two 3-dimensional real coordinate vectors is again such a vector. (Contributed by Jiamin Zhao, 31-Jul-2026)

Ref Expression
Hypotheses crossp.1 ⊢ 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) )
crossp.2 ⊢ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) )
Assertion crosspcli ( 𝐴 ⊠ 𝐵 ) ∈ ( ℝ ↑m ( 1 ... 3 ) )

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 1 2 crosspclifi ⊢ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ∈ ℝ
6 5 a1i ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝑘 ∈ ( 1 ... 3 ) ) → if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ∈ ℝ )
7 6 fmpttd ⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) : ( 1 ... 3 ) ⟶ ℝ )
8 1 7 ax-mp ⊢ ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) : ( 1 ... 3 ) ⟶ ℝ
9 reex ⊢ ℝ ∈ V
10 ovex ⊢ ( 1 ... 3 ) ∈ V
11 9 10 elmap ⊢ ( ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↔ ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) : ( 1 ... 3 ) ⟶ ℝ )
12 8 11 mpbir ⊢ ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) ∈ ( ℝ ↑m ( 1 ... 3 ) )
13 4 12 eqeltri ⊢ ( 𝐴 ⊠ 𝐵 ) ∈ ( ℝ ↑m ( 1 ... 3 ) )