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