Theorem mulgt0sr 4008

Description: The product of two positive signed reals is positive.

Hypotheses

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

Assertion

Ref	Expression
mulgt0sr	|- ((0R <R A /\ 0R <R B) -> 0R <R (A .R B))

Proof of Theorem mulgt0sr

Step	Hyp	Ref	Expression
1		mulgt0sr.1	. . . . 5 |- A e. V
2		ltrelsr 3974	. . . . 5 |- <R (_ (R. X. R.)
3	1, 2	brel 2459	. . . 4 |- (0R <R A -> (0R e. R. /\ A e. R.))
4	3	pm3.27d 262	. . 3 |- (0R <R A -> A e. R.)
5		mulgt0sr.2	. . . . 5 |- B e. V
6	5, 2	brel 2459	. . . 4 |- (0R <R B -> (0R e. R. /\ B e. R.))
7	6	pm3.27d 262	. . 3 |- (0R <R B -> B e. R.)
8	4, 7	anim12i 268	. 2 |- ((0R <R A /\ 0R <R B) -> (A e. R. /\ B e. R.))
9		df-nr 3961	. . 3 |- R. = ((P. X. P.)/. ~R )
10		breq2 2066	. . . . 5 |- ([<.x, y>.] ~R = A -> (0R <R [<.x, y>.] ~R <-> 0R <R A))
11	10	anbi1d 469	. . . 4 |- ([<.x, y>.] ~R = A -> ((0R <R [<.x, y>.] ~R /\ 0R <R [<.z, w>.] ~R ) <-> (0R <R A /\ 0R <R [<.z, w>.] ~R )))
12		opreq1 3006	. . . . 5 |- ([<.x, y>.] ~R = A -> ([<.x, y>.] ~R .R [<.z, w>.] ~R ) = (A .R [<.z, w>.] ~R ))
13	12	breq2d 2072	. . . 4 |- ([<.x, y>.] ~R = A -> (0R <R ([<.x, y>.] ~R .R [<.z, w>.] ~R ) <-> 0R <R (A .R [<.z, w>.] ~R )))
14	11, 13	imbi12d 474	. . 3 |- ([<.x, y>.] ~R = A -> (((0R <R [<.x, y>.] ~R /\ 0R <R [<.z, w>.] ~R ) -> 0R <R ([<.x, y>.] ~R .R [<.z, w>.] ~R )) <-> ((0R <R A /\ 0R <R [<.z, w>.] ~R ) -> 0R <R (A .R [<.z, w>.] ~R ))))
15		breq2 2066	. . . . 5 |- ([<.z, w>.] ~R = B -> (0R <R [<.z, w>.] ~R <-> 0R <R B))
16	15	anbi2d 468	. . . 4 |- ([<.z, w>.] ~R = B -> ((0R <R A /\ 0R <R [<.z, w>.] ~R ) <-> (0R <R A /\ 0R <R B)))
17		opreq2 3007	. . . . 5 |- ([<.z, w>.] ~R = B -> (A .R [<.z, w>.] ~R ) = (A .R B))
18	17	breq2d 2072	. . . 4 |- ([<.z, w>.] ~R = B -> (0R <R (A .R [<.z, w>.] ~R ) <-> 0R <R (A .R B)))
19	16, 18	imbi12d 474	. . 3 |- ([<.z, w>.] ~R = B -> (((0R <R A /\ 0R <R [<.z, w>.] ~R ) -> 0R <R (A .R [<.z, w>.] ~R )) <-> ((0R <R A /\ 0R <R B) -> 0R <R (A .R B))))
20		oprex 3018	. . . . . . . . . . . . . . . . . 18 |- ((x .P z) +P. (y .P w)) e. V
21		oprex 3018	. . . . . . . . . . . . . . . . . 18 |- (((x .P w) +P. (y .P z)) +P. (v .P u)) e. V
22	20, 21	addcanpr 3946	. . . . . . . . . . . . . . . . 17 |- (((v .P w) e. P. /\ ((x .P z) +P. (y .P w)) e. P.) -> (((v .P w) +P. ((x .P z) +P. (y .P w))) = ((v .P w) +P. (((x .P w) +P. (y .P z)) +P. (v .P u))) -> ((x .P z) +P. (y .P w)) = (((x .P w) +P. (y .P z)) +P. (v .P u))))
23		opreq12 3008	. . . . . . . . . . . . . . . . . . . 20 |- (((y +P. v) = x /\ (w +P. u) = z) -> ((y +P. v) .P (w +P. u)) = (x .P z))
24	23	opreq1d 3012	. . . . . . . . . . . . . . . . . . 19 |- (((y +P. v) = x /\ (w +P. u) = z) -> (((y +P. v) .P (w +P. u)) +P. ((y .P w) +P. (v .P w))) = ((x .P z) +P. ((y .P w) +P. (v .P w))))
25		opreq2 3007	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((w +P. u) = z -> (y .P (w +P. u)) = (y .P z))
26		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 |- w e. V
27		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 |- u e. V
28	26, 27	distrpr 3926	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y .P (w +P. u)) = ((y .P w) +P. (y .P u))
29	25, 28	syl5eqr 1138	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w +P. u) = z -> ((y .P w) +P. (y .P u)) = (y .P z))
30	29	opreq1d 3012	. . . . . . . . . . . . . . . . . . . . 21 |- ((w +P. u) = z -> (((y .P w) +P. (y .P u)) +P. ((v .P w) +P. (v .P u))) = ((y .P z) +P. ((v .P w) +P. (v .P u))))
31		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 |- y e. V
32		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . 24 |- v e. V
33		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- f e. V
34		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- g e. V
35	33, 34	mulcompr 3919	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f .P g) = (g .P f)
36		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- h e. V
37	34, 36	distrpr 3926	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f .P (g +P. h)) = ((f .P g) +P. (f .P h))
38	31, 32, 26, 35, 37	caoprdistrr 3081	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y +P. v) .P w) = ((y .P w) +P. (v .P w))
39	31, 32, 27, 35, 37	caoprdistrr 3081	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y +P. v) .P u) = ((y .P u) +P. (v .P u))
40	38, 39	opreq12i 3011	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y +P. v) .P w) +P. ((y +P. v) .P u)) = (((y .P w) +P. (v .P w)) +P. ((y .P u) +P. (v .P u)))
41	26, 27	distrpr 3926	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y +P. v) .P (w +P. u)) = (((y +P. v) .P w) +P. ((y +P. v) .P u))
42		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y .P w) e. V
43		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y .P u) e. V
44		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v .P w) e. V
45	33, 34	addcompr 3917	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f +P. g) = (g +P. f)
46	34, 36	addasspr 3918	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f +P. g) +P. h) = (f +P. (g +P. h))
47		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v .P u) e. V
48	42, 43, 44, 45, 46, 47	caopr4 3078	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y .P w) +P. (y .P u)) +P. ((v .P w) +P. (v .P u))) = (((y .P w) +P. (v .P w)) +P. ((y .P u) +P. (v .P u)))
49	40, 41, 48	3eqtr4 1126	. . . . . . . . . . . . . . . . . . . . 21 |- ((y +P. v) .P (w +P. u)) = (((y .P w) +P. (y .P u)) +P. ((v .P w) +P. (v .P u)))
50		oprex 3018	. . . . . . . . . . . . . . . . . . . . . 22 |- (y .P z) e. V
51	44, 50, 47, 45, 46	caopr12 3075	. . . . . . . . . . . . . . . . . . . . 21 |- ((v .P w) +P. ((y .P z) +P. (v .P u))) = ((y .P z) +P. ((v .P w) +P. (v .P u)))
52	30, 49, 51	3eqtr4g 1147	. . . . . . . . . . . . . . . . . . . 20 |- ((w +P. u) = z -> ((y +P. v) .P (w +P. u)) = ((v .P w) +P. ((y .P z) +P. (v .P u))))
53		opreq1 3006	. . . . . . . . . . . . . . . . . . . . 21 |- ((y +P. v) = x -> ((y +P. v) .P w) = (x .P w))
54	53, 38	syl5eqr 1138	. . . . . . . . . . . . . . . . . . . 20 |- ((y +P. v) = x -> ((y .P w) +P. (v .P w)) = (x .P w))
55	52, 54	opreqan12rd 3016	. . . . . . . . . . . . . . . . . . 19 |- (((y +P. v) = x /\ (w +P. u) = z) -> (((y +P. v) .P (w +P. u)) +P. ((y .P w) +P. (v .P w))) = (((v .P w) +P. ((y .P z) +P. (v .P u))) +P. (x .P w)))
56	24, 55	eqtr3d 1130	. . . . . . . . . . . . . . . . . 18 |- (((y +P. v) = x /\ (w +P. u) = z) -> ((x .P z) +P. ((y .P w) +P. (v .P w))) = (((v .P w) +P. ((y .P z) +P. (v .P u))) +P. (x .P w)))
57	42, 44	addasspr 3918	. . . . . . . . . . . . . . . . . . 19 |- (((x .P z) +P. (y .P w)) +P. (v .P w)) = ((x .P z) +P. ((y .P w) +P. (v .P w)))
58	20, 44	addcompr 3917	. . . . . . . . . . . . . . . . . . 19 |- (((x .P z) +P. (y .P w)) +P. (v .P w)) = ((v .P w) +P. ((x .P z) +P. (y .P w)))
59	57, 58	eqtr3 1121	. . . . . . . . . . . . . . . . . 18 |- ((x .P z) +P. ((y .P w) +P. (v .P w))) = ((v .P w) +P. ((x .P z) +P. (y .P w)))
60		oprex 3018	. . . . . . . . . . . . . . . . . . . 20 |- (x .P w) e. V
61		oprex 3018	. . . . . . . . . . . . . . . . . . . 20 |- ((y .P z) +P. (v .P u)) e. V
62	60, 61	addasspr 3918	. . . . . . . . . . . . . . . . . . 19 |- (((v .P w) +P. (x .P w)) +P. ((y .P z) +P. (v .P u))) = ((v .P w) +P. ((x .P w) +P. ((y .P z) +P. (v .P u))))
63	44, 61, 60, 45, 46	caopr32 3074	. . . . . . . . . . . . . . . . . . 19 |- (((v .P w) +P. ((y .P z) +P. (v .P u))) +P. (x .P w)) = (((v .P w) +P. (x .P w)) +P. ((y .P z) +P. (v .P u)))
64	50, 47	addasspr 3918	. . . . . . . . . . . . . . . . . . . 20 |- (((x .P w) +P. (y .P z)) +P. (v .P u)) = ((x .P w) +P. ((y .P z) +P. (v .P u)))
65	64	opreq2i 3010	. . . . . . . . . . . . . . . . . . 19 |- ((v .P w) +P. (