Theorem distrpq 5067

Description: Multiplication of positive fractions is distributive.

Hypotheses

Ref	Expression
distrpq.1	|- B e. V
distrpq.2	|- C e. V

Assertion

Ref	Expression
distrpq	|- (A .Q (B +Q C)) = ((A .Q B) +Q (A .Q C))

Proof of Theorem distrpq

Step	Hyp	Ref	Expression
1		df-nq 5038	. . 3 |- Q. = ((N. X. N.)/. ~Q )
2		addpipq 5054	. . 3 |- (((z e. N. /\ w e. N.) /\ (v e. N. /\ u e. N.)) -> ([<.z, w>.] ~Q +Q [<.v, u>.] ~Q ) = [<.((z .N u) +N (w .N v)), (w .N u)>.] ~Q )
3		mulpipq 5055	. . . 4 |- (((x e. N. /\ y e. N.) /\ (((z .N u) +N (w .N v)) e. N. /\ (w .N u) e. N.)) -> ([<.x, y>.] ~Q .Q [<.((z .N u) +N (w .N v)), (w .N u)>.] ~Q ) = [<.(x .N ((z .N u) +N (w .N v))), (y .N (w .N u))>.] ~Q )
4		mulclpi 5021	. . . . . . . 8 |- ((x e. N. /\ ((z .N u) +N (w .N v)) e. N.) -> (x .N ((z .N u) +N (w .N v))) e. N.)
5		pm3.26 319	. . . . . . . . 9 |- ((y e. N. /\ (w .N u) e. N.) -> y e. N.)
6		mulclpi 5021	. . . . . . . . 9 |- ((y e. N. /\ (w .N u) e. N.) -> (y .N (w .N u)) e. N.)
7	5, 6	jca 288	. . . . . . . 8 |- ((y e. N. /\ (w .N u) e. N.) -> (y e. N. /\ (y .N (w .N u)) e. N.))
8	4, 7	anim12i 333	. . . . . . 7 |- (((x e. N. /\ ((z .N u) +N (w .N v)) e. N.) /\ (y e. N. /\ (w .N u) e. N.)) -> ((x .N ((z .N u) +N (w .N v))) e. N. /\ (y e. N. /\ (y .N (w .N u)) e. N.)))
9		an12 484	. . . . . . . 8 |- (((x .N ((z .N u) +N (w .N v))) e. N. /\ (y e. N. /\ (y .N (w .N u)) e. N.)) <-> (y e. N. /\ ((x .N ((z .N u) +N (w .N v))) e. N. /\ (y .N (w .N u)) e. N.)))
10		3anass 779	. . . . . . . 8 |- ((y e. N. /\ (x .N ((z .N u) +N (w .N v))) e. N. /\ (y .N (w .N u)) e. N.) <-> (y e. N. /\ ((x .N ((z .N u) +N (w .N v))) e. N. /\ (y .N (w .N u)) e. N.)))
11	9, 10	bitr4 176	. . . . . . 7 |- (((x .N ((z .N u) +N (w .N v))) e. N. /\ (y e. N. /\ (y .N (w .N u)) e. N.)) <-> (y e. N. /\ (x .N ((z .N u) +N (w .N v))) e. N. /\ (y .N (w .N u)) e. N.))
12	8, 11	sylib 198	. . . . . 6 |- (((x e. N. /\ ((z .N u) +N (w .N v)) e. N.) /\ (y e. N. /\ (w .N u) e. N.)) -> (y e. N. /\ (x .N ((z .N u) +N (w .N v))) e. N. /\ (y .N (w .N u)) e. N.))
13	12	an4s 508	. . . . 5 |- (((x e. N. /\ y e. N.) /\ (((z .N u) +N (w .N v)) e. N. /\ (w .N u) e. N.)) -> (y e. N. /\ (x .N ((z .N u) +N (w .N v))) e. N. /\ (y .N (w .N u)) e. N.))
14		visset 1813	. . . . . 6 |- y e. V
15		oprex 3983	. . . . . 6 |- (x .N ((z .N u) +N (w .N v))) e. V
16		oprex 3983	. . . . . 6 |- (y .N (w .N u)) e. V
17	14, 15, 16	distrpqlem 5066	. . . . 5 |- ((y e. N. /\ (x .N ((z .N u) +N (w .N v))) e. N. /\ (y .N (w .N u)) e. N.) -> [<.(y .N (x .N ((z .N u) +N (w .N v)))), (y .N (y .N (w .N u)))>.] ~Q = [<.(x .N ((z .N u) +N (w .N v))), (y .N (w .N u))>.] ~Q )
18	13, 17	syl 10	. . . 4 |- (((x e. N. /\ y e. N.) /\ (((z .N u) +N (w .N v)) e. N. /\ (w .N u) e. N.)) -> [<.(y .N (x .N ((z .N u) +N (w .N v)))), (y .N (y .N (w .N u)))>.] ~Q = [<.(x .N ((z .N u) +N (w .N v))), (y .N (w .N u))>.] ~Q )
19	3, 18	eqtr4d 1510	. . 3 |- (((x e. N. /\ y e. N.) /\ (((z .N u) +N (w .N v)) e. N. /\ (w .N u) e. N.)) -> ([<.x, y>.] ~Q .Q [<.((z .N u) +N (w .N v)), (w .N u)>.] ~Q ) = [<.(y .N (x .N ((z .N u) +N (w .N v)))), (y .N (y .N (w .N u)))>.] ~Q )
20		mulpipq 5055	. . 3 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> ([<.x, y>.] ~Q .Q [<.z, w>.] ~Q ) = [<.(x .N z), (y .N w)>.] ~Q )
21		mulpipq 5055	. . 3 |- (((x e. N. /\ y e. N.) /\ (v e. N. /\ u e. N.)) -> ([<.x, y>.] ~Q .Q [<.v, u>.] ~Q ) = [<.(x .N v), (y .N u)>.] ~Q )
22		addpipq 5054	. . 3 |- ((((x .N z) e. N. /\ (y .N w) e. N.) /\ ((x .N v) e. N. /\ (y .N u) e. N.)) -> ([<.(x .N z), (y .N w)>.] ~Q +Q [<.(x .N v), (y .N u)>.] ~Q ) = [<.(((x .N z) .N (y .N u)) +N ((y .N w) .N (x .N v))), ((y .N w) .N (y .N u))>.] ~Q )
23		addclpi 5020	. . . . . 6 |- (((z .N u) e. N. /\ (w .N v) e. N.) -> ((z .N u) +N (w .N v)) e. N.)
24		mulclpi 5021	. . . . . 6 |- ((z e. N. /\ u e. N.) -> (z .N u) e. N.)
25		mulclpi 5021	. . . . . 6 |- ((w e. N. /\ v e. N.) -> (w .N v) e. N.)
26	23, 24, 25	syl2an 454	. . . . 5 |- (((z e. N. /\ u e. N.) /\ (w e. N. /\ v e. N.)) -> ((z .N u) +N (w .N v)) e. N.)
27	26	an42s 509	. . . 4 |- (((z e. N. /\ w e. N.) /\ (v e. N. /\ u e. N.)) -> ((z .N u) +N (w .N v)) e. N.)
28		mulclpi 5021	. . . . 5 |- ((w e. N. /\ u e. N.) -> (w .N u) e. N.)
29	28	ad2ant2l 408	. . . 4 |- (((z e. N. /\ w e. N.) /\ (v e. N. /\ u e. N.)) -> (w .N u) e. N.)
30	27, 29	jca 288	. . 3 |- (((z e. N. /\ w e. N.) /\ (v e. N. /\ u e. N.)) -> (((z .N u) +N (w .N v)) e. N. /\ (w .N u) e. N.))
31		mulclpi 5021	. . . . 5 |- ((x e. N. /\ z e. N.) -> (x .N z) e. N.)
32		mulclpi 5021	. . . . 5 |- ((y e. N. /\ w e. N.) -> (y .N w) e. N.)
33	31, 32	anim12i 333	. . . 4 |- (((x e. N. /\ z e. N.) /\ (y e. N. /\ w e. N.)) -> ((x .N z) e. N. /\ (y .N w) e. N.))
34	33	an4s 508	. . 3 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> ((x .N z) e. N. /\ (y .N w) e. N.))
35		mulclpi 5021	. . . . 5 |- ((x e. N. /\ v e. N.) -> (x .N v) e. N.)
36		mulclpi 5021	. . . . 5 |- ((y e. N. /\ u e. N.) -> (y .N u) e. N.)
37	35, 36	anim12i 333	. . . 4 |- (((x e. N. /\ v e. N.) /\ (y e. N. /\ u e. N.)) -> ((x .N v) e. N. /\ (y .N u) e. N.))
38	37	an4s 508	. . 3 |- (((x e. N. /\ y e. N.) /\ (v e. N. /\ u e. N.)) -> ((x .N v) e. N. /\ (y .N u) e. N.))
39		oprex 3983	. . . . 5 |- (z .N u) e. V
40		oprex 3983	. . . . 5 |- (w .N v) e. V
41	39, 40	distrpi 5026	. . . 4 |- ((y .N x) .N ((z .N u) +N (w .N v))) = (((y .N x) .N (z .N u)) +N ((y .N x) .N (w .N v)))
42		visset 1813	. . . . 5 |- x e. V
43		oprex 3983	. . . . 5 |- ((z .N u) +N (w .N v)) e. V
44	42, 43	mulasspi 5025	. . . 4 |- ((y .N x) .N ((z .N u) +N (w .N v))) = (y .N (x .N ((z .N u) +N (