Theorem distrpq 3861

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 3832	. . 3 |- Q. = ((N. X. N.)/. ~Q )
2		addpipq 3848	. . 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 3849	. . . 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 3815	. . . . . . . 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 256	. . . . . . . . 9 |- ((y e. N. /\ (w .N u) e. N.) -> y e. N.)
6		mulclpi 3815	. . . . . . . . 9 |- ((y e. N. /\ (w .N u) e. N.) -> (y .N (w .N u)) e. N.)
7	5, 6	jca 236	. . . . . . . 8 |- ((y e. N. /\ (w .N u) e. N.) -> (y e. N. /\ (y .N (w .N u)) e. N.))
8	4, 7	anim12i 268	. . . . . . 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 370	. . . . . . . 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 585	. . . . . . . 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 154	. . . . . . 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 173	. . . . . 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 390	. . . . 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 1350	. . . . . 6 |- y e. V
15		oprex 3018	. . . . . 6 |- (x .N ((z .N u) +N (w .N v))) e. V
16		oprex 3018	. . . . . 6 |- (y .N (w .N u)) e. V
17	14, 15, 16	distrpqlem 3860	. . . . 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 12	. . . 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 1131	. . 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 3849	. . 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 3849	. . 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 3848	. . 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 3814	. . . . . 6 |- (((z .N u) e. N. /\ (w .N v) e. N.) -> ((z .N u) +N (w .N v)) e. N.)
24		mulclpi 3815	. . . . . 6 |- ((z e. N. /\ u e. N.) -> (z .N u) e. N.)
25		mulclpi 3815	. . . . . 6 |- ((w e. N. /\ v e. N.) -> (w .N v) e. N.)
26	23, 24, 25	syl2an 349	. . . . 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 391	. . . 4 |- (((z e. N. /\ w e. N.) /\ (v e. N. /\ u e. N.)) -> ((z .N u) +N (w .N v)) e. N.)
28		mulclpi 3815	. . . . . 6 |- ((w e. N. /\ u e. N.) -> (w .N u) e. N.)
29	28	adantl 305	. . . . 5 |- (((z e. N. /\ v e. N.) /\ (w e. N. /\ u e. N.)) -> (w .N u) e. N.)
30	29	an4s 390	. . . 4 |- (((z e. N. /\ w e. N.) /\ (v e. N. /\ u e. N.)) -> (w .N u) e. N.)
31	27, 30	jca 236	. . 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.))
32		mulclpi 3815	. . . . 5 |- ((x e. N. /\ z e. N.) -> (x .N z) e. N.)
33		mulclpi 3815	. . . . 5 |- ((y e. N. /\ w e. N.) -> (y .N w) e. N.)
34	32, 33	anim12i 268	. . . 4 |- (((x e. N. /\ z e. N.) /\ (y e. N. /\ w e. N.)) -> ((x .N z) e. N. /\ (y .N w) e. N.))
35	34	an4s 390	. . 3 |- (((x e. N. /\ y e. N.) /\ (z e. N. /\ w e. N.)) -> ((x .N z) e. N. /\ (y .N w) e. N.))
36		mulclpi 3815	. . . . 5 |- ((x e. N. /\ v e. N.) -> (x .N v) e. N.)
37		mulclpi 3815	. . . . 5 |- ((y e. N. /\ u e. N.) -> (y .N u) e. N.)
38	36, 37	anim12i 268	. . . 4 |- (((x e. N. /\ v e. N.) /\ (y e. N. /\ u e. N.)) -> ((x .N v) e. N. /\ (y .N u) e. N.))
39	38	an4s 390	. . 3 |- (((x e. N. /\ y e. N.) /\ (v e. N. /\ u e. N.)) -> ((x .N v) e. N. /\ (y .N u) e. N.))
40		oprex 3018	. . . . 5 |- (z .N u) e. V
41		oprex 3018	. . . . 5 |- (w .N v) e. V
42	40, 41	distrpi 3820	. . . 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)))
43		visset 1350	. . . . 5 |- x e. V
44		oprex 3018	. . . . 5 |- ((z .N u) +N (w .N v)) e. V
45	43, 44	mulasspi 3819	. . . 4 |- ((y .N x) .N ((z .N u) +N (w .N v))) = (y .N (x .N ((z .N u) +N (w .N v))))
46	43, 14	mulcompi 3818	. . . . . . 7 |- (x .N