Metamath Proof Explorer

Theorem crosspval

Description: Value of the cross product of two 3-dimensional real coordinate vectors as a function on ( 1 ... 3 ) . (Contributed by Jiamin Zhao, 31-Jul-2026)

Ref Expression
Assertion 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 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ ( 𝑢 = 𝐴 → ( 𝑢 ‘ 2 ) = ( 𝐴 ‘ 2 ) )
2 1 oveq1d ⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) = ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) )
3 fveq1 ⊢ ( 𝑢 = 𝐴 → ( 𝑢 ‘ 3 ) = ( 𝐴 ‘ 3 ) )
4 3 oveq1d ⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) = ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) )
5 2 4 oveq12d ⊢ ( 𝑢 = 𝐴 → ( ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) = ( ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) )
6 3 oveq1d ⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) = ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) )
7 fveq1 ⊢ ( 𝑢 = 𝐴 → ( 𝑢 ‘ 1 ) = ( 𝐴 ‘ 1 ) )
8 7 oveq1d ⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) = ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) )
9 6 8 oveq12d ⊢ ( 𝑢 = 𝐴 → ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) = ( ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) )
10 7 oveq1d ⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) = ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) )
11 1 oveq1d ⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) = ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) )
12 10 11 oveq12d ⊢ ( 𝑢 = 𝐴 → ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) )
13 9 12 ifeq12d ⊢ ( 𝑢 = 𝐴 → if ( 𝑘 = 2 , ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) = if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) )
14 5 13 ifeq12d ⊢ ( 𝑢 = 𝐴 → if ( 𝑘 = 1 , ( ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) ) = if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) ) )
15 14 mpteq2dv ⊢ ( 𝑢 = 𝐴 → ( 𝑘 ∈ ( 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 ) ) ) ) ) ) )
16 fveq1 ⊢ ( 𝑣 = 𝐵 → ( 𝑣 ‘ 3 ) = ( 𝐵 ‘ 3 ) )
17 16 oveq2d ⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) = ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) )
18 fveq1 ⊢ ( 𝑣 = 𝐵 → ( 𝑣 ‘ 2 ) = ( 𝐵 ‘ 2 ) )
19 18 oveq2d ⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) = ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) )
20 17 19 oveq12d ⊢ ( 𝑣 = 𝐵 → ( ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) = ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) )
21 fveq1 ⊢ ( 𝑣 = 𝐵 → ( 𝑣 ‘ 1 ) = ( 𝐵 ‘ 1 ) )
22 21 oveq2d ⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) = ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) )
23 16 oveq2d ⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) = ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) )
24 22 23 oveq12d ⊢ ( 𝑣 = 𝐵 → ( ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) = ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) )
25 18 oveq2d ⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) = ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) )
26 21 oveq2d ⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) = ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) )
27 25 26 oveq12d ⊢ ( 𝑣 = 𝐵 → ( ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) = ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) )
28 24 27 ifeq12d ⊢ ( 𝑣 = 𝐵 → if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) = if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) )
29 20 28 ifeq12d ⊢ ( 𝑣 = 𝐵 → if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) ) = if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) )
30 29 mpteq2dv ⊢ ( 𝑣 = 𝐵 → ( 𝑘 ∈ ( 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 ) ) ) ) ) ) )
31 df-crossp ⊢ ⊠ = ( 𝑢 ∈ ( ℝ ↑m ( 1 ... 3 ) ) , 𝑣 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ↦ ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 3 ) ) − ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝑢 ‘ 3 ) · ( 𝑣 ‘ 1 ) ) − ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 3 ) ) ) , ( ( ( 𝑢 ‘ 1 ) · ( 𝑣 ‘ 2 ) ) − ( ( 𝑢 ‘ 2 ) · ( 𝑣 ‘ 1 ) ) ) ) ) ) )
32 ovex ⊢ ( 1 ... 3 ) ∈ V
33 32 mptex ⊢ ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) ∈ V
34 15 30 31 33 ovmpo ⊢ ( ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ∧ 𝐵 ∈ ( ℝ ↑m ( 1 ... 3 ) ) ) → ( 𝐴 ⊠ 𝐵 ) = ( 𝑘 ∈ ( 1 ... 3 ) ↦ if ( 𝑘 = 1 , ( ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 3 ) ) − ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 2 ) ) ) , if ( 𝑘 = 2 , ( ( ( 𝐴 ‘ 3 ) · ( 𝐵 ‘ 1 ) ) − ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 3 ) ) ) , ( ( ( 𝐴 ‘ 1 ) · ( 𝐵 ‘ 2 ) ) − ( ( 𝐴 ‘ 2 ) · ( 𝐵 ‘ 1 ) ) ) ) ) ) )