Description: Closure of the second component of the cross product's Sarrus expansion. (A helper for crosspclifi and crosspv2i .) (Contributed by Jiamin Zhao, 31-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | crosspcle.1 | |- A e. ( RR ^m ( 1 ... 3 ) ) |
|
| crosspcle.2 | |- B e. ( RR ^m ( 1 ... 3 ) ) |
||
| Assertion | crosspcle2i | |- ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) e. RR |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | crosspcle.1 | |- A e. ( RR ^m ( 1 ... 3 ) ) |
|
| 2 | crosspcle.2 | |- B e. ( RR ^m ( 1 ... 3 ) ) |
|
| 3 | 1 | rr3fv3cli | |- ( A ` 3 ) e. RR |
| 4 | 2 | rr3fv1cli | |- ( B ` 1 ) e. RR |
| 5 | 3 4 | remulcli | |- ( ( A ` 3 ) x. ( B ` 1 ) ) e. RR |
| 6 | 1 | rr3fv1cli | |- ( A ` 1 ) e. RR |
| 7 | 2 | rr3fv3cli | |- ( B ` 3 ) e. RR |
| 8 | 6 7 | remulcli | |- ( ( A ` 1 ) x. ( B ` 3 ) ) e. RR |
| 9 | 5 8 | resubcli | |- ( ( ( A ` 3 ) x. ( B ` 1 ) ) - ( ( A ` 1 ) x. ( B ` 3 ) ) ) e. RR |