Theorem affineequiv

Description: Equivalence between two ways of expressing B as an affine combination of A and C . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	affineequiv.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	affineequiv.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	affineequiv.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	affineequiv.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
Assertion	affineequiv	⊢ ( 𝜑 → ( 𝐵 = ( ( 𝐷 · 𝐴 ) + ( ( 1 − 𝐷 ) · 𝐶 ) ) ↔ ( 𝐶 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		affineequiv.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		affineequiv.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		affineequiv.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		affineequiv.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5	4 3	mulcld	⊢ ( 𝜑 → ( 𝐷 · 𝐶 ) ∈ ℂ )
6	4 1	mulcld	⊢ ( 𝜑 → ( 𝐷 · 𝐴 ) ∈ ℂ )
7	3 5 6	subsubd	⊢ ( 𝜑 → ( 𝐶 − ( ( 𝐷 · 𝐶 ) − ( 𝐷 · 𝐴 ) ) ) = ( ( 𝐶 − ( 𝐷 · 𝐶 ) ) + ( 𝐷 · 𝐴 ) ) )
8	3 5	subcld	⊢ ( 𝜑 → ( 𝐶 − ( 𝐷 · 𝐶 ) ) ∈ ℂ )
9	8 6	addcomd	⊢ ( 𝜑 → ( ( 𝐶 − ( 𝐷 · 𝐶 ) ) + ( 𝐷 · 𝐴 ) ) = ( ( 𝐷 · 𝐴 ) + ( 𝐶 − ( 𝐷 · 𝐶 ) ) ) )
10	7 9	eqtr2d	⊢ ( 𝜑 → ( ( 𝐷 · 𝐴 ) + ( 𝐶 − ( 𝐷 · 𝐶 ) ) ) = ( 𝐶 − ( ( 𝐷 · 𝐶 ) − ( 𝐷 · 𝐴 ) ) ) )
11		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
12	11 4 3	subdird	⊢ ( 𝜑 → ( ( 1 − 𝐷 ) · 𝐶 ) = ( ( 1 · 𝐶 ) − ( 𝐷 · 𝐶 ) ) )
13	3	mulid2d	⊢ ( 𝜑 → ( 1 · 𝐶 ) = 𝐶 )
14	13	oveq1d	⊢ ( 𝜑 → ( ( 1 · 𝐶 ) − ( 𝐷 · 𝐶 ) ) = ( 𝐶 − ( 𝐷 · 𝐶 ) ) )
15	12 14	eqtrd	⊢ ( 𝜑 → ( ( 1 − 𝐷 ) · 𝐶 ) = ( 𝐶 − ( 𝐷 · 𝐶 ) ) )
16	15	oveq2d	⊢ ( 𝜑 → ( ( 𝐷 · 𝐴 ) + ( ( 1 − 𝐷 ) · 𝐶 ) ) = ( ( 𝐷 · 𝐴 ) + ( 𝐶 − ( 𝐷 · 𝐶 ) ) ) )
17	3 2	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
18	3 1	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ∈ ℂ )
19	4 18	mulcld	⊢ ( 𝜑 → ( 𝐷 · ( 𝐶 − 𝐴 ) ) ∈ ℂ )
20	2 17 19	addsubassd	⊢ ( 𝜑 → ( ( 𝐵 + ( 𝐶 − 𝐵 ) ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) = ( 𝐵 + ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ) )
21	2 3	pncan3d	⊢ ( 𝜑 → ( 𝐵 + ( 𝐶 − 𝐵 ) ) = 𝐶 )
22	4 3 1	subdid	⊢ ( 𝜑 → ( 𝐷 · ( 𝐶 − 𝐴 ) ) = ( ( 𝐷 · 𝐶 ) − ( 𝐷 · 𝐴 ) ) )
23	21 22	oveq12d	⊢ ( 𝜑 → ( ( 𝐵 + ( 𝐶 − 𝐵 ) ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) = ( 𝐶 − ( ( 𝐷 · 𝐶 ) − ( 𝐷 · 𝐴 ) ) ) )
24	20 23	eqtr3d	⊢ ( 𝜑 → ( 𝐵 + ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ) = ( 𝐶 − ( ( 𝐷 · 𝐶 ) − ( 𝐷 · 𝐴 ) ) ) )
25	10 16 24	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐷 · 𝐴 ) + ( ( 1 − 𝐷 ) · 𝐶 ) ) = ( 𝐵 + ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ) )
26	25	eqeq2d	⊢ ( 𝜑 → ( 𝐵 = ( ( 𝐷 · 𝐴 ) + ( ( 1 − 𝐷 ) · 𝐶 ) ) ↔ 𝐵 = ( 𝐵 + ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ) ) )
27	2	addid1d	⊢ ( 𝜑 → ( 𝐵 + 0 ) = 𝐵 )
28	27	eqeq1d	⊢ ( 𝜑 → ( ( 𝐵 + 0 ) = ( 𝐵 + ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ) ↔ 𝐵 = ( 𝐵 + ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ) ) )
29		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
30	17 19	subcld	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ∈ ℂ )
31	2 29 30	addcand	⊢ ( 𝜑 → ( ( 𝐵 + 0 ) = ( 𝐵 + ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ) ↔ 0 = ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ) )
32	26 28 31	3bitr2d	⊢ ( 𝜑 → ( 𝐵 = ( ( 𝐷 · 𝐴 ) + ( ( 1 − 𝐷 ) · 𝐶 ) ) ↔ 0 = ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ) )
33		eqcom	⊢ ( 0 = ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) ↔ ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) = 0 )
34	32 33	bitrdi	⊢ ( 𝜑 → ( 𝐵 = ( ( 𝐷 · 𝐴 ) + ( ( 1 − 𝐷 ) · 𝐶 ) ) ↔ ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) = 0 ) )
35	17 19	subeq0ad	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) − ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) = 0 ↔ ( 𝐶 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) )
36	34 35	bitrd	⊢ ( 𝜑 → ( 𝐵 = ( ( 𝐷 · 𝐴 ) + ( ( 1 − 𝐷 ) · 𝐶 ) ) ↔ ( 𝐶 − 𝐵 ) = ( 𝐷 · ( 𝐶 − 𝐴 ) ) ) )