Metamath Proof Explorer

Theorem affinecomb1

Description: Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023)

Ref Expression
Hypotheses affinecomb1.a ⊢φ→A∈ℝ
affinecomb1.b ⊢φ→B∈ℝ
affinecomb1.c ⊢φ→C∈ℝ
affinecomb1.d ⊢φ→B≠C
affinecomb1.e ⊢φ→E∈ℝ
affinecomb1.f ⊢φ→F∈ℝ
affinecomb1.g ⊢φ→G∈ℝ
affinecomb1.s ⊢S=G−FC−B
Assertion affinecomb1 ⊢φ→∃t∈ℝA=1−t⁢B+t⁢C∧E=1−t⁢F+t⁢G↔E=S⁢A−B+F

Proof

Step Hyp Ref Expression
1 affinecomb1.a ⊢φ→A∈ℝ
2 affinecomb1.b ⊢φ→B∈ℝ
3 affinecomb1.c ⊢φ→C∈ℝ
4 affinecomb1.d ⊢φ→B≠C
5 affinecomb1.e ⊢φ→E∈ℝ
6 affinecomb1.f ⊢φ→F∈ℝ
7 affinecomb1.g ⊢φ→G∈ℝ
8 affinecomb1.s ⊢S=G−FC−B
9 1 adantr ⊢φ∧t∈ℝ→A∈ℝ
10 9 recnd ⊢φ∧t∈ℝ→A∈ℂ
11 2 adantr ⊢φ∧t∈ℝ→B∈ℝ
12 11 recnd ⊢φ∧t∈ℝ→B∈ℂ
13 3 adantr ⊢φ∧t∈ℝ→C∈ℝ
14 13 recnd ⊢φ∧t∈ℝ→C∈ℂ
15 simpr ⊢φ∧t∈ℝ→t∈ℝ
16 15 recnd ⊢φ∧t∈ℝ→t∈ℂ
17 4 adantr ⊢φ∧t∈ℝ→B≠C
18 10 12 14 16 17 affineequivne ⊢φ∧t∈ℝ→A=1−t⁢B+t⁢C↔t=A−BC−B
19 oveq2 ⊢t=A−BC−B→1−t=1−A−BC−B
20 19 oveq1d ⊢t=A−BC−B→1−t⁢F=1−A−BC−B⁢F
21 oveq1 ⊢t=A−BC−B→t⁢G=A−BC−B⁢G
22 20 21 oveq12d ⊢t=A−BC−B→1−t⁢F+t⁢G=1−A−BC−B⁢F+A−BC−B⁢G
23 22 eqeq2d ⊢t=A−BC−B→E=1−t⁢F+t⁢G↔E=1−A−BC−B⁢F+A−BC−B⁢G
24 23 adantl ⊢φ∧t∈ℝ∧t=A−BC−B→E=1−t⁢F+t⁢G↔E=1−A−BC−B⁢F+A−BC−B⁢G
25 eqidd ⊢φ→A−BC−B⁢G−F+F=A−BC−B⁢G−F+F
26 1 2 resubcld ⊢φ→A−B∈ℝ
27 3 2 resubcld ⊢φ→C−B∈ℝ
28 3 recnd ⊢φ→C∈ℂ
29 2 recnd ⊢φ→B∈ℂ
30 4 necomd ⊢φ→C≠B
31 28 29 30 subne0d ⊢φ→C−B≠0
32 26 27 31 redivcld ⊢φ→A−BC−B∈ℝ
33 7 6 resubcld ⊢φ→G−F∈ℝ
34 32 33 remulcld ⊢φ→A−BC−B⁢G−F∈ℝ
35 34 6 readdcld ⊢φ→A−BC−B⁢G−F+F∈ℝ
36 35 recnd ⊢φ→A−BC−B⁢G−F+F∈ℂ
37 6 recnd ⊢φ→F∈ℂ
38 7 recnd ⊢φ→G∈ℂ
39 32 recnd ⊢φ→A−BC−B∈ℂ
40 36 37 38 39 affineequiv4 ⊢φ→A−BC−B⁢G−F+F=1−A−BC−B⁢F+A−BC−B⁢G↔A−BC−B⁢G−F+F=A−BC−B⁢G−F+F
41 25 40 mpbird ⊢φ→A−BC−B⁢G−F+F=1−A−BC−B⁢F+A−BC−B⁢G
42 26 recnd ⊢φ→A−B∈ℂ
43 27 recnd ⊢φ→C−B∈ℂ
44 33 recnd ⊢φ→G−F∈ℂ
45 42 43 44 31 div13d ⊢φ→A−BC−B⁢G−F=G−FC−B⁢A−B
46 8 oveq1i ⊢S⁢A−B=G−FC−B⁢A−B
47 45 46 eqtr4di ⊢φ→A−BC−B⁢G−F=S⁢A−B
48 47 oveq1d ⊢φ→A−BC−B⁢G−F+F=S⁢A−B+F
49 41 48 eqtr3d ⊢φ→1−A−BC−B⁢F+A−BC−B⁢G=S⁢A−B+F
50 49 adantr ⊢φ∧t∈ℝ→1−A−BC−B⁢F+A−BC−B⁢G=S⁢A−B+F
51 50 eqeq2d ⊢φ∧t∈ℝ→E=1−A−BC−B⁢F+A−BC−B⁢G↔E=S⁢A−B+F
52 51 biimpd ⊢φ∧t∈ℝ→E=1−A−BC−B⁢F+A−BC−B⁢G→E=S⁢A−B+F
53 52 adantr ⊢φ∧t∈ℝ∧t=A−BC−B→E=1−A−BC−B⁢F+A−BC−B⁢G→E=S⁢A−B+F
54 24 53 sylbid ⊢φ∧t∈ℝ∧t=A−BC−B→E=1−t⁢F+t⁢G→E=S⁢A−B+F
55 54 ex ⊢φ∧t∈ℝ→t=A−BC−B→E=1−t⁢F+t⁢G→E=S⁢A−B+F
56 18 55 sylbid ⊢φ∧t∈ℝ→A=1−t⁢B+t⁢C→E=1−t⁢F+t⁢G→E=S⁢A−B+F
57 56 impd ⊢φ∧t∈ℝ→A=1−t⁢B+t⁢C∧E=1−t⁢F+t⁢G→E=S⁢A−B+F
58 57 rexlimdva ⊢φ→∃t∈ℝA=1−t⁢B+t⁢C∧E=1−t⁢F+t⁢G→E=S⁢A−B+F
59 5 adantr ⊢φ∧t=A−BC−B→E∈ℝ
60 59 recnd ⊢φ∧t=A−BC−B→E∈ℂ
61 37 adantr ⊢φ∧t=A−BC−B→F∈ℂ
62 38 adantr ⊢φ∧t=A−BC−B→G∈ℂ
63 32 adantr ⊢φ∧t=A−BC−B→A−BC−B∈ℝ
64 eleq1 ⊢t=A−BC−B→t∈ℝ↔A−BC−B∈ℝ
65 64 adantl ⊢φ∧t=A−BC−B→t∈ℝ↔A−BC−B∈ℝ
66 63 65 mpbird ⊢φ∧t=A−BC−B→t∈ℝ
67 66 recnd ⊢φ∧t=A−BC−B→t∈ℂ
68 60 61 62 67 affineequiv4 ⊢φ∧t=A−BC−B→E=1−t⁢F+t⁢G↔E=t⁢G−F+F
69 19 oveq1d ⊢t=A−BC−B→1−t⁢B=1−A−BC−B⁢B
70 oveq1 ⊢t=A−BC−B→t⁢C=A−BC−B⁢C
71 69 70 oveq12d ⊢t=A−BC−B→1−t⁢B+t⁢C=1−A−BC−B⁢B+A−BC−B⁢C
72 eqidd ⊢φ→A−BC−B=A−BC−B
73 1 recnd ⊢φ→A∈ℂ
74 73 29 28 39 4 affineequivne ⊢φ→A=1−A−BC−B⁢B+A−BC−B⁢C↔A−BC−B=A−BC−B
75 72 74 mpbird ⊢φ→A=1−A−BC−B⁢B+A−BC−B⁢C
76 75 eqcomd ⊢φ→1−A−BC−B⁢B+A−BC−B⁢C=A
77 71 76 sylan9eqr ⊢φ∧t=A−BC−B→1−t⁢B+t⁢C=A
78 77 eqcomd ⊢φ∧t=A−BC−B→A=1−t⁢B+t⁢C
79 78 biantrurd ⊢φ∧t=A−BC−B→E=1−t⁢F+t⁢G↔A=1−t⁢B+t⁢C∧E=1−t⁢F+t⁢G
80 45 adantr ⊢φ∧t=A−BC−B→A−BC−B⁢G−F=G−FC−B⁢A−B
81 oveq1 ⊢t=A−BC−B→t⁢G−F=A−BC−B⁢G−F
82 81 adantl ⊢φ∧t=A−BC−B→t⁢G−F=A−BC−B⁢G−F
83 46 a1i ⊢φ∧t=A−BC−B→S⁢A−B=G−FC−B⁢A−B
84 80 82 83 3eqtr4d ⊢φ∧t=A−BC−B→t⁢G−F=S⁢A−B
85 84 oveq1d ⊢φ∧t=A−BC−B→t⁢G−F+F=S⁢A−B+F
86 85 eqeq2d ⊢φ∧t=A−BC−B→E=t⁢G−F+F↔E=S⁢A−B+F
87 68 79 86 3bitr3d ⊢φ∧t=A−BC−B→A=1−t⁢B+t⁢C∧E=1−t⁢F+t⁢G↔E=S⁢A−B+F
88 32 87 rspcedv ⊢φ→E=S⁢A−B+F→∃t∈ℝA=1−t⁢B+t⁢C∧E=1−t⁢F+t⁢G
89 58 88 impbid ⊢φ→∃t∈ℝA=1−t⁢B+t⁢C∧E=1−t⁢F+t⁢G↔E=S⁢A−B+F