lterpq

Description: Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	lterpq	⊢ ( 𝐴 <_pQ 𝐵 ↔ ( [Q] ‘ 𝐴 ) <_Q ( [Q] ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ltpq	⊢ <_pQ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) <_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) }
2		opabssxp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) <_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) } ⊆ ( ( N × N ) × ( N × N ) )
3	1 2	eqsstri	⊢ <_pQ ⊆ ( ( N × N ) × ( N × N ) )
4	3	brel	⊢ ( 𝐴 <_pQ 𝐵 → ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) )
5		ltrelnq	⊢ <_Q ⊆ ( Q × Q )
6	5	brel	⊢ ( ( [Q] ‘ 𝐴 ) <_Q ( [Q] ‘ 𝐵 ) → ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ) )
7		elpqn	⊢ ( ( [Q] ‘ 𝐴 ) ∈ Q → ( [Q] ‘ 𝐴 ) ∈ ( N × N ) )
8		elpqn	⊢ ( ( [Q] ‘ 𝐵 ) ∈ Q → ( [Q] ‘ 𝐵 ) ∈ ( N × N ) )
9		nqerf	⊢ [Q] : ( N × N ) ⟶ Q
10	9	fdmi	⊢ dom [Q] = ( N × N )
11		0nelxp	⊢ ¬ ∅ ∈ ( N × N )
12	10 11	ndmfvrcl	⊢ ( ( [Q] ‘ 𝐴 ) ∈ ( N × N ) → 𝐴 ∈ ( N × N ) )
13	10 11	ndmfvrcl	⊢ ( ( [Q] ‘ 𝐵 ) ∈ ( N × N ) → 𝐵 ∈ ( N × N ) )
14	12 13	anim12i	⊢ ( ( ( [Q] ‘ 𝐴 ) ∈ ( N × N ) ∧ ( [Q] ‘ 𝐵 ) ∈ ( N × N ) ) → ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) )
15	7 8 14	syl2an	⊢ ( ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ) → ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) )
16	6 15	syl	⊢ ( ( [Q] ‘ 𝐴 ) <_Q ( [Q] ‘ 𝐵 ) → ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) )
17		xp1st	⊢ ( 𝐴 ∈ ( N × N ) → ( 1^st ‘ 𝐴 ) ∈ N )
18		xp2nd	⊢ ( 𝐵 ∈ ( N × N ) → ( 2^nd ‘ 𝐵 ) ∈ N )
19		mulclpi	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ N ∧ ( 2^nd ‘ 𝐵 ) ∈ N ) → ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ∈ N )
20	17 18 19	syl2an	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ∈ N )
21		ltmpi	⊢ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ∈ N → ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) <_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ↔ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) <_N ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) ) )
22	20 21	syl	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) <_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ↔ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) <_N ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) ) )
23		nqercl	⊢ ( 𝐴 ∈ ( N × N ) → ( [Q] ‘ 𝐴 ) ∈ Q )
24		nqercl	⊢ ( 𝐵 ∈ ( N × N ) → ( [Q] ‘ 𝐵 ) ∈ Q )
25		ordpinq	⊢ ( ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ) → ( ( [Q] ‘ 𝐴 ) <_Q ( [Q] ‘ 𝐵 ) ↔ ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) <_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) )
26	23 24 25	syl2an	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) <_Q ( [Q] ‘ 𝐵 ) ↔ ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) <_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) )
27		1st2nd2	⊢ ( 𝐴 ∈ ( N × N ) → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
28		1st2nd2	⊢ ( 𝐵 ∈ ( N × N ) → 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ )
29	27 28	breqan12d	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 <_pQ 𝐵 ↔ ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ <_pQ ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ) )
30		ordpipq	⊢ ( ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ <_pQ ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) )
31	29 30	syl6bb	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 <_pQ 𝐵 ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
32		xp1st	⊢ ( ( [Q] ‘ 𝐴 ) ∈ ( N × N ) → ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ∈ N )
33	23 7 32	3syl	⊢ ( 𝐴 ∈ ( N × N ) → ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ∈ N )
34		xp2nd	⊢ ( ( [Q] ‘ 𝐵 ) ∈ ( N × N ) → ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ∈ N )
35	24 8 34	3syl	⊢ ( 𝐵 ∈ ( N × N ) → ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ∈ N )
36		mulclpi	⊢ ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ∈ N ∧ ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ∈ N ) → ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ∈ N )
37	33 35 36	syl2an	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ∈ N )
38		ltmpi	⊢ ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ∈ N → ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ↔ ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) <_N ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ) )
39	37 38	syl	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) <_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ↔ ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) <_N ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ) )
40		mulcompi	⊢ ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) )
41	40	a1i	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) )
42		nqerrel	⊢ ( 𝐴 ∈ ( N × N ) → 𝐴 ~_Q ( [Q] ‘ 𝐴 ) )
43	23 7	syl	⊢ ( 𝐴 ∈ ( N × N ) → ( [Q] ‘ 𝐴 ) ∈ ( N × N ) )
44		enqbreq2	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐴 ) ∈ ( N × N ) ) → ( 𝐴 ~_Q ( [Q] ‘ 𝐴 ) ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) = ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
45	43 44	mpdan	⊢ ( 𝐴 ∈ ( N × N ) → ( 𝐴 ~_Q ( [Q] ‘ 𝐴 ) ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) = ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
46	42 45	mpbid	⊢ ( 𝐴 ∈ ( N × N ) → ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) = ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ 𝐴 ) ) )
47	46	eqcomd	⊢ ( 𝐴 ∈ ( N × N ) → ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ 𝐴 ) ) = ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) )
48		nqerrel	⊢ ( 𝐵 ∈ ( N × N ) → 𝐵 ~_Q ( [Q] ‘ 𝐵 ) )
49	24 8	syl	⊢ ( 𝐵 ∈ ( N × N ) → ( [Q] ‘ 𝐵 ) ∈ ( N × N ) )
50		enqbreq2	⊢ ( ( 𝐵 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐵 ) ∈ ( N × N ) ) → ( 𝐵 ~_Q ( [Q] ‘ 𝐵 ) ↔ ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) = ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ 𝐵 ) ) ) )
51	49 50	mpdan	⊢ ( 𝐵 ∈ ( N × N ) → ( 𝐵 ~_Q ( [Q] ‘ 𝐵 ) ↔ ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) = ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ 𝐵 ) ) ) )
52	48 51	mpbid	⊢ ( 𝐵 ∈ ( N × N ) → ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) = ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ 𝐵 ) ) )
53	47 52	oveqan12d	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ 𝐴 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ 𝐵 ) ) ) )
54		mulcompi	⊢ ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) = ( ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) )
55		fvex	⊢ ( 1^st ‘ 𝐵 ) ∈ V
56		fvex	⊢ ( 2^nd ‘ 𝐴 ) ∈ V
57		fvex	⊢ ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ∈ V
58		mulcompi	⊢ ( 𝑥 ·_N 𝑦 ) = ( 𝑦 ·_N 𝑥 )
59		mulasspi	⊢ ( ( 𝑥 ·_N 𝑦 ) ·_N 𝑧 ) = ( 𝑥 ·_N ( 𝑦 ·_N 𝑧 ) )
60		fvex	⊢ ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ∈ V
61	55 56 57 58 59 60	caov411	⊢ ( ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) = ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ 𝐴 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) )
62	54 61	eqtri	⊢ ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) = ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ 𝐴 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) )
63		mulcompi	⊢ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) = ( ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) )
64		fvex	⊢ ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ∈ V
65		fvex	⊢ ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ∈ V
66		fvex	⊢ ( 1^st ‘ 𝐴 ) ∈ V
67		fvex	⊢ ( 2^nd ‘ 𝐵 ) ∈ V
68	64 65 66 58 59 67	caov411	⊢ ( ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ 𝐵 ) ) )
69	63 68	eqtri	⊢ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ 𝐵 ) ) )
70	53 62 69	3eqtr4g	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) )
71	41 70	breq12d	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) <_N ( ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ↔ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) <_N ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) ) )
72	31 39 71	3bitrd	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 <_pQ 𝐵 ↔ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐴 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) <_N ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ ( [Q] ‘ 𝐵 ) ) ·_N ( 2^nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) ) )
73	22 26 72	3bitr4rd	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 <_pQ 𝐵 ↔ ( [Q] ‘ 𝐴 ) <_Q ( [Q] ‘ 𝐵 ) ) )
74	4 16 73	pm5.21nii	⊢ ( 𝐴 <_pQ 𝐵 ↔ ( [Q] ‘ 𝐴 ) <_Q ( [Q] ‘ 𝐵 ) )

Metamath Proof Explorer

Theorem lterpq

Proof