Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  affineequiv Structured version   Unicode version

Theorem affineequiv 20667
 Description: Equivalence between two ways of expressing as an affine combination of and . (Contributed by David Moews, 28-Feb-2017.)
Hypotheses
Ref Expression
affineequiv.A
affineequiv.B
affineequiv.C
affineequiv.D
Assertion
Ref Expression
affineequiv

Proof of Theorem affineequiv
StepHypRef Expression
1 affineequiv.C . . . . . . . 8
2 affineequiv.D . . . . . . . . 9
32, 1mulcld 9108 . . . . . . . 8
4 affineequiv.A . . . . . . . . 9
52, 4mulcld 9108 . . . . . . . 8
61, 3, 5subsubd 9439 . . . . . . 7
71, 3subcld 9411 . . . . . . . 8
87, 5addcomd 9268 . . . . . . 7
96, 8eqtr2d 2469 . . . . . 6
10 ax-1cn 9048 . . . . . . . . . 10
1110a1i 11 . . . . . . . . 9
1211, 2, 1subdird 9490 . . . . . . . 8
131mulid2d 9106 . . . . . . . . 9
1413oveq1d 6096 . . . . . . . 8
1512, 14eqtrd 2468 . . . . . . 7
1615oveq2d 6097 . . . . . 6
17 affineequiv.B . . . . . . . 8
181, 17subcld 9411 . . . . . . . 8
191, 4subcld 9411 . . . . . . . . 9
202, 19mulcld 9108 . . . . . . . 8
2117, 18, 20addsubassd 9431 . . . . . . 7
2217, 1pncan3d 9414 . . . . . . . 8
232, 1, 4subdid 9489 . . . . . . . 8
2422, 23oveq12d 6099 . . . . . . 7
2521, 24eqtr3d 2470 . . . . . 6
269, 16, 253eqtr4d 2478 . . . . 5
2726eqeq2d 2447 . . . 4
2817addid1d 9266 . . . . 5
2928eqeq1d 2444 . . . 4
30 0cn 9084 . . . . . 6
3130a1i 11 . . . . 5
3218, 20subcld 9411 . . . . 5
3317, 31, 32addcand 9269 . . . 4
3427, 29, 333bitr2d 273 . . 3
35 eqcom 2438 . . 3
3634, 35syl6bb 253 . 2