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	Could not format assertion : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ B e. ( RR ^m ( 1 ... 3 ) ) ) -> ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> if ( k = 1 , ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) , if ( k = 2 , ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fveq1	$$⊢u=A\to u\left(2\right)=A\left(2\right)$$
2	1	oveq1d	$$⊢u=A\to u\left(2\right)v\left(3\right)=A\left(2\right)v\left(3\right)$$
3		fveq1	$$⊢u=A\to u\left(3\right)=A\left(3\right)$$
4	3	oveq1d	$$⊢u=A\to u\left(3\right)v\left(2\right)=A\left(3\right)v\left(2\right)$$
5	2 4	oveq12d	$$⊢u=A\to u\left(2\right)v\left(3\right)-u\left(3\right)v\left(2\right)=A\left(2\right)v\left(3\right)-A\left(3\right)v\left(2\right)$$
6	3	oveq1d	$$⊢u=A\to u\left(3\right)v\left(1\right)=A\left(3\right)v\left(1\right)$$
7		fveq1	$$⊢u=A\to u\left(1\right)=A\left(1\right)$$
8	7	oveq1d	$$⊢u=A\to u\left(1\right)v\left(3\right)=A\left(1\right)v\left(3\right)$$
9	6 8	oveq12d	$$⊢u=A\to u\left(3\right)v\left(1\right)-u\left(1\right)v\left(3\right)=A\left(3\right)v\left(1\right)-A\left(1\right)v\left(3\right)$$
10	7	oveq1d	$$⊢u=A\to u\left(1\right)v\left(2\right)=A\left(1\right)v\left(2\right)$$
11	1	oveq1d	$$⊢u=A\to u\left(2\right)v\left(1\right)=A\left(2\right)v\left(1\right)$$
12	10 11	oveq12d	$$⊢u=A\to u\left(1\right)v\left(2\right)-u\left(2\right)v\left(1\right)=A\left(1\right)v\left(2\right)-A\left(2\right)v\left(1\right)$$
13	9 12	ifeq12d	$$⊢u=A\to if\left(k=2,u\left(3\right)v\left(1\right)-u\left(1\right)v\left(3\right),u\left(1\right)v\left(2\right)-u\left(2\right)v\left(1\right)\right)=if\left(k=2,A\left(3\right)v\left(1\right)-A\left(1\right)v\left(3\right),A\left(1\right)v\left(2\right)-A\left(2\right)v\left(1\right)\right)$$
14	5 13	ifeq12d	$$⊢u=A\to if\left(k=1,u\left(2\right)v\left(3\right)-u\left(3\right)v\left(2\right),if\left(k=2,u\left(3\right)v\left(1\right)-u\left(1\right)v\left(3\right),u\left(1\right)v\left(2\right)-u\left(2\right)v\left(1\right)\right)\right)=if\left(k=1,A\left(2\right)v\left(3\right)-A\left(3\right)v\left(2\right),if\left(k=2,A\left(3\right)v\left(1\right)-A\left(1\right)v\left(3\right),A\left(1\right)v\left(2\right)-A\left(2\right)v\left(1\right)\right)\right)$$
15	14	mpteq2dv	$$⊢u=A\to \left(k\in \left(1\dots 3\right)⟼if\left(k=1,u\left(2\right)v\left(3\right)-u\left(3\right)v\left(2\right),if\left(k=2,u\left(3\right)v\left(1\right)-u\left(1\right)v\left(3\right),u\left(1\right)v\left(2\right)-u\left(2\right)v\left(1\right)\right)\right)\right)=\left(k\in \left(1\dots 3\right)⟼if\left(k=1,A\left(2\right)v\left(3\right)-A\left(3\right)v\left(2\right),if\left(k=2,A\left(3\right)v\left(1\right)-A\left(1\right)v\left(3\right),A\left(1\right)v\left(2\right)-A\left(2\right)v\left(1\right)\right)\right)\right)$$
16		fveq1	$$⊢v=B\to v\left(3\right)=B\left(3\right)$$
17	16	oveq2d	$$⊢v=B\to A\left(2\right)v\left(3\right)=A\left(2\right)B\left(3\right)$$
18		fveq1	$$⊢v=B\to v\left(2\right)=B\left(2\right)$$
19	18	oveq2d	$$⊢v=B\to A\left(3\right)v\left(2\right)=A\left(3\right)B\left(2\right)$$
20	17 19	oveq12d	$$⊢v=B\to A\left(2\right)v\left(3\right)-A\left(3\right)v\left(2\right)=A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right)$$
21		fveq1	$$⊢v=B\to v\left(1\right)=B\left(1\right)$$
22	21	oveq2d	$$⊢v=B\to A\left(3\right)v\left(1\right)=A\left(3\right)B\left(1\right)$$
23	16	oveq2d	$$⊢v=B\to A\left(1\right)v\left(3\right)=A\left(1\right)B\left(3\right)$$
24	22 23	oveq12d	$$⊢v=B\to A\left(3\right)v\left(1\right)-A\left(1\right)v\left(3\right)=A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right)$$
25	18	oveq2d	$$⊢v=B\to A\left(1\right)v\left(2\right)=A\left(1\right)B\left(2\right)$$
26	21	oveq2d	$$⊢v=B\to A\left(2\right)v\left(1\right)=A\left(2\right)B\left(1\right)$$
27	25 26	oveq12d	$$⊢v=B\to A\left(1\right)v\left(2\right)-A\left(2\right)v\left(1\right)=A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)$$
28	24 27	ifeq12d	$$⊢v=B\to if\left(k=2,A\left(3\right)v\left(1\right)-A\left(1\right)v\left(3\right),A\left(1\right)v\left(2\right)-A\left(2\right)v\left(1\right)\right)=if\left(k=2,A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right),A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)\right)$$
29	20 28	ifeq12d	$$⊢v=B\to if\left(k=1,A\left(2\right)v\left(3\right)-A\left(3\right)v\left(2\right),if\left(k=2,A\left(3\right)v\left(1\right)-A\left(1\right)v\left(3\right),A\left(1\right)v\left(2\right)-A\left(2\right)v\left(1\right)\right)\right)=if\left(k=1,A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right),if\left(k=2,A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right),A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)\right)\right)$$
30	29	mpteq2dv	$$⊢v=B\to \left(k\in \left(1\dots 3\right)⟼if\left(k=1,A\left(2\right)v\left(3\right)-A\left(3\right)v\left(2\right),if\left(k=2,A\left(3\right)v\left(1\right)-A\left(1\right)v\left(3\right),A\left(1\right)v\left(2\right)-A\left(2\right)v\left(1\right)\right)\right)\right)=\left(k\in \left(1\dots 3\right)⟼if\left(k=1,A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right),if\left(k=2,A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right),A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)\right)\right)\right)$$
31		df-crossp	Could not format crossp = ( u e. ( RR ^m ( 1 ... 3 ) ) , v e. ( RR ^m ( 1 ... 3 ) ) |-> ( k e. ( 1 ... 3 ) |-> if ( k = 1 , ( ( ( u ` 2 ) x. ( v ` 3 ) ) - ( ( u ` 3 ) x. ( v ` 2 ) ) ) , if ( k = 2 , ( ( ( u ` 3 ) x. ( v ` 1 ) ) - ( ( u ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( u ` 1 ) x. ( v ` 2 ) ) - ( ( u ` 2 ) x. ( v ` 1 ) ) ) ) ) ) ) : No typesetting found for |- crossp = ( u e. ( RR ^m ( 1 ... 3 ) ) , v e. ( RR ^m ( 1 ... 3 ) ) |-> ( k e. ( 1 ... 3 ) |-> if ( k = 1 , ( ( ( u ` 2 ) x. ( v ` 3 ) ) - ( ( u ` 3 ) x. ( v ` 2 ) ) ) , if ( k = 2 , ( ( ( u ` 3 ) x. ( v ` 1 ) ) - ( ( u ` 1 ) x. ( v ` 3 ) ) ) , ( ( ( u ` 1 ) x. ( v ` 2 ) ) - ( ( u ` 2 ) x. ( v ` 1 ) ) ) ) ) ) ) with typecode |-
32		ovex	$$⊢\left(1\dots 3\right)\in \mathrm{V}$$
33	32	mptex	$$⊢\left(k\in \left(1\dots 3\right)⟼if\left(k=1,A\left(2\right)B\left(3\right)-A\left(3\right)B\left(2\right),if\left(k=2,A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right),A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)\right)\right)\right)\in \mathrm{V}$$
34	15 30 31 33	ovmpo	Could not format ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ B e. ( RR ^m ( 1 ... 3 ) ) ) -> ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> if ( k = 1 , ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) , if ( k = 2 , ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) ) ) ) : No typesetting found for |- ( ( A e. ( RR ^m ( 1 ... 3 ) ) /\ B e. ( RR ^m ( 1 ... 3 ) ) ) -> ( A crossp B ) = ( k e. ( 1 ... 3 ) |-> if ( k = 1 , ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) , if ( k = 2 , ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) , ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) ) ) ) ) with typecode |-