Metamath Proof Explorer


Theorem affineequivne

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

Ref Expression
Hypotheses affineequiv.a φA
affineequiv.b φB
affineequiv.c φC
affineequiv.d φD
affineequivne.d φBC
Assertion affineequivne φA=1DB+DCD=ABCB

Proof

Step Hyp Ref Expression
1 affineequiv.a φA
2 affineequiv.b φB
3 affineequiv.c φC
4 affineequiv.d φD
5 affineequivne.d φBC
6 1 2 3 4 affineequiv3 φA=1DB+DCAB=DCB
7 1 2 subcld φAB
8 3 2 subcld φCB
9 5 necomd φCB
10 3 2 9 subne0d φCB0
11 7 4 8 10 divmul3d φABCB=DAB=DCB
12 eqcom ABCB=DD=ABCB
13 11 12 bitr3di φAB=DCBD=ABCB
14 6 13 bitrd φA=1DB+DCD=ABCB