# Metamath Proof Explorer

## Theorem ttgcontlem1

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

Ref Expression
Hypotheses ttgval.n ${⊢}{G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
ttgitvval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
ttgitvval.b ${⊢}{P}={\mathrm{Base}}_{{H}}$
ttgitvval.m
ttgitvval.s
ttgelitv.x ${⊢}{\phi }\to {X}\in {P}$
ttgelitv.y ${⊢}{\phi }\to {Y}\in {P}$
ttgbtwnid.r ${⊢}{R}={\mathrm{Base}}_{\mathrm{Scalar}\left({H}\right)}$
ttgbtwnid.2 ${⊢}{\phi }\to \left[0,1\right]\subseteq {R}$
ttgitvval.p
ttgcontlem1.h ${⊢}{\phi }\to {H}\in \mathrm{ℂVec}$
ttgcontlem1.a ${⊢}{\phi }\to {A}\in {P}$
ttgcontlem1.n ${⊢}{\phi }\to {N}\in {P}$
ttgcontlem1.o ${⊢}{\phi }\to {M}\ne 0$
ttgcontlem1.p ${⊢}{\phi }\to {K}\ne 0$
ttgcontlem1.q ${⊢}{\phi }\to {K}\ne 1$
ttgcontlem1.r ${⊢}{\phi }\to {L}\ne {M}$
ttgcontlem1.s ${⊢}{\phi }\to {L}\le \frac{{M}}{{K}}$
ttgcontlem1.l ${⊢}{\phi }\to {L}\in \left[0,1\right]$
ttgcontlem1.k ${⊢}{\phi }\to {K}\in \left[0,1\right]$
ttgcontlem1.m ${⊢}{\phi }\to {M}\in \left[0,{L}\right]$
ttgcontlem1.y
ttgcontlem1.x
ttgcontlem1.b
Assertion ttgcontlem1 ${⊢}{\phi }\to {B}\in \left({X}{I}{Y}\right)$

### Proof

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