Metamath Proof Explorer


Theorem xpord2lem

Description: Lemma for cross product ordering. Calculate the value of the cross product relationship. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis xpord2.1 T = x y | x A × B y A × B 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y 2 nd x = 2 nd y x y
Assertion xpord2lem a b T c d a A b B c A d B a R c a = c b S d b = d a c b d

Proof

Step Hyp Ref Expression
1 xpord2.1 T = x y | x A × B y A × B 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y 2 nd x = 2 nd y x y
2 opex a b V
3 opex c d V
4 eleq1 x = a b x A × B a b A × B
5 opelxp a b A × B a A b B
6 4 5 bitrdi x = a b x A × B a A b B
7 vex a V
8 vex b V
9 7 8 op1std x = a b 1 st x = a
10 9 breq1d x = a b 1 st x R 1 st y a R 1 st y
11 9 eqeq1d x = a b 1 st x = 1 st y a = 1 st y
12 10 11 orbi12d x = a b 1 st x R 1 st y 1 st x = 1 st y a R 1 st y a = 1 st y
13 7 8 op2ndd x = a b 2 nd x = b
14 13 breq1d x = a b 2 nd x S 2 nd y b S 2 nd y
15 13 eqeq1d x = a b 2 nd x = 2 nd y b = 2 nd y
16 14 15 orbi12d x = a b 2 nd x S 2 nd y 2 nd x = 2 nd y b S 2 nd y b = 2 nd y
17 neeq1 x = a b x y a b y
18 12 16 17 3anbi123d x = a b 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y 2 nd x = 2 nd y x y a R 1 st y a = 1 st y b S 2 nd y b = 2 nd y a b y
19 6 18 3anbi13d x = a b x A × B y A × B 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y 2 nd x = 2 nd y x y a A b B y A × B a R 1 st y a = 1 st y b S 2 nd y b = 2 nd y a b y
20 eleq1 y = c d y A × B c d A × B
21 opelxp c d A × B c A d B
22 20 21 bitrdi y = c d y A × B c A d B
23 vex c V
24 vex d V
25 23 24 op1std y = c d 1 st y = c
26 25 breq2d y = c d a R 1 st y a R c
27 25 eqeq2d y = c d a = 1 st y a = c
28 26 27 orbi12d y = c d a R 1 st y a = 1 st y a R c a = c
29 23 24 op2ndd y = c d 2 nd y = d
30 29 breq2d y = c d b S 2 nd y b S d
31 29 eqeq2d y = c d b = 2 nd y b = d
32 30 31 orbi12d y = c d b S 2 nd y b = 2 nd y b S d b = d
33 neeq2 y = c d a b y a b c d
34 7 8 opthne a b c d a c b d
35 33 34 bitrdi y = c d a b y a c b d
36 28 32 35 3anbi123d y = c d a R 1 st y a = 1 st y b S 2 nd y b = 2 nd y a b y a R c a = c b S d b = d a c b d
37 22 36 3anbi23d y = c d a A b B y A × B a R 1 st y a = 1 st y b S 2 nd y b = 2 nd y a b y a A b B c A d B a R c a = c b S d b = d a c b d
38 2 3 19 37 1 brab a b T c d a A b B c A d B a R c a = c b S d b = d a c b d