HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem muladdt 5393
Description: Product of two sums.
Assertion
Ref Expression
muladdt |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((A + B) x. (C + D)) = (((A x. C) + (D x. B)) + ((A x. D) + (C x. B))))
Proof of Theorem muladdt
StepHypRef Expression
1 axdistr 5251 . . 3 |- (((A + B) e. CC /\ C e. CC /\ D e. CC) -> ((A + B) x. (C + D)) = (((A + B) x. C) + ((A + B) x. D)))
2 axaddcl 5243 . . . 4 |- ((A e. CC /\ B e. CC) -> (A + B) e. CC)
32adantr 389 . . 3 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (A + B) e. CC)
4 simprl 414 . . 3 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> C e. CC)
5 simprr 415 . . 3 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> D e. CC)
61, 3, 4, 5syl3anc 856 . 2 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((A + B) x. (C + D)) = (((A + B) x. C) + ((A + B) x. D)))
7 adddirt 5291 . . . . 5 |- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) x. C) = ((A x. C) + (B x. C)))
873expa 831 . . . 4 |- (((A e. CC /\ B e. CC) /\ C e. CC) -> ((A + B) x. C) = ((A x. C) + (B x. C)))
98adantrr 395 . . 3 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((A + B) x. C) = ((A x. C) + (B x. C)))
10 adddirt 5291 . . . . 5 |- ((A e. CC /\ B e. CC /\ D e. CC) -> ((A + B) x. D) = ((A x. D) + (B x. D)))
11103expa 831 . . . 4 |- (((A e. CC /\ B e. CC) /\ D e. CC) -> ((A + B) x. D) = ((A x. D) + (B x. D)))
1211adantrl 394 . . 3 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((A + B) x. D) = ((A x. D) + (B x. D)))
139, 12opreq12d 3963 . 2 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (((A + B) x. C) + ((A + B) x. D)) = (((A x. C) + (B x. C)) + ((A x. D) + (B x. D))))
14 add23t 5309 . . . 4 |- (((A x. C) e. CC /\ (B x. C) e. CC /\ ((A x. D) + (B x. D)) e. CC) -> (((A x. C) + (B x. C)) + ((A x. D) + (B x. D))) = (((A x. C) + ((A x. D) + (B x. D))) + (B x. C)))
15 axmulcl 5245 . . . . 5 |- ((A e. CC /\ C e. CC) -> (A x. C) e. CC)
1615ad2ant2r 409 . . . 4 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (A x. C) e. CC)
17 axmulcl 5245 . . . . 5 |- ((B e. CC /\ C e. CC) -> (B x. C) e. CC)
1817ad2ant2lr 410 . . . 4 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (B x. C) e. CC)
19 axaddcl 5243 . . . . . . 7 |- (((A x. D) e. CC /\ (B x. D) e. CC) -> ((A x. D) + (B x. D)) e. CC)
20 axmulcl 5245 . . . . . . 7 |- ((A e. CC /\ D e. CC) -> (A x. D) e. CC)
21 axmulcl 5245 . . . . . . 7 |- ((B e. CC /\ D e. CC) -> (B x. D) e. CC)
2219, 20, 21syl2an 454 . . . . . 6 |- (((A e. CC /\ D e. CC) /\ (B e. CC /\ D e. CC)) -> ((A x. D) + (B x. D)) e. CC)
2322anandirs 512 . . . . 5 |- (((A e. CC /\ B e. CC) /\ D e. CC) -> ((A x. D) + (B x. D)) e. CC)
2423adantrl 394 . . . 4 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((A x. D) + (B x. D)) e. CC)
2514, 16, 18, 24syl3anc 856 . . 3 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (((A x. C) + (B x. C)) + ((A x. D) + (B x. D))) = (((A x. C) + ((A x. D) + (B x. D))) + (B x. C)))
26 axmulcom 5248 . . . . . . 7 |- ((B e. CC /\ D e. CC) -> (B x. D) = (D x. B))
2726ad2ant2l 408 . . . . . 6 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (B x. D) = (D x. B))
2827opreq2d 3961 . . . . 5 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (((A x. C) + (A x. D)) + (B x. D)) = (((A x. C) + (A x. D)) + (D x. B)))
29 axaddass 5249 . . . . . 6 |- (((A x. C) e. CC /\ (A x. D) e. CC /\ (B x. D) e. CC) -> (((A x. C) + (A x. D)) + (B x. D)) = ((A x. C) + ((A x. D) + (B x. D))))
3020ad2ant2rl 411 . . . . . 6 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (A x. D) e. CC)
3121ad2ant2l 408 . . . . . 6 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (B x. D) e. CC)
3229, 16, 30, 31syl3anc 856 . . . . 5 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (((A x. C) + (A x. D)) + (B x. D)) = ((A x. C) + ((A x. D) + (B x. D))))
33 add23t 5309 . . . . . 6 |- (((A x. C) e. CC /\ (A x. D) e. CC /\ (D x. B) e. CC) -> (((A x. C) + (A x. D)) + (D x. B)) = (((A x. C) + (D x. B)) + (A x. D)))
34 axmulcl 5245 . . . . . . . 8 |- ((D e. CC /\ B e. CC) -> (D x. B) e. CC)
3534ancoms 436 . . . . . . 7 |- ((B e. CC /\ D e. CC) -> (D x. B) e. CC)
3635ad2ant2l 408 . . . . . 6 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (D x. B) e. CC)
3733, 16, 30, 36syl3anc 856 . . . . 5 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (((A x. C) + (A x. D)) + (D x. B)) = (((A x. C) + (D x. B)) + (A x. D)))
3828, 32, 373eqtr3d 1507 . . . 4 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((A x. C) + ((A x. D) + (B x. D))) = (((A x. C) + (D x. B)) + (A x. D)))
39 axmulcom 5248 . . . . 5 |- ((B e. CC /\ C e. CC) -> (B x. C) = (C x. B))
4039ad2ant2lr 410 . . . 4 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (B x. C) = (C x. B))
4138, 40opreq12d 3963 . . 3 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (((A x. C) + ((A x. D) + (B x. D))) + (B x. C)) = ((((A x. C) + (D x. B)) + (A x. D)) + (C x. B)))
42 axaddass 5249 . . . 4 |- ((((A x. C) + (D x. B)) e. CC /\ (A x. D) e. CC /\ (C x. B) e. CC) -> ((((A x. C) + (D x. B)) + (A x. D)) + (C x. B)) = (((A x. C) + (D x. B)) + ((A x. D) + (C x. B))))
43 axaddcl 5243 . . . . . 6 |- (((A x. C) e. CC /\ (D x. B) e. CC) -> ((A x. C) + (D x. B)) e. CC)
4443, 15, 35syl2an 454 . . . . 5 |- (((A e. CC /\ C e. CC) /\ (B e. CC /\ D e. CC)) -> ((A x. C) + (D x. B)) e. CC)
4544an4s 507 . . . 4 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((A x. C) + (D x. B)) e. CC)
46 axmulcl 5245 . . . . . 6 |- ((C e. CC /\ B e. CC) ->