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