Metamath Proof Explorer

Theorem ttgcontlem1

Description: Lemma for % ttgcont . (Contributed by Thierry Arnoux, 24-May-2019)

Ref Expression
Hypotheses ttgval.n ⊢ 𝐺 = ( toTG ‘ 𝐻 )
ttgitvval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ttgitvval.b ⊢ 𝑃 = ( Base ‘ 𝐻 )
ttgitvval.m ⊢ − = ( -g ‘ 𝐻 )
ttgitvval.s ⊢ · = ( ·𝑠 ‘ 𝐻 )
ttgelitv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
ttgelitv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
ttgbtwnid.r ⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝐻 ) )
ttgbtwnid.2 ⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ 𝑅 )
ttgitvval.p ⊢ + = ( +g ‘ 𝐻 )
ttgcontlem1.h ⊢ ( 𝜑 → 𝐻 ∈ ℂVec )
ttgcontlem1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
ttgcontlem1.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑃 )
ttgcontlem1.o ⊢ ( 𝜑 → 𝑀 ≠ 0 )
ttgcontlem1.p ⊢ ( 𝜑 → 𝐾 ≠ 0 )
ttgcontlem1.q ⊢ ( 𝜑 → 𝐾 ≠ 1 )
ttgcontlem1.r ⊢ ( 𝜑 → 𝐿 ≠ 𝑀 )
ttgcontlem1.s ⊢ ( 𝜑 → 𝐿 ≤ ( 𝑀 / 𝐾 ) )
ttgcontlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 [,] 1 ) )
ttgcontlem1.k ⊢ ( 𝜑 → 𝐾 ∈ ( 0 [,] 1 ) )
ttgcontlem1.m ⊢ ( 𝜑 → 𝑀 ∈ ( 0 [,] 𝐿 ) )
ttgcontlem1.y ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) = ( 𝐾 · ( 𝑌 − 𝐴 ) ) )
ttgcontlem1.x ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) = ( 𝑀 · ( 𝑁 − 𝐴 ) ) )
ttgcontlem1.b ⊢ ( 𝜑 → 𝐵 = ( 𝐴 + ( 𝐿 · ( 𝑁 − 𝐴 ) ) ) )
Assertion ttgcontlem1 ( 𝜑 → 𝐵 ∈ ( 𝑋 𝐼 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ttgval.n ⊢ 𝐺 = ( toTG ‘ 𝐻 )
2 ttgitvval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 ttgitvval.b ⊢ 𝑃 = ( Base ‘ 𝐻 )
4 ttgitvval.m ⊢ − = ( -g ‘ 𝐻 )
5 ttgitvval.s ⊢ · = ( ·𝑠 ‘ 𝐻 )
6 ttgelitv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
7 ttgelitv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
8 ttgbtwnid.r ⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝐻 ) )
9 ttgbtwnid.2 ⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ 𝑅 )
10 ttgitvval.p ⊢ + = ( +g ‘ 𝐻 )
11 ttgcontlem1.h ⊢ ( 𝜑 → 𝐻 ∈ ℂVec )
12 ttgcontlem1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
13 ttgcontlem1.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑃 )
14 ttgcontlem1.o ⊢ ( 𝜑 → 𝑀 ≠ 0 )
15 ttgcontlem1.p ⊢ ( 𝜑 → 𝐾 ≠ 0 )
16 ttgcontlem1.q ⊢ ( 𝜑 → 𝐾 ≠ 1 )
17 ttgcontlem1.r ⊢ ( 𝜑 → 𝐿 ≠ 𝑀 )
18 ttgcontlem1.s ⊢ ( 𝜑 → 𝐿 ≤ ( 𝑀 / 𝐾 ) )
19 ttgcontlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 [,] 1 ) )
20 ttgcontlem1.k ⊢ ( 𝜑 → 𝐾 ∈ ( 0 [,] 1 ) )
21 ttgcontlem1.m ⊢ ( 𝜑 → 𝑀 ∈ ( 0 [,] 𝐿 ) )
22 ttgcontlem1.y ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) = ( 𝐾 · ( 𝑌 − 𝐴 ) ) )
23 ttgcontlem1.x ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) = ( 𝑀 · ( 𝑁 − 𝐴 ) ) )
24 ttgcontlem1.b ⊢ ( 𝜑 → 𝐵 = ( 𝐴 + ( 𝐿 · ( 𝑁 − 𝐴 ) ) ) )
25 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
26 25 19 sselid ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
27 25 20 sselid ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
28 26 27 remulcld ⊢ ( 𝜑 → ( 𝐿 · 𝐾 ) ∈ ℝ )
29 0re ⊢ 0 ∈ ℝ
30 iccssre ⊢ ( ( 0 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 0 [,] 𝐿 ) ⊆ ℝ )
31 29 26 30 sylancr ⊢ ( 𝜑 → ( 0 [,] 𝐿 ) ⊆ ℝ )
32 31 21 sseldd ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
33 32 27 remulcld ⊢ ( 𝜑 → ( 𝑀 · 𝐾 ) ∈ ℝ )
34 28 33 resubcld ⊢ ( 𝜑 → ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) ∈ ℝ )
35 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
36 32 35 remulcld ⊢ ( 𝜑 → ( 𝑀 · 1 ) ∈ ℝ )
37 36 33 resubcld ⊢ ( 𝜑 → ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ∈ ℝ )
38 32 recnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
39 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
40 27 recnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
41 38 39 40 subdid ⊢ ( 𝜑 → ( 𝑀 · ( 1 − 𝐾 ) ) = ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) )
42 39 40 subcld ⊢ ( 𝜑 → ( 1 − 𝐾 ) ∈ ℂ )
43 16 necomd ⊢ ( 𝜑 → 1 ≠ 𝐾 )
44 39 40 43 subne0d ⊢ ( 𝜑 → ( 1 − 𝐾 ) ≠ 0 )
45 38 42 14 44 mulne0d ⊢ ( 𝜑 → ( 𝑀 · ( 1 − 𝐾 ) ) ≠ 0 )
46 41 45 eqnetrrd ⊢ ( 𝜑 → ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ≠ 0 )
47 34 37 46 redivcld ⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) ∈ ℝ )
48 0xr ⊢ 0 ∈ ℝ*
49 26 rexrd ⊢ ( 𝜑 → 𝐿 ∈ ℝ* )
50 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ ( 0 [,] 𝐿 ) ) → 0 ≤ 𝑀 )
51 48 49 21 50 mp3an2i ⊢ ( 𝜑 → 0 ≤ 𝑀 )
52 32 51 14 ne0gt0d ⊢ ( 𝜑 → 0 < 𝑀 )
53 32 52 elrpd ⊢ ( 𝜑 → 𝑀 ∈ ℝ+ )
54 35 rexrd ⊢ ( 𝜑 → 1 ∈ ℝ* )
55 iccleub ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ ( 0 [,] 1 ) ) → 𝐾 ≤ 1 )
56 48 54 20 55 mp3an2i ⊢ ( 𝜑 → 𝐾 ≤ 1 )
57 27 35 56 43 leneltd ⊢ ( 𝜑 → 𝐾 < 1 )
58 difrp ⊢ ( ( 𝐾 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐾 < 1 ↔ ( 1 − 𝐾 ) ∈ ℝ+ ) )
59 27 35 58 syl2anc ⊢ ( 𝜑 → ( 𝐾 < 1 ↔ ( 1 − 𝐾 ) ∈ ℝ+ ) )
60 57 59 mpbid ⊢ ( 𝜑 → ( 1 − 𝐾 ) ∈ ℝ+ )
61 53 60 rpmulcld ⊢ ( 𝜑 → ( 𝑀 · ( 1 − 𝐾 ) ) ∈ ℝ+ )
62 41 61 eqeltrrd ⊢ ( 𝜑 → ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ∈ ℝ+ )
63 26 32 resubcld ⊢ ( 𝜑 → ( 𝐿 − 𝑀 ) ∈ ℝ )
64 iccleub ⊢ ( ( 0 ∈ ℝ* ∧ 𝐿 ∈ ℝ* ∧ 𝑀 ∈ ( 0 [,] 𝐿 ) ) → 𝑀 ≤ 𝐿 )
65 48 49 21 64 mp3an2i ⊢ ( 𝜑 → 𝑀 ≤ 𝐿 )
66 26 32 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( 𝐿 − 𝑀 ) ↔ 𝑀 ≤ 𝐿 ) )
67 65 66 mpbird ⊢ ( 𝜑 → 0 ≤ ( 𝐿 − 𝑀 ) )
68 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝐾 ∈ ( 0 [,] 1 ) ) → 0 ≤ 𝐾 )
69 48 54 20 68 mp3an2i ⊢ ( 𝜑 → 0 ≤ 𝐾 )
70 63 27 67 69 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐿 − 𝑀 ) · 𝐾 ) )
71 26 recnd ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
72 71 38 40 subdird ⊢ ( 𝜑 → ( ( 𝐿 − 𝑀 ) · 𝐾 ) = ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) )
73 70 72 breqtrd ⊢ ( 𝜑 → 0 ≤ ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) )
74 34 62 73 divge0d ⊢ ( 𝜑 → 0 ≤ ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) )
75 27 69 15 ne0gt0d ⊢ ( 𝜑 → 0 < 𝐾 )
76 27 75 elrpd ⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
77 26 32 76 lemuldivd ⊢ ( 𝜑 → ( ( 𝐿 · 𝐾 ) ≤ 𝑀 ↔ 𝐿 ≤ ( 𝑀 / 𝐾 ) ) )
78 18 77 mpbird ⊢ ( 𝜑 → ( 𝐿 · 𝐾 ) ≤ 𝑀 )
79 38 mulid1d ⊢ ( 𝜑 → ( 𝑀 · 1 ) = 𝑀 )
80 78 79 breqtrrd ⊢ ( 𝜑 → ( 𝐿 · 𝐾 ) ≤ ( 𝑀 · 1 ) )
81 28 36 33 80 lesub1dd ⊢ ( 𝜑 → ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) ≤ ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) )
82 38 39 mulcld ⊢ ( 𝜑 → ( 𝑀 · 1 ) ∈ ℂ )
83 38 40 mulcld ⊢ ( 𝜑 → ( 𝑀 · 𝐾 ) ∈ ℂ )
84 82 83 subcld ⊢ ( 𝜑 → ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ∈ ℂ )
85 84 mulid1d ⊢ ( 𝜑 → ( ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) · 1 ) = ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) )
86 81 85 breqtrrd ⊢ ( 𝜑 → ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) ≤ ( ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) · 1 ) )
87 34 35 62 ledivmuld ⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) ≤ 1 ↔ ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) ≤ ( ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) · 1 ) ) )
88 86 87 mpbird ⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) ≤ 1 )
89 elicc01 ⊢ ( ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) ∈ ( 0 [,] 1 ) ↔ ( ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) ∧ ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) ≤ 1 ) )
90 47 74 88 89 syl3anbrc ⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) ∈ ( 0 [,] 1 ) )
91 11 cvsclm ⊢ ( 𝜑 → 𝐻 ∈ ℂMod )
92 9 19 sseldd ⊢ ( 𝜑 → 𝐿 ∈ 𝑅 )
93 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
94 iccss2 ⊢ ( ( 0 ∈ ( 0 [,] 1 ) ∧ 𝐿 ∈ ( 0 [,] 1 ) ) → ( 0 [,] 𝐿 ) ⊆ ( 0 [,] 1 ) )
95 93 19 94 sylancr ⊢ ( 𝜑 → ( 0 [,] 𝐿 ) ⊆ ( 0 [,] 1 ) )
96 95 9 sstrd ⊢ ( 𝜑 → ( 0 [,] 𝐿 ) ⊆ 𝑅 )
97 96 21 sseldd ⊢ ( 𝜑 → 𝑀 ∈ 𝑅 )
98 eqid ⊢ ( Scalar ‘ 𝐻 ) = ( Scalar ‘ 𝐻 )
99 98 8 clmsubcl ⊢ ( ( 𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ) → ( 𝐿 − 𝑀 ) ∈ 𝑅 )
100 91 92 97 99 syl3anc ⊢ ( 𝜑 → ( 𝐿 − 𝑀 ) ∈ 𝑅 )
101 98 8 cvsdivcl ⊢ ( ( 𝐻 ∈ ℂVec ∧ ( ( 𝐿 − 𝑀 ) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ 𝑀 ≠ 0 ) ) → ( ( 𝐿 − 𝑀 ) / 𝑀 ) ∈ 𝑅 )
102 11 100 97 14 101 syl13anc ⊢ ( 𝜑 → ( ( 𝐿 − 𝑀 ) / 𝑀 ) ∈ 𝑅 )
103 9 20 sseldd ⊢ ( 𝜑 → 𝐾 ∈ 𝑅 )
104 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
105 104 a1i ⊢ ( 𝜑 → 1 ∈ ( 0 [,] 1 ) )
106 9 105 sseldd ⊢ ( 𝜑 → 1 ∈ 𝑅 )
107 98 8 clmsubcl ⊢ ( ( 𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅 ) → ( 1 − 𝐾 ) ∈ 𝑅 )
108 91 106 103 107 syl3anc ⊢ ( 𝜑 → ( 1 − 𝐾 ) ∈ 𝑅 )
109 98 8 cvsdivcl ⊢ ( ( 𝐻 ∈ ℂVec ∧ ( 𝐾 ∈ 𝑅 ∧ ( 1 − 𝐾 ) ∈ 𝑅 ∧ ( 1 − 𝐾 ) ≠ 0 ) ) → ( 𝐾 / ( 1 − 𝐾 ) ) ∈ 𝑅 )
110 11 103 108 44 109 syl13anc ⊢ ( 𝜑 → ( 𝐾 / ( 1 − 𝐾 ) ) ∈ 𝑅 )
111 clmgrp ⊢ ( 𝐻 ∈ ℂMod → 𝐻 ∈ Grp )
112 91 111 syl ⊢ ( 𝜑 → 𝐻 ∈ Grp )
113 3 4 grpsubcl ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ) → ( 𝑌 − 𝑋 ) ∈ 𝑃 )
114 112 7 6 113 syl3anc ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ 𝑃 )
115 3 98 5 8 clmvsass ⊢ ( ( 𝐻 ∈ ℂMod ∧ ( ( ( 𝐿 − 𝑀 ) / 𝑀 ) ∈ 𝑅 ∧ ( 𝐾 / ( 1 − 𝐾 ) ) ∈ 𝑅 ∧ ( 𝑌 − 𝑋 ) ∈ 𝑃 ) ) → ( ( ( ( 𝐿 − 𝑀 ) / 𝑀 ) · ( 𝐾 / ( 1 − 𝐾 ) ) ) · ( 𝑌 − 𝑋 ) ) = ( ( ( 𝐿 − 𝑀 ) / 𝑀 ) · ( ( 𝐾 / ( 1 − 𝐾 ) ) · ( 𝑌 − 𝑋 ) ) ) )
116 91 102 110 114 115 syl13anc ⊢ ( 𝜑 → ( ( ( ( 𝐿 − 𝑀 ) / 𝑀 ) · ( 𝐾 / ( 1 − 𝐾 ) ) ) · ( 𝑌 − 𝑋 ) ) = ( ( ( 𝐿 − 𝑀 ) / 𝑀 ) · ( ( 𝐾 / ( 1 − 𝐾 ) ) · ( 𝑌 − 𝑋 ) ) ) )
117 63 recnd ⊢ ( 𝜑 → ( 𝐿 − 𝑀 ) ∈ ℂ )
118 117 38 40 42 14 44 divmuldivd ⊢ ( 𝜑 → ( ( ( 𝐿 − 𝑀 ) / 𝑀 ) · ( 𝐾 / ( 1 − 𝐾 ) ) ) = ( ( ( 𝐿 − 𝑀 ) · 𝐾 ) / ( 𝑀 · ( 1 − 𝐾 ) ) ) )
119 72 41 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐿 − 𝑀 ) · 𝐾 ) / ( 𝑀 · ( 1 − 𝐾 ) ) ) = ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) )
120 118 119 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐿 − 𝑀 ) / 𝑀 ) · ( 𝐾 / ( 1 − 𝐾 ) ) ) = ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) )
121 120 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐿 − 𝑀 ) / 𝑀 ) · ( 𝐾 / ( 1 − 𝐾 ) ) ) · ( 𝑌 − 𝑋 ) ) = ( ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) · ( 𝑌 − 𝑋 ) ) )
122 3 4 grpsubcl ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃 ) → ( 𝑋 − 𝐴 ) ∈ 𝑃 )
123 112 6 12 122 syl3anc ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ 𝑃 )
124 22 oveq2d ⊢ ( 𝜑 → ( ( 1 − 𝐾 ) · ( 𝑋 − 𝐴 ) ) = ( ( 1 − 𝐾 ) · ( 𝐾 · ( 𝑌 − 𝐴 ) ) ) )
125 40 42 mulcomd ⊢ ( 𝜑 → ( 𝐾 · ( 1 − 𝐾 ) ) = ( ( 1 − 𝐾 ) · 𝐾 ) )
126 125 oveq1d ⊢ ( 𝜑 → ( ( 𝐾 · ( 1 − 𝐾 ) ) · ( 𝑌 − 𝐴 ) ) = ( ( ( 1 − 𝐾 ) · 𝐾 ) · ( 𝑌 − 𝐴 ) ) )
127 3 4 grpsubcl ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑌 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃 ) → ( 𝑌 − 𝐴 ) ∈ 𝑃 )
128 112 7 12 127 syl3anc ⊢ ( 𝜑 → ( 𝑌 − 𝐴 ) ∈ 𝑃 )
129 3 98 5 8 clmvsass ⊢ ( ( 𝐻 ∈ ℂMod ∧ ( 𝐾 ∈ 𝑅 ∧ ( 1 − 𝐾 ) ∈ 𝑅 ∧ ( 𝑌 − 𝐴 ) ∈ 𝑃 ) ) → ( ( 𝐾 · ( 1 − 𝐾 ) ) · ( 𝑌 − 𝐴 ) ) = ( 𝐾 · ( ( 1 − 𝐾 ) · ( 𝑌 − 𝐴 ) ) ) )
130 91 103 108 128 129 syl13anc ⊢ ( 𝜑 → ( ( 𝐾 · ( 1 − 𝐾 ) ) · ( 𝑌 − 𝐴 ) ) = ( 𝐾 · ( ( 1 − 𝐾 ) · ( 𝑌 − 𝐴 ) ) ) )
131 3 98 5 8 clmvsass ⊢ ( ( 𝐻 ∈ ℂMod ∧ ( ( 1 − 𝐾 ) ∈ 𝑅 ∧ 𝐾 ∈ 𝑅 ∧ ( 𝑌 − 𝐴 ) ∈ 𝑃 ) ) → ( ( ( 1 − 𝐾 ) · 𝐾 ) · ( 𝑌 − 𝐴 ) ) = ( ( 1 − 𝐾 ) · ( 𝐾 · ( 𝑌 − 𝐴 ) ) ) )
132 91 108 103 128 131 syl13anc ⊢ ( 𝜑 → ( ( ( 1 − 𝐾 ) · 𝐾 ) · ( 𝑌 − 𝐴 ) ) = ( ( 1 − 𝐾 ) · ( 𝐾 · ( 𝑌 − 𝐴 ) ) ) )
133 126 130 132 3eqtr3d ⊢ ( 𝜑 → ( 𝐾 · ( ( 1 − 𝐾 ) · ( 𝑌 − 𝐴 ) ) ) = ( ( 1 − 𝐾 ) · ( 𝐾 · ( 𝑌 − 𝐴 ) ) ) )
134 eqid ⊢ ( -g ‘ ( Scalar ‘ 𝐻 ) ) = ( -g ‘ ( Scalar ‘ 𝐻 ) )
135 clmlmod ⊢ ( 𝐻 ∈ ℂMod → 𝐻 ∈ LMod )
136 91 135 syl ⊢ ( 𝜑 → 𝐻 ∈ LMod )
137 3 5 98 8 4 134 136 106 103 128 lmodsubdir ⊢ ( 𝜑 → ( ( 1 ( -g ‘ ( Scalar ‘ 𝐻 ) ) 𝐾 ) · ( 𝑌 − 𝐴 ) ) = ( ( 1 · ( 𝑌 − 𝐴 ) ) − ( 𝐾 · ( 𝑌 − 𝐴 ) ) ) )
138 98 8 clmsub ⊢ ( ( 𝐻 ∈ ℂMod ∧ 1 ∈ 𝑅 ∧ 𝐾 ∈ 𝑅 ) → ( 1 − 𝐾 ) = ( 1 ( -g ‘ ( Scalar ‘ 𝐻 ) ) 𝐾 ) )
139 91 106 103 138 syl3anc ⊢ ( 𝜑 → ( 1 − 𝐾 ) = ( 1 ( -g ‘ ( Scalar ‘ 𝐻 ) ) 𝐾 ) )
140 139 oveq1d ⊢ ( 𝜑 → ( ( 1 − 𝐾 ) · ( 𝑌 − 𝐴 ) ) = ( ( 1 ( -g ‘ ( Scalar ‘ 𝐻 ) ) 𝐾 ) · ( 𝑌 − 𝐴 ) ) )
141 3 5 clmvs1 ⊢ ( ( 𝐻 ∈ ℂMod ∧ ( 𝑌 − 𝐴 ) ∈ 𝑃 ) → ( 1 · ( 𝑌 − 𝐴 ) ) = ( 𝑌 − 𝐴 ) )
142 91 128 141 syl2anc ⊢ ( 𝜑 → ( 1 · ( 𝑌 − 𝐴 ) ) = ( 𝑌 − 𝐴 ) )
143 142 eqcomd ⊢ ( 𝜑 → ( 𝑌 − 𝐴 ) = ( 1 · ( 𝑌 − 𝐴 ) ) )
144 143 22 oveq12d ⊢ ( 𝜑 → ( ( 𝑌 − 𝐴 ) − ( 𝑋 − 𝐴 ) ) = ( ( 1 · ( 𝑌 − 𝐴 ) ) − ( 𝐾 · ( 𝑌 − 𝐴 ) ) ) )
145 137 140 144 3eqtr4d ⊢ ( 𝜑 → ( ( 1 − 𝐾 ) · ( 𝑌 − 𝐴 ) ) = ( ( 𝑌 − 𝐴 ) − ( 𝑋 − 𝐴 ) ) )
146 3 4 grpnnncan2 ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃 ) ) → ( ( 𝑌 − 𝐴 ) − ( 𝑋 − 𝐴 ) ) = ( 𝑌 − 𝑋 ) )
147 112 7 6 12 146 syl13anc ⊢ ( 𝜑 → ( ( 𝑌 − 𝐴 ) − ( 𝑋 − 𝐴 ) ) = ( 𝑌 − 𝑋 ) )
148 145 147 eqtrd ⊢ ( 𝜑 → ( ( 1 − 𝐾 ) · ( 𝑌 − 𝐴 ) ) = ( 𝑌 − 𝑋 ) )
149 148 oveq2d ⊢ ( 𝜑 → ( 𝐾 · ( ( 1 − 𝐾 ) · ( 𝑌 − 𝐴 ) ) ) = ( 𝐾 · ( 𝑌 − 𝑋 ) ) )
150 124 133 149 3eqtr2rd ⊢ ( 𝜑 → ( 𝐾 · ( 𝑌 − 𝑋 ) ) = ( ( 1 − 𝐾 ) · ( 𝑋 − 𝐴 ) ) )
151 3 5 98 8 11 103 108 114 123 15 150 cvsmuleqdivd ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) = ( ( ( 1 − 𝐾 ) / 𝐾 ) · ( 𝑋 − 𝐴 ) ) )
152 3 5 98 8 11 108 103 114 123 44 15 151 cvsdiveqd ⊢ ( 𝜑 → ( ( 𝐾 / ( 1 − 𝐾 ) ) · ( 𝑌 − 𝑋 ) ) = ( 𝑋 − 𝐴 ) )
153 152 123 eqeltrd ⊢ ( 𝜑 → ( ( 𝐾 / ( 1 − 𝐾 ) ) · ( 𝑌 − 𝑋 ) ) ∈ 𝑃 )
154 3 4 grpsubcl ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑁 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃 ) → ( 𝑁 − 𝐴 ) ∈ 𝑃 )
155 112 13 12 154 syl3anc ⊢ ( 𝜑 → ( 𝑁 − 𝐴 ) ∈ 𝑃 )
156 3 98 5 8 lmodvscl ⊢ ( ( 𝐻 ∈ LMod ∧ 𝐿 ∈ 𝑅 ∧ ( 𝑁 − 𝐴 ) ∈ 𝑃 ) → ( 𝐿 · ( 𝑁 − 𝐴 ) ) ∈ 𝑃 )
157 136 92 155 156 syl3anc ⊢ ( 𝜑 → ( 𝐿 · ( 𝑁 − 𝐴 ) ) ∈ 𝑃 )
158 3 10 grpcl ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐴 ∈ 𝑃 ∧ ( 𝐿 · ( 𝑁 − 𝐴 ) ) ∈ 𝑃 ) → ( 𝐴 + ( 𝐿 · ( 𝑁 − 𝐴 ) ) ) ∈ 𝑃 )
159 112 12 157 158 syl3anc ⊢ ( 𝜑 → ( 𝐴 + ( 𝐿 · ( 𝑁 − 𝐴 ) ) ) ∈ 𝑃 )
160 24 159 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
161 3 4 grpsubcl ⊢ ( ( 𝐻 ∈ Grp ∧ 𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ) → ( 𝐵 − 𝑋 ) ∈ 𝑃 )
162 112 160 6 161 syl3anc ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ 𝑃 )
163 71 38 17 subne0d ⊢ ( 𝜑 → ( 𝐿 − 𝑀 ) ≠ 0 )
164 23 oveq2d ⊢ ( 𝜑 → ( ( 𝐿 − 𝑀 ) · ( 𝑋 − 𝐴 ) ) = ( ( 𝐿 − 𝑀 ) · ( 𝑀 · ( 𝑁 − 𝐴 ) ) ) )
165 38 117 mulcomd ⊢ ( 𝜑 → ( 𝑀 · ( 𝐿 − 𝑀 ) ) = ( ( 𝐿 − 𝑀 ) · 𝑀 ) )
166 165 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 · ( 𝐿 − 𝑀 ) ) · ( 𝑁 − 𝐴 ) ) = ( ( ( 𝐿 − 𝑀 ) · 𝑀 ) · ( 𝑁 − 𝐴 ) ) )
167 3 98 5 8 clmvsass ⊢ ( ( 𝐻 ∈ ℂMod ∧ ( 𝑀 ∈ 𝑅 ∧ ( 𝐿 − 𝑀 ) ∈ 𝑅 ∧ ( 𝑁 − 𝐴 ) ∈ 𝑃 ) ) → ( ( 𝑀 · ( 𝐿 − 𝑀 ) ) · ( 𝑁 − 𝐴 ) ) = ( 𝑀 · ( ( 𝐿 − 𝑀 ) · ( 𝑁 − 𝐴 ) ) ) )
168 91 97 100 155 167 syl13anc ⊢ ( 𝜑 → ( ( 𝑀 · ( 𝐿 − 𝑀 ) ) · ( 𝑁 − 𝐴 ) ) = ( 𝑀 · ( ( 𝐿 − 𝑀 ) · ( 𝑁 − 𝐴 ) ) ) )
169 3 98 5 8 clmvsass ⊢ ( ( 𝐻 ∈ ℂMod ∧ ( ( 𝐿 − 𝑀 ) ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ∧ ( 𝑁 − 𝐴 ) ∈ 𝑃 ) ) → ( ( ( 𝐿 − 𝑀 ) · 𝑀 ) · ( 𝑁 − 𝐴 ) ) = ( ( 𝐿 − 𝑀 ) · ( 𝑀 · ( 𝑁 − 𝐴 ) ) ) )
170 91 100 97 155 169 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐿 − 𝑀 ) · 𝑀 ) · ( 𝑁 − 𝐴 ) ) = ( ( 𝐿 − 𝑀 ) · ( 𝑀 · ( 𝑁 − 𝐴 ) ) ) )
171 166 168 170 3eqtr3d ⊢ ( 𝜑 → ( 𝑀 · ( ( 𝐿 − 𝑀 ) · ( 𝑁 − 𝐴 ) ) ) = ( ( 𝐿 − 𝑀 ) · ( 𝑀 · ( 𝑁 − 𝐴 ) ) ) )
172 3 5 98 8 4 134 136 92 97 155 lmodsubdir ⊢ ( 𝜑 → ( ( 𝐿 ( -g ‘ ( Scalar ‘ 𝐻 ) ) 𝑀 ) · ( 𝑁 − 𝐴 ) ) = ( ( 𝐿 · ( 𝑁 − 𝐴 ) ) − ( 𝑀 · ( 𝑁 − 𝐴 ) ) ) )
173 98 8 clmsub ⊢ ( ( 𝐻 ∈ ℂMod ∧ 𝐿 ∈ 𝑅 ∧ 𝑀 ∈ 𝑅 ) → ( 𝐿 − 𝑀 ) = ( 𝐿 ( -g ‘ ( Scalar ‘ 𝐻 ) ) 𝑀 ) )
174 91 92 97 173 syl3anc ⊢ ( 𝜑 → ( 𝐿 − 𝑀 ) = ( 𝐿 ( -g ‘ ( Scalar ‘ 𝐻 ) ) 𝑀 ) )
175 174 oveq1d ⊢ ( 𝜑 → ( ( 𝐿 − 𝑀 ) · ( 𝑁 − 𝐴 ) ) = ( ( 𝐿 ( -g ‘ ( Scalar ‘ 𝐻 ) ) 𝑀 ) · ( 𝑁 − 𝐴 ) ) )
176 24 oveq1d ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( 𝐴 + ( 𝐿 · ( 𝑁 − 𝐴 ) ) ) − 𝐴 ) )
177 lmodabl ⊢ ( 𝐻 ∈ LMod → 𝐻 ∈ Abel )
178 136 177 syl ⊢ ( 𝜑 → 𝐻 ∈ Abel )
179 3 10 4 ablpncan2 ⊢ ( ( 𝐻 ∈ Abel ∧ 𝐴 ∈ 𝑃 ∧ ( 𝐿 · ( 𝑁 − 𝐴 ) ) ∈ 𝑃 ) → ( ( 𝐴 + ( 𝐿 · ( 𝑁 − 𝐴 ) ) ) − 𝐴 ) = ( 𝐿 · ( 𝑁 − 𝐴 ) ) )
180 178 12 157 179 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐿 · ( 𝑁 − 𝐴 ) ) ) − 𝐴 ) = ( 𝐿 · ( 𝑁 − 𝐴 ) ) )
181 176 180 eqtrd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐿 · ( 𝑁 − 𝐴 ) ) )
182 181 23 oveq12d ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) − ( 𝑋 − 𝐴 ) ) = ( ( 𝐿 · ( 𝑁 − 𝐴 ) ) − ( 𝑀 · ( 𝑁 − 𝐴 ) ) ) )
183 172 175 182 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐿 − 𝑀 ) · ( 𝑁 − 𝐴 ) ) = ( ( 𝐵 − 𝐴 ) − ( 𝑋 − 𝐴 ) ) )
184 3 4 grpnnncan2 ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝐵 ∈ 𝑃 ∧ 𝑋 ∈ 𝑃 ∧ 𝐴 ∈ 𝑃 ) ) → ( ( 𝐵 − 𝐴 ) − ( 𝑋 − 𝐴 ) ) = ( 𝐵 − 𝑋 ) )
185 112 160 6 12 184 syl13anc ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) − ( 𝑋 − 𝐴 ) ) = ( 𝐵 − 𝑋 ) )
186 183 185 eqtrd ⊢ ( 𝜑 → ( ( 𝐿 − 𝑀 ) · ( 𝑁 − 𝐴 ) ) = ( 𝐵 − 𝑋 ) )
187 186 oveq2d ⊢ ( 𝜑 → ( 𝑀 · ( ( 𝐿 − 𝑀 ) · ( 𝑁 − 𝐴 ) ) ) = ( 𝑀 · ( 𝐵 − 𝑋 ) ) )
188 164 171 187 3eqtr2rd ⊢ ( 𝜑 → ( 𝑀 · ( 𝐵 − 𝑋 ) ) = ( ( 𝐿 − 𝑀 ) · ( 𝑋 − 𝐴 ) ) )
189 3 5 98 8 11 97 100 162 123 14 188 cvsmuleqdivd ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) = ( ( ( 𝐿 − 𝑀 ) / 𝑀 ) · ( 𝑋 − 𝐴 ) ) )
190 3 5 98 8 11 100 97 162 123 163 14 189 cvsdiveqd ⊢ ( 𝜑 → ( ( 𝑀 / ( 𝐿 − 𝑀 ) ) · ( 𝐵 − 𝑋 ) ) = ( 𝑋 − 𝐴 ) )
191 152 190 eqtr4d ⊢ ( 𝜑 → ( ( 𝐾 / ( 1 − 𝐾 ) ) · ( 𝑌 − 𝑋 ) ) = ( ( 𝑀 / ( 𝐿 − 𝑀 ) ) · ( 𝐵 − 𝑋 ) ) )
192 3 5 98 8 11 97 100 153 162 14 163 191 cvsdiveqd ⊢ ( 𝜑 → ( ( ( 𝐿 − 𝑀 ) / 𝑀 ) · ( ( 𝐾 / ( 1 − 𝐾 ) ) · ( 𝑌 − 𝑋 ) ) ) = ( 𝐵 − 𝑋 ) )
193 116 121 192 3eqtr3rd ⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) = ( ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) · ( 𝑌 − 𝑋 ) ) )
194 oveq1 ⊢ ( 𝑘 = ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) → ( 𝑘 · ( 𝑌 − 𝑋 ) ) = ( ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) · ( 𝑌 − 𝑋 ) ) )
195 194 rspceeqv ⊢ ( ( ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) ∈ ( 0 [,] 1 ) ∧ ( 𝐵 − 𝑋 ) = ( ( ( ( 𝐿 · 𝐾 ) − ( 𝑀 · 𝐾 ) ) / ( ( 𝑀 · 1 ) − ( 𝑀 · 𝐾 ) ) ) · ( 𝑌 − 𝑋 ) ) ) → ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝐵 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) )
196 90 193 195 syl2anc ⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝐵 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) )
197 1 2 3 4 5 6 7 11 160 ttgelitv ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ( 𝐵 − 𝑋 ) = ( 𝑘 · ( 𝑌 − 𝑋 ) ) ) )
198 196 197 mpbird ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 𝐼 𝑌 ) )