Theorem ltmpq 5057

Description: Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of [Gleason] p. 120.

Hypotheses

Ref	Expression
ltapq.1	|- A e. V
ltapq.2	|- B e. V

Assertion

Ref	Expression
ltmpq	|- (C e. Q. -> (A <Q B <-> (C .Q A) <Q (C .Q B)))

Proof of Theorem ltmpq

Step	Hyp	Ref	Expression
1		ltapq.2	. 2 |- B e. V
2		dmmulpq 5041	. 2 |- dom .Q = (Q. X. Q.)
3		ltapq.1	. 2 |- A e. V
4		ltrelpq 5031	. 2 |- <Q (_ (Q. X. Q.)
5		0npq 5030	. 2 |- -. (/) e. Q.
6		df-nq 5018	. . 3 |- Q. = ((N. X. N.)/. ~Q )
7		breq1 2617	. . . 4 |- ([<.x, y>.] ~Q = A -> ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> A <Q [<.z, w>.] ~Q ))
8		opreq2 3960	. . . . 5 |- ([<.x, y>.] ~Q = A -> ([<.v, u>.] ~Q .Q [<.x, y>.] ~Q ) = ([<.v, u>.] ~Q .Q A))
9	8	breq1d 2624	. . . 4 |- ([<.x, y>.] ~Q = A -> (([<.v, u>.] ~Q .Q [<.x, y>.] ~Q ) <Q ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q ) <-> ([<.v, u>.] ~Q .Q A) <Q ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q )))
10	7, 9	bibi12d 628	. . 3 |- ([<.x, y>.] ~Q = A -> (([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> ([<.v, u>.] ~Q .Q [<.x, y>.] ~Q ) <Q ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q )) <-> (A <Q [<.z, w>.] ~Q <-> ([<.v, u>.] ~Q .Q A) <Q ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q ))))
11		breq2 2618	. . . 4 |- ([<.z, w>.] ~Q = B -> (A <Q [<.z, w>.] ~Q <-> A <Q B))
12		opreq2 3960	. . . . 5 |- ([<.z, w>.] ~Q = B -> ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q ) = ([<.v, u>.] ~Q .Q B))
13	12	breq2d 2625	. . . 4 |- ([<.z, w>.] ~Q = B -> (([<.v, u>.] ~Q .Q A) <Q ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q ) <-> ([<.v, u>.] ~Q .Q A) <Q ([<.v, u>.] ~Q .Q B)))
14	11, 13	bibi12d 628	. . 3 |- ([<.z, w>.] ~Q = B -> ((A <Q [<.z, w>.] ~Q <-> ([<.v, u>.] ~Q .Q A) <Q ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q )) <-> (A <Q B <-> ([<.v, u>.] ~Q .Q A) <Q ([<.v, u>.] ~Q .Q B))))
15		opreq1 3959	. . . . 5 |- ([<.v, u>.] ~Q = C -> ([<.v, u>.] ~Q .Q A) = (C .Q A))
16		opreq1 3959	. . . . 5 |- ([<.v, u>.] ~Q = C -> ([<.v, u>.] ~Q .Q B) = (C .Q B))
17	15, 16	breq12d 2626	. . . 4 |- ([<.v, u>.] ~Q = C -> (([<.v, u>.] ~Q .Q A) <Q ([<.v, u>.] ~Q .Q B) <-> (C .Q A) <Q (C .Q B)))
18	17	bibi2d 617	. . 3 |- ([<.v, u>.] ~Q = C -> ((A <Q B <-> ([<.v, u>.] ~Q .Q A) <Q ([<.v, u>.] ~Q .Q B)) <-> (A <Q B <-> (C .Q A) <Q (C .Q B))))
19		mulclpi 5001	. . . . . . . . 9 |- ((v e. N. /\ u e. N.) -> (v .N u) e. N.)
20		oprex 3974	. . . . . . . . . . 11 |- (x .N w) e. V
21		oprex 3974	. . . . . . . . . . 11 |- (y .N z) e. V
22	20, 21	ltmpi 5011	. . . . . . . . . 10 |- ((v .N u) e. N. -> ((x .N w) <N (y .N z) <-> ((v .N u) .N (x .N w)) <N ((v .N u) .N (y .N z))))
23		visset 1809	. . . . . . . . . . . 12 |- v e. V
24		visset 1809	. . . . . . . . . . . 12 |- x e. V
25		visset 1809	. . . . . . . . . . . 12 |- u e. V
26		visset 1809	. . . . . . . . . . . . 13 |- f e. V
27		visset 1809	. . . . . . . . . . . . 13 |- g e. V
28	26, 27	mulcompi 5004	. . . . . . . . . . . 12 |- (f .N g) = (g .N f)
29		visset 1809	. . . . . . . . . . . . 13 |- h e. V
30	27, 29	mulasspi 5005	. . . . . . . . . . . 12 |- ((f .N g) .N h) = (f .N (g .N h))
31		visset 1809	. . . . . . . . . . . 12 |- w e. V
32	23, 24, 25, 28, 30, 31	caopr4 4056	. . . . . . . . . . 11 |- ((v .N x) .N (u .N w)) = ((v .N u) .N (x .N w))
33		visset 1809	. . . . . . . . . . . . 13 |- y e. V
34		visset 1809	. . . . . . . . . . . . 13 |- z e. V
35	25, 33, 23, 28, 30, 34	caopr4 4056	. . . . . . . . . . . 12 |- ((u .N y) .N (v .N z)) = ((u .N v) .N (y .N z))
36	25, 23	mulcompi 5004	. . . . . . . . . . . . 13 |- (u .N v) = (v .N u)
37	36	opreq1i 3962	. . . . . . . . . . . 12 |- ((u .N v) .N (y .N z)) = ((v .N u) .N (y .N z))
38	35, 37	eqtr 1492	. . . . . . . . . . 11 |- ((u .N y) .N (v .N z)) = ((v .N u) .N (y .N z))
39	32, 38	breq12i 2623	. . . . . . . . . 10 |- (((v .N x) .N (u .N w)) <N ((u .N y) .N (v .N z)) <-> ((v .N u) .N (x .N w)) <N ((v .N u) .N (y .N z)))
40	22, 39	syl6bbr 537	. . . . . . . . 9 |- ((v .N u) e. N. -> ((x .N w) <N (y .N z) <-> ((v .N x) .N (u .N w)) <N ((u .N y) .N (v .N z))))
41	19, 40	syl 10	. . . . . . . 8 |- ((v e. N. /\ u e. N.) -> ((x .N w) <N (y .N z) <-> ((v .N x) .N (u .N w)) <N ((u .N y) .N (v .N z))))
42	24, 33, 34, 31	ordpipq 5036	. . . . . . . 8 |- ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> (x .N w) <N (y .N z))
43		oprex 3974	. . . . . . . . 9 |- (v .N x) e. V
44		oprex 3974	. . . . . . . . 9 |- (u .N y) e. V
45		oprex 3974	. . . . . . . . 9 |- (v .N z) e. V
46		oprex 3974	. . . . . . . . 9 |- (u .N w) e. V
47	43, 44, 45, 46	ordpipq 5036	. . . . . . . 8 |- ([<.(v .N x), (u .N y)>.] ~Q <Q [<.(v .N z), (u .N w)>.] ~Q <-> ((v .N x) .N (u .N w)) <N ((u .N y) .N (v .N z)))
48	41, 42, 47	3bitr4g 554	. . . . . . 7 |- ((v e. N. /\ u e. N.) -> ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> [<.(v .N x), (u .N y)>.] ~Q <Q [<.(v .N z), (u .N w)>.] ~Q ))
49	48	adantr 389	. . . . . 6 |- (((v e. N. /\ u e. N.) /\ ((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.))) -> ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> [<.(v .N x), (u .N y)>.] ~Q <Q [<.(v .N z), (u .N w)>.] ~Q ))
50		mulpipq 5035	. . . . . . . 8 |- (((v e. N. /\ u e. N.) /\ (x e. N. /\ y e. N.)) -> ([<.v, u>.] ~Q .Q [<.x, y>.] ~Q ) = [<.(v .N x), (u .N y)>.] ~Q )
51	50	adantrr 395	. . . . . . 7 |- (((v e. N. /\ u e. N.) /\ ((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.))) -> ([<.v, u>.] ~Q .Q [<.x, y>.] ~Q ) = [<.(v .N x), (u .N y)>.] ~Q )
52		mulpipq 5035	. . . . . . . 8 |- (((v e. N. /\ u e. N.) /\ (z e. N. /\ w e. N.)) -> ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q ) = [<.(v .N z), (u .N w)>.] ~Q )
53	52	adantrl 394	. . . . . . 7 |- (((v e. N. /\ u e. N.) /\ ((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.))) -> ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q ) = [<.(v .N z), (u .N w)>.] ~Q )
54	51, 53	breq12d 2626	. . . . . 6 |- (((v e. N. /\ u e. N.) /\ ((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.))) -> (([<.v, u>.] ~Q .Q [<.x, y>.] ~Q ) <Q ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q ) <-> [<.(v .N x), (u .N y)>.] ~Q <Q [<.(v .N z), (u .N w)>.] ~Q ))
55	49, 54	bitr4d 530	. . . . 5 |- (((v e. N. /\ u e. N.) /\ ((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.))) -> ([<.x, y>.] ~Q <Q [<.z, w>.] ~Q <-> ([<.v, u>.] ~Q .Q [<.x, y>.] ~Q ) <Q ([<.v, u>.] ~Q .Q [<.z, w>.] ~Q )