Theorem distrsr 5172

Description: Multiplication of signed reals is distributive.

Hypotheses

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

Assertion

Ref	Expression
distrsr	|- (A .R (B +R C)) = ((A .R B) +R (A .R C))

Proof of Theorem distrsr

Step	Hyp	Ref	Expression
1		df-nr 5139	. . 3 |- R. = ((P. X. P.)/. ~R )
2		addsrpr 5156	. . 3 |- (((z e. P. /\ w e. P.) /\ (v e. P. /\ u e. P.)) -> ([<.z, w>.] ~R +R [<.v, u>.] ~R ) = [<.(z +P. v), (w +P. u)>.] ~R )
3		mulsrpr 5157	. . 3 |- (((x e. P. /\ y e. P.) /\ ((z +P. v) e. P. /\ (w +P. u) e. P.)) -> ([<.x, y>.] ~R .R [<.(z +P. v), (w +P. u)>.] ~R ) = [<.((x .P. (z +P. v)) +P. (y .P. (w +P. u))), ((x .P. (w +P. u)) +P. (y .P. (z +P. v)))>.] ~R )
4		mulsrpr 5157	. . 3 |- (((x e. P. /\ y e. P.) /\ (z e. P. /\ w e. P.)) -> ([<.x, y>.] ~R .R [<.z, w>.] ~R ) = [<.((x .P. z) +P. (y .P. w)), ((x .P. w) +P. (y .P. z))>.] ~R )
5		mulsrpr 5157	. . 3 |- (((x e. P. /\ y e. P.) /\ (v e. P. /\ u e. P.)) -> ([<.x, y>.] ~R .R [<.v, u>.] ~R ) = [<.((x .P. v) +P. (y .P. u)), ((x .P. u) +P. (y .P. v))>.] ~R )
6		addsrpr 5156	. . 3 |- (((((x .P. z) +P. (y .P. w)) e. P. /\ ((x .P. w) +P. (y .P. z)) e. P.) /\ (((x .P. v) +P. (y .P. u)) e. P. /\ ((x .P. u) +P. (y .P. v)) e. P.)) -> ([<.((x .P. z) +P. (y .P. w)), ((x .P. w) +P. (y .P. z))>.] ~R +R [<.((x .P. v) +P. (y .P. u)), ((x .P. u) +P. (y .P. v))>.] ~R ) = [<.(((x .P. z) +P. (y .P. w)) +P. ((x .P. v) +P. (y .P. u))), (((x .P. w) +P. (y .P. z)) +P. ((x .P. u) +P. (y .P. v)))>.] ~R )
7		addclpr 5092	. . . . 5 |- ((z e. P. /\ v e. P.) -> (z +P. v) e. P.)
8		addclpr 5092	. . . . 5 |- ((w e. P. /\ u e. P.) -> (w +P. u) e. P.)
9	7, 8	anim12i 333	. . . 4 |- (((z e. P. /\ v e. P.) /\ (w e. P. /\ u e. P.)) -> ((z +P. v) e. P. /\ (w +P. u) e. P.))
10	9	an4s 507	. . 3 |- (((z e. P. /\ w e. P.) /\ (v e. P. /\ u e. P.)) -> ((z +P. v) e. P. /\ (w +P. u) e. P.))
11		addclpr 5092	. . . . . 6 |- (((x .P. z) e. P. /\ (y .P. w) e. P.) -> ((x .P. z) +P. (y .P. w)) e. P.)
12		mulclpr 5094	. . . . . 6 |- ((x e. P. /\ z e. P.) -> (x .P. z) e. P.)
13		mulclpr 5094	. . . . . 6 |- ((y e. P. /\ w e. P.) -> (y .P. w) e. P.)
14	11, 12, 13	syl2an 454	. . . . 5 |- (((x e. P. /\ z e. P.) /\ (y e. P. /\ w e. P.)) -> ((x .P. z) +P. (y .P. w)) e. P.)
15	14	an4s 507	. . . 4 |- (((x e. P. /\ y e. P.) /\ (z e. P. /\ w e. P.)) -> ((x .P. z) +P. (y .P. w)) e. P.)
16		addclpr 5092	. . . . . 6 |- (((x .P. w) e. P. /\ (y .P. z) e. P.) -> ((x .P. w) +P. (y .P. z)) e. P.)
17		mulclpr 5094	. . . . . 6 |- ((x e. P. /\ w e. P.) -> (x .P. w) e. P.)
18		mulclpr 5094	. . . . . 6 |- ((y e. P. /\ z e. P.) -> (y .P. z) e. P.)
19	16, 17, 18	syl2an 454	. . . . 5 |- (((x e. P. /\ w e. P.) /\ (y e. P. /\ z e. P.)) -> ((x .P. w) +P. (y .P. z)) e. P.)
20	19	an42s 508	. . . 4 |- (((x e. P. /\ y e. P.) /\ (z e. P. /\ w e. P.)) -> ((x .P. w) +P. (y .P. z)) e. P.)
21	15, 20	jca 288	. . 3 |- (((x e. P. /\ y e. P.) /\ (z e. P. /\ w e. P.)) -> (((x .P. z) +P. (y .P. w)) e. P. /\ ((x .P. w) +P. (y .P. z)) e. P.))
22		addclpr 5092	. . . . . 6 |- (((x .P. v) e. P. /\ (y .P. u) e. P.) -> ((x .P. v) +P. (y .P. u)) e. P.)
23		mulclpr 5094	. . . . . 6 |- ((x e. P. /\ v e. P.) -> (x .P. v) e. P.)
24		mulclpr 5094	. . . . . 6 |- ((y e. P. /\ u e. P.) -> (y .P. u) e. P.)
25	22, 23, 24	syl2an 454	. . . . 5 |- (((x e. P. /\ v e. P.) /\ (y e. P. /\ u e. P.)) -> ((x .P. v) +P. (y .P. u)) e. P.)
26	25	an4s 507	. . . 4 |- (((x e. P. /\ y e. P.) /\ (v e. P. /\ u e. P.)) -> ((x .P. v) +P. (y .P. u)) e. P.)
27		addclpr 5092	. . . . . 6 |- (((x .P. u) e. P. /\ (y .P. v) e. P.) -> ((x .P. u) +P. (y .P. v)) e. P.)
28		mulclpr 5094	. . . . . 6 |- ((x e. P. /\ u e. P.) -> (x .P. u) e. P.)
29		mulclpr 5094	. . . . . 6 |- ((y e. P. /\ v e. P.) -> (y .P. v) e. P.)
30	27, 28, 29	syl2an 454	. . . . 5 |- (((x e. P. /\ u e. P.) /\ (y e. P. /\ v e. P.)) -> ((x .P. u) +P. (y .P. v)) e. P.)
31	30	an42s 508	. . . 4 |- (((x e. P. /\ y e. P.) /\ (v e. P. /\ u e. P.)) -> ((x .P. u) +P. (y .P. v)) e. P.)
32	26, 31	jca 288	. . 3 |- (((x e. P. /\ y e. P.) /\ (v e. P. /\ u e. P.)) -> (((x .P. v) +P. (y .P. u)) e. P. /\ ((x .P. u) +P. (y .P. v)) e. P.))
33		visset 1804	. . . . . 6 |- z e. V
34		visset 1804	. . . . . 6 |- v e. V
35	33, 34	distrpr 5104	. . . . 5 |- (x .P. (z +P. v)) = ((x .P. z) +P. (x .P. v))
36		visset 1804	. . . . . 6 |- w e. V
37		visset 1804	. . . . . 6 |- u e. V
38	36, 37	distrpr 5104	. . . . 5 |- (y .P. (w +P. u)) = ((y .P. w) +P. (y .P. u))
39	35, 38	opreq12i 3958	. . . 4 |- ((x .P. (z +P. v)) +P. (y .P. (w +P. u))) = (((x .P. z) +P. (x .P. v)) +P. ((y .P. w) +P. (y .P. u)))
40		oprex 3968	. . . . 5 |- (x .P. z) e. V
41		oprex 3968	. . . . 5 |- (x .P. v) e. V
42		oprex 3968	. . . . 5 |- (y .P. w) e. V
43		visset 1804	. . . . . 6 |- f e. V
44		visset 1804	. . . . . 6 |- g e. V
45	43, 44	addcompr 5095	. . . . 5 |- (f +P. g) = (g +P. f)
46		visset 1804	. . . . . 6 |- h e. V
47	44, 46	addasspr 5096	. . . . 5 |- ((f +P. g) +P. h) = (f +P. (g +P. h))
48		oprex 3968	. . . . 5 |- (y .P. u) e. V
49	40, 41, 42, 45, 47, 48	caopr4 4050	. . . 4 |- (((x .P. z) +P. (x .P. v)) +P. ((y .P. w) +P. (y .P. u))) = (((x .P. z) +P. (y .P. w)) +P. ((x .P. v) +P. (y .P. u)))
50	39, 49	eqtr 1487	. . 3 |- ((x .P. (z +P. v)) +P. (y .P. (w +P. u))) = (((x .P. z) +P. (y .P. w)) +P. ((x .P. v) +P. (y .P. u)))
51	36, 37	distrpr 5104	. . . . 5 |- (x .P. (w +P. u)) = ((x .P. w) +P. (x .P. u))
52	33, 34	distrpr 5104	. . . . 5 |- (y .P. (z +P. v)) = ((y .P. z) +P. (y .P. v))
53	51, 52	opreq12i 3958	. . . 4 |- ((x .P. (w +P. u)) +P. (y .P. (z +P. v))) = (((x .P. w) +P. (x .P. u)) +P. ((y .P. z) +P. (y .P. v)))
54		oprex 3968	. . . . 5 |- (x .P. w) e. V
55		oprex 3968	. . . . 5 |- (x .P. u) e. V
56		oprex 3968	. . . . 5 |- (y .P. z) e. V
57		oprex 3968	. . . . 5 |- (y .P. v) e. V
58	54, 55, 56, 45, 47, 57	caopr4 4050	. . . 4 |- (((x .P. w) +P. (x .P. u)) +P. ((y .P. z) +P. (y .P. v))) = (((x .P. w) +P. (y .P. z)) +P. ((x .P. u) +P. (y .P. v)))
59	53, 58	eqtr 1487	. . 3 |- ((x .P. (w +P. u)) +P. (y .P. (z +P. v))) = (((x .P. w) +P. (y .P. z)) +P. ((x .P. u) +P. (y .P. v)))
60	1, 2, 3, 4, 5, 6, 10, 21, 32, 50, 59	ecoprdi 4305	. 2 |- ((A e. R. /\ B e. R. /\ C e. R.) -> (A .R (B