ttgcontlem1

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

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

Proof

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

Metamath Proof Explorer

Theorem ttgcontlem1

Proof