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

Theorem affineequiv 20620
 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 9064 . . . . . . . 8
4 affineequiv.A . . . . . . . . 9
52, 4mulcld 9064 . . . . . . . 8
61, 3, 5subsubd 9395 . . . . . . 7
71, 3subcld 9367 . . . . . . . 8
87, 5addcomd 9224 . . . . . . 7
96, 8eqtr2d 2437 . . . . . 6
10 ax-1cn 9004 . . . . . . . . . 10
1110a1i 11 . . . . . . . . 9
1211, 2, 1subdird 9446 . . . . . . . 8
131mulid2d 9062 . . . . . . . . 9
1413oveq1d 6055 . . . . . . . 8
1512, 14eqtrd 2436 . . . . . . 7
1615oveq2d 6056 . . . . . 6
17 affineequiv.B . . . . . . . 8
181, 17subcld 9367 . . . . . . . 8
191, 4subcld 9367 . . . . . . . . 9
202, 19mulcld 9064 . . . . . . . 8
2117, 18, 20addsubassd 9387 . . . . . . 7
2217, 1pncan3d 9370 . . . . . . . 8
232, 1, 4subdid 9445 . . . . . . . 8
2422, 23oveq12d 6058 . . . . . . 7
2521, 24eqtr3d 2438 . . . . . 6
269, 16, 253eqtr4d 2446 . . . . 5
2726eqeq2d 2415 . . . 4
2817addid1d 9222 . . . . 5
2928eqeq1d 2412 . . . 4
30 0cn 9040 . . . . . 6
3130a1i 11 . . . . 5
3218, 20subcld 9367 . . . . 5
3317, 31, 32addcand 9225 . . . 4
3427, 29, 333bitr2d 273 . . 3
35 eqcom 2406 . . 3
3634, 35syl6bb 253 . 2