Theorem crosspv3i

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

	Ref	Expression
Hypotheses	crossp.1	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
	crossp.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
Assertion	crosspv3i	Could not format assertion : No typesetting found for |- ( ( A crossp B ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		crossp.1	$$⊢A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crossp.2	$$⊢B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3		crosspval	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 |-
4	1 2 3	mp2an	Could not format ( 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 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 |-
5	4	fveq1i	Could not format ( ( A crossp B ) ` 3 ) = ( ( 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 ) ) ) ) ) ) ` 3 ) : No typesetting found for |- ( ( A crossp B ) ` 3 ) = ( ( 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 ) ) ) ) ) ) ` 3 ) with typecode |-
6		3elfz13	$$⊢3\in \left(1\dots 3\right)$$
7	1 2	crosspcle3i	$$⊢A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)\in ℝ$$
8		id	$$⊢k=1\to k=1$$
9		1ne3	$$⊢1\ne 3$$
10	9	a1i	$$⊢k=1\to 1\ne 3$$
11	8 10	eqnetrd	$$⊢k=1\to k\ne 3$$
12	11	necon2bi	$$⊢k=3\to \neg k=1$$
13	12	iffalsed	$$⊢k=3\to 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)=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)$$
14		id	$$⊢k=2\to k=2$$
15		2ne3	$$⊢2\ne 3$$
16	15	a1i	$$⊢k=2\to 2\ne 3$$
17	14 16	eqnetrd	$$⊢k=2\to k\ne 3$$
18	17	necon2bi	$$⊢k=3\to \neg k=2$$
19	18	iffalsed	$$⊢k=3\to 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)=A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)$$
20	13 19	eqtrd	$$⊢k=3\to 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)=A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)$$
21		eqid	$$⊢\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)=\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)$$
22	20 21	fvmptg	$$⊢\left(3\in \left(1\dots 3\right)\wedge A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)\in ℝ\right)\to \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)\left(3\right)=A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)$$
23	6 7 22	mp2an	$$⊢\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)\left(3\right)=A\left(1\right)B\left(2\right)-A\left(2\right)B\left(1\right)$$
24	5 23	eqtri	Could not format ( ( A crossp B ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) : No typesetting found for |- ( ( A crossp B ) ` 3 ) = ( ( ( A ` 1 ) x. ( B ` 2 ) ) - ( ( A ` 2 ) x. ( B ` 1 ) ) ) with typecode |-