Theorem crosspcle1d

Description: Closure of the first component of the cross product's coordinate formula. (Contributed by Jiamin Zhao, 11-Aug-2026)

	Ref	Expression
Hypotheses	crosspcled.1	|- ( ph -> A e. ( RR ^m ( 1 ... 3 ) ) )
	crosspcled.2	|- ( ph -> B e. ( RR ^m ( 1 ... 3 ) ) )
Assertion	crosspcle1d	|- ( ph -> ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		crosspcled.1	|- ( ph -> A e. ( RR ^m ( 1 ... 3 ) ) )
2		crosspcled.2	|- ( ph -> B e. ( RR ^m ( 1 ... 3 ) ) )
3	1	rr3fv2cld	|- ( ph -> ( A ` 2 ) e. RR )
4	2	rr3fv3cld	|- ( ph -> ( B ` 3 ) e. RR )
5	3 4	remulcld	|- ( ph -> ( ( A ` 2 ) x. ( B ` 3 ) ) e. RR )
6	1	rr3fv3cld	|- ( ph -> ( A ` 3 ) e. RR )
7	2	rr3fv2cld	|- ( ph -> ( B ` 2 ) e. RR )
8	6 7	remulcld	|- ( ph -> ( ( A ` 3 ) x. ( B ` 2 ) ) e. RR )
9	5 8	resubcld	|- ( ph -> ( ( ( A ` 2 ) x. ( B ` 3 ) ) - ( ( A ` 3 ) x. ( B ` 2 ) ) ) e. RR )