Theorem distrsr 3994

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 3961	. . 3 |- R. = ((P. X. P.)/. ~R )
2		addsrpr 3978	. . 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 3979	. . 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 3979	. . 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 3979	. . 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 3978	. . 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 3914	. . . . 5 |- ((z e. P. /\ v e. P.) -> (z +P. v) e. P.)
8		addclpr 3914	. . . . 5 |- ((w e. P. /\ u e. P.) -> (w +P. u) e. P.)
9	7, 8	anim12i 268	. . . 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 390	. . 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 3914	. . . . . 6 |- (((x .P z) e. P. /\ (y .P w) e. P.) -> ((x .P z) +P. (y .P w)) e. P.)
12		mulclpr 3916	. . . . . 6 |- ((x e. P. /\ z e. P.) -> (x .P z) e. P.)
13		mulclpr 3916	. . . . . 6 |- ((y e. P. /\ w e. P.) -> (y .P w) e. P.)
14	11, 12, 13	syl2an 349	. . . . 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 390	. . . 4 |- (((x e. P. /\ y e. P.) /\ (z e. P. /\ w e. P.)) -> ((x .P z) +P. (y .P w)) e. P.)
16		addclpr 3914	. . . . . 6 |- (((x .P w) e. P. /\ (y .P z) e. P.) -> ((x .P w) +P. (y .P z)) e. P.)
17		mulclpr 3916	. . . . . 6 |- ((x e. P. /\ w e. P.) -> (x .P w) e. P.)
18		mulclpr 3916	. . . . . 6 |- ((y e. P. /\ z e. P.) -> (y .P z) e. P.)
19	16, 17, 18	syl2an 349	. . . . 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 391	. . . 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 236	. . 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 3914	. . . . . 6 |- (((x .P v) e. P. /\ (y .P u) e. P.) -> ((x .P v) +P. (y .P u)) e. P.)
23		mulclpr 3916	. . . . . 6 |- ((x e. P. /\ v e. P.) -> (x .P v) e. P.)
24		mulclpr 3916	. . . . . 6 |- ((y e. P. /\ u e. P.) -> (y .P u) e. P.)
25	22, 23, 24	syl2an 349	. . . . 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 390	. . . 4 |- (((x e. P. /\ y e. P.) /\ (v e. P. /\ u e. P.)) -> ((x .P v) +P. (y .P u)) e. P.)
27		addclpr 3914	. . . . . 6 |- (((x .P u) e. P. /\ (y .P v) e. P.) -> ((x .P u) +P. (y .P v)) e. P.)
28		mulclpr 3916	. . . . . 6 |- ((x e. P. /\ u e. P.) -> (x .P u) e. P.)
29		mulclpr 3916	. . . . . 6 |- ((y e. P. /\ v e. P.) -> (y .P v) e. P.)
30	27, 28, 29	syl2an 349	. . . . 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 391	. . . 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 236	. . 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 1350	. . . . . 6 |- z e. V
34		visset 1350	. . . . . 6 |- v e. V
35	33, 34	distrpr 3926	. . . . 5 |- (x .P (z +P. v)) = ((x .P z) +P. (x .P v))
36		visset 1350	. . . . . 6 |- w e. V
37		visset 1350	. . . . . 6 |- u e. V
38	36, 37	distrpr 3926	. . . . 5 |- (y .P (w +P. u)) = ((y .P w) +P. (y .P u))
39	35, 38	opreq12i 3011	. . . 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 3018	. . . . 5 |- (x .P z) e. V
41		oprex 3018	. . . . 5 |- (x .P v) e. V
42		oprex 3018	. . . . 5 |- (y .P w) e. V
43		visset 1350	. . . . . 6 |- f e. V
44		visset 1350	. . . . . 6 |- g e. V
45	43, 44	addcompr 3917	. . . . 5 |- (f +P. g) = (g +P. f)
46		visset 1350	. . . . . 6 |- h e. V
47	44, 46	addasspr 3918	. . . . 5 |- ((f +P. g) +P. h) = (f +P. (g +P. h))
48		oprex 3018	. . . . 5 |- (y .P u) e. V
49	40, 41, 42, 45, 47, 48	caopr4 3078	. . . 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 1119	. . 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 3926	. . . . 5 |- (x .P (w +P. u)) = ((x .P w) +P. (x .P u))
52	33, 34	distrpr 3926	. . . . 5 |- (y .P (z +P. v)) = ((y .P z) +P. (y .P v))
53	51, 52	opreq12i 3011	. . . 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 3018	. . . . 5 |- (x .P w) e. V
55		oprex 3018	. . . . 5 |- (x .P u) e. V
56		oprex 3018	. . . . 5 |- (y .P z) e. V
57		oprex 3018	. . . . 5 |- (y .P v) e. V
58	54, 55, 56, 45, 47, 57	caopr4 3078	. . . 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 1119	. . 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 3257	. 2 |- ((A e. R. /\ B e. R. /\ C e. R.) -> (A .R (B +R C)) = ((A .R B) +R (A .R C)))
61		distrsr.1	. . 3 |- B e. V
62		dmaddsr 3988	. . 3 |- dom +R = (R. X. R.)
63		distrsr.2	. . 3 |- C e. V
64		0nsr 3982	. . 3 |- -. (/) e. R.
65		dmmulsr 3989	. . 3 |- dom .R = (R. X. R.)
66	61, 62, 63, 64, 65	ndmoprdistr 3063	. 2 |- (-. (A e. R. /\ B e. R.