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 ( 𝜑𝐴 ∈ ℂ )
affineequiv.b ( 𝜑𝐵 ∈ ℂ )
affineequiv.c ( 𝜑𝐶 ∈ ℂ )
affineequiv.d ( 𝜑𝐷 ∈ ℂ )
Assertion affineequiv3 ( 𝜑 → ( 𝐴 = ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) ↔ ( 𝐴𝐵 ) = ( 𝐷 · ( 𝐶𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 affineequiv.a ( 𝜑𝐴 ∈ ℂ )
2 affineequiv.b ( 𝜑𝐵 ∈ ℂ )
3 affineequiv.c ( 𝜑𝐶 ∈ ℂ )
4 affineequiv.d ( 𝜑𝐷 ∈ ℂ )
5 1cnd ( 𝜑 → 1 ∈ ℂ )
6 5 4 subcld ( 𝜑 → ( 1 − 𝐷 ) ∈ ℂ )
7 6 2 mulcld ( 𝜑 → ( ( 1 − 𝐷 ) · 𝐵 ) ∈ ℂ )
8 4 3 mulcld ( 𝜑 → ( 𝐷 · 𝐶 ) ∈ ℂ )
9 7 8 addcomd ( 𝜑 → ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) = ( ( 𝐷 · 𝐶 ) + ( ( 1 − 𝐷 ) · 𝐵 ) ) )
10 9 eqeq2d ( 𝜑 → ( 𝐴 = ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) ↔ 𝐴 = ( ( 𝐷 · 𝐶 ) + ( ( 1 − 𝐷 ) · 𝐵 ) ) ) )
11 3 1 2 4 affineequiv ( 𝜑 → ( 𝐴 = ( ( 𝐷 · 𝐶 ) + ( ( 1 − 𝐷 ) · 𝐵 ) ) ↔ ( 𝐵𝐴 ) = ( 𝐷 · ( 𝐵𝐶 ) ) ) )
12 1 2 negsubdi2d ( 𝜑 → - ( 𝐴𝐵 ) = ( 𝐵𝐴 ) )
13 12 eqcomd ( 𝜑 → ( 𝐵𝐴 ) = - ( 𝐴𝐵 ) )
14 13 eqeq1d ( 𝜑 → ( ( 𝐵𝐴 ) = ( 𝐷 · ( 𝐵𝐶 ) ) ↔ - ( 𝐴𝐵 ) = ( 𝐷 · ( 𝐵𝐶 ) ) ) )
15 3 2 negsubdi2d ( 𝜑 → - ( 𝐶𝐵 ) = ( 𝐵𝐶 ) )
16 15 eqcomd ( 𝜑 → ( 𝐵𝐶 ) = - ( 𝐶𝐵 ) )
17 16 oveq2d ( 𝜑 → ( 𝐷 · ( 𝐵𝐶 ) ) = ( 𝐷 · - ( 𝐶𝐵 ) ) )
18 3 2 subcld ( 𝜑 → ( 𝐶𝐵 ) ∈ ℂ )
19 4 18 mulneg2d ( 𝜑 → ( 𝐷 · - ( 𝐶𝐵 ) ) = - ( 𝐷 · ( 𝐶𝐵 ) ) )
20 17 19 eqtrd ( 𝜑 → ( 𝐷 · ( 𝐵𝐶 ) ) = - ( 𝐷 · ( 𝐶𝐵 ) ) )
21 20 eqeq2d ( 𝜑 → ( - ( 𝐴𝐵 ) = ( 𝐷 · ( 𝐵𝐶 ) ) ↔ - ( 𝐴𝐵 ) = - ( 𝐷 · ( 𝐶𝐵 ) ) ) )
22 1 2 subcld ( 𝜑 → ( 𝐴𝐵 ) ∈ ℂ )
23 4 18 mulcld ( 𝜑 → ( 𝐷 · ( 𝐶𝐵 ) ) ∈ ℂ )
24 22 23 neg11ad ( 𝜑 → ( - ( 𝐴𝐵 ) = - ( 𝐷 · ( 𝐶𝐵 ) ) ↔ ( 𝐴𝐵 ) = ( 𝐷 · ( 𝐶𝐵 ) ) ) )
25 14 21 24 3bitrd ( 𝜑 → ( ( 𝐵𝐴 ) = ( 𝐷 · ( 𝐵𝐶 ) ) ↔ ( 𝐴𝐵 ) = ( 𝐷 · ( 𝐶𝐵 ) ) ) )
26 10 11 25 3bitrd ( 𝜑 → ( 𝐴 = ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) ↔ ( 𝐴𝐵 ) = ( 𝐷 · ( 𝐶𝐵 ) ) ) )