Theorem crosspv2d

Description: Value of the second component of the cross product. (Contributed by Jiamin Zhao, 12-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		crosspd.1	$$⊢\phi \to A\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
2		crosspd.2	$$⊢\phi \to B\in \left({ℝ}^{\left(1\dots 3\right)}\right)$$
3		id	$$⊢k=1\to k=1$$
4		1ne2	$$⊢1\ne 2$$
5	4	a1i	$$⊢k=1\to 1\ne 2$$
6	3 5	eqnetrd	$$⊢k=1\to k\ne 2$$
7	6	necon2bi	$$⊢k=2\to \neg k=1$$
8	7	iffalsed	$$⊢k=2\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)$$
9		iftrue	$$⊢k=2\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(3\right)B\left(1\right)-A\left(1\right)B\left(3\right)$$
10	8 9	eqtrd	$$⊢k=2\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(3\right)B\left(1\right)-A\left(1\right)B\left(3\right)$$
11		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 |-
12	1 2 11	syl2anc	Could not format ( ph -> ( 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 |- ( ph -> ( 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 |-
13		2elfz13	$$⊢2\in \left(1\dots 3\right)$$
14	13	a1i	$$⊢\phi \to 2\in \left(1\dots 3\right)$$
15	1 2	crosspcle2d	$$⊢\phi \to A\left(3\right)B\left(1\right)-A\left(1\right)B\left(3\right)\in ℝ$$
16	10 12 14 15	fvmptd4	Could not format ( ph -> ( ( A crossp B ) ` 2 ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) ) : No typesetting found for |- ( ph -> ( ( A crossp B ) ` 2 ) = ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) ) with typecode |-