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

Proof

Step	Hyp	Ref	Expression
1		affineequiv.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		affineequiv.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		affineequiv.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		affineequiv.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5	1 2 3 4	affineequiv3	⊢ ( 𝜑 → ( 𝐴 = ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐵 ) ) ) )
6	3 2	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
7	4 6	mulcld	⊢ ( 𝜑 → ( 𝐷 · ( 𝐶 − 𝐵 ) ) ∈ ℂ )
8	1 2 7	subadd2d	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐵 ) ) ↔ ( ( 𝐷 · ( 𝐶 − 𝐵 ) ) + 𝐵 ) = 𝐴 ) )
9		eqcom	⊢ ( ( ( 𝐷 · ( 𝐶 − 𝐵 ) ) + 𝐵 ) = 𝐴 ↔ 𝐴 = ( ( 𝐷 · ( 𝐶 − 𝐵 ) ) + 𝐵 ) )
10	8 9	bitrdi	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐵 ) ) ↔ 𝐴 = ( ( 𝐷 · ( 𝐶 − 𝐵 ) ) + 𝐵 ) ) )
11	5 10	bitrd	⊢ ( 𝜑 → ( 𝐴 = ( ( ( 1 − 𝐷 ) · 𝐵 ) + ( 𝐷 · 𝐶 ) ) ↔ 𝐴 = ( ( 𝐷 · ( 𝐶 − 𝐵 ) ) + 𝐵 ) ) )