Metamath Proof Explorer


Theorem affineequiv2

Description: Equivalence between two ways of expressing B as an affine combination of A and C . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses affineequiv.a φ A
affineequiv.b φ B
affineequiv.c φ C
affineequiv.d φ D
Assertion affineequiv2 φ B = D A + 1 D C B A = 1 D C A

Proof

Step Hyp Ref Expression
1 affineequiv.a φ A
2 affineequiv.b φ B
3 affineequiv.c φ C
4 affineequiv.d φ D
5 1 2 3 4 affineequiv φ B = D A + 1 D C C B = D C A
6 3 1 subcld φ C A
7 3 2 subcld φ C B
8 4 6 mulcld φ D C A
9 6 7 8 subcanad φ C - A - C B = C - A - D C A C B = D C A
10 3 1 2 nnncan1d φ C - A - C B = B A
11 1cnd φ 1
12 11 4 6 subdird φ 1 D C A = 1 C A D C A
13 6 mulid2d φ 1 C A = C A
14 13 oveq1d φ 1 C A D C A = C - A - D C A
15 12 14 eqtr2d φ C - A - D C A = 1 D C A
16 10 15 eqeq12d φ C - A - C B = C - A - D C A B A = 1 D C A
17 5 9 16 3bitr2d φ B = D A + 1 D C B A = 1 D C A