Metamath Proof Explorer


Theorem affineequiv3

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 affineequiv3 φ A = 1 D B + D C A B = D C B

Proof

Step Hyp Ref Expression
1 affineequiv.a φ A
2 affineequiv.b φ B
3 affineequiv.c φ C
4 affineequiv.d φ D
5 1cnd φ 1
6 5 4 subcld φ 1 D
7 6 2 mulcld φ 1 D B
8 4 3 mulcld φ D C
9 7 8 addcomd φ 1 D B + D C = D C + 1 D B
10 9 eqeq2d φ A = 1 D B + D C A = D C + 1 D B
11 3 1 2 4 affineequiv φ A = D C + 1 D B B A = D B C
12 1 2 negsubdi2d φ A B = B A
13 12 eqcomd φ B A = A B
14 13 eqeq1d φ B A = D B C A B = D B C
15 3 2 negsubdi2d φ C B = B C
16 15 eqcomd φ B C = C B
17 16 oveq2d φ D B C = D C B
18 3 2 subcld φ C B
19 4 18 mulneg2d φ D C B = D C B
20 17 19 eqtrd φ D B C = D C B
21 20 eqeq2d φ A B = D B C A B = D C B
22 1 2 subcld φ A B
23 4 18 mulcld φ D C B
24 22 23 neg11ad φ A B = D C B A B = D C B
25 14 21 24 3bitrd φ B A = D B C A B = D C B
26 10 11 25 3bitrd φ A = 1 D B + D C A B = D C B