Metamath Proof Explorer


Theorem affineequiv4

Description: Equivalence between two ways of expressing A as an affine combination of B and C . (Contributed by AV, 22-Jan-2023)

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

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 affineequiv3 φ A = 1 D B + D C A B = D C B
6 3 2 subcld φ C B
7 4 6 mulcld φ D C B
8 1 2 7 subadd2d φ A B = D C B D C B + B = A
9 eqcom D C B + B = A A = D C B + B
10 8 9 bitrdi φ A B = D C B A = D C B + B
11 5 10 bitrd φ A = 1 D B + D C A = D C B + B