axsegconlem1

Description: Lemma for axsegcon . Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013)

		Ref	Expression
	Assertion	axsegconlem1	$⊢ (A = B \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$

Proof

Step	Hyp	Ref	Expression
1		fveere	$⊢ (B \in 𝔼 (N) \land k \in (1 \dots N)) \to B (k) \in ℝ$
2	1	3ad2antl1	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land k \in (1 \dots N)) \to B (k) \in ℝ$
3		fveere	$⊢ (C \in 𝔼 (N) \land k \in (1 \dots N)) \to C (k) \in ℝ$
4	3	3ad2antl2	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land k \in (1 \dots N)) \to C (k) \in ℝ$
5		fveere	$⊢ (D \in 𝔼 (N) \land k \in (1 \dots N)) \to D (k) \in ℝ$
6	5	3ad2antl3	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land k \in (1 \dots N)) \to D (k) \in ℝ$
7	4 6	resubcld	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land k \in (1 \dots N)) \to C (k) - D (k) \in ℝ$
8	2 7	resubcld	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land k \in (1 \dots N)) \to B (k) - (C (k) - D (k)) \in ℝ$
9	8	ralrimiva	$⊢ (B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \to \forall k \in (1 \dots N) B (k) - (C (k) - D (k)) \in ℝ$
10		eleenn	$⊢ B \in 𝔼 (N) \to N \in ℕ$
11		mptelee	$⊢ N \in ℕ \to ((k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \in 𝔼 (N) \leftrightarrow \forall k \in (1 \dots N) B (k) - (C (k) - D (k)) \in ℝ)$
12	10 11	syl	$⊢ B \in 𝔼 (N) \to ((k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \in 𝔼 (N) \leftrightarrow \forall k \in (1 \dots N) B (k) - (C (k) - D (k)) \in ℝ)$
13	12	3ad2ant1	$⊢ (B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \to ((k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \in 𝔼 (N) \leftrightarrow \forall k \in (1 \dots N) B (k) - (C (k) - D (k)) \in ℝ)$
14	9 13	mpbird	$⊢ (B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \to (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \in 𝔼 (N)$
15		fveecn	$⊢ (B \in 𝔼 (N) \land i \in (1 \dots N)) \to B (i) \in ℂ$
16	15	3ad2antl1	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land i \in (1 \dots N)) \to B (i) \in ℂ$
17		fveecn	$⊢ (C \in 𝔼 (N) \land i \in (1 \dots N)) \to C (i) \in ℂ$
18	17	3ad2antl2	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land i \in (1 \dots N)) \to C (i) \in ℂ$
19		fveecn	$⊢ (D \in 𝔼 (N) \land i \in (1 \dots N)) \to D (i) \in ℂ$
20	19	3ad2antl3	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land i \in (1 \dots N)) \to D (i) \in ℂ$
21		1m0e1	$⊢ 1 - 0 = 1$
22	21	oveq1i	$⊢ (1 - 0) B (i) = 1 B (i)$
23		mullid	$⊢ B (i) \in ℂ \to 1 B (i) = B (i)$
24	23	3ad2ant1	$⊢ (B (i) \in ℂ \land C (i) \in ℂ \land D (i) \in ℂ) \to 1 B (i) = B (i)$
25	22 24	eqtrid	$⊢ (B (i) \in ℂ \land C (i) \in ℂ \land D (i) \in ℂ) \to (1 - 0) B (i) = B (i)$
26		subcl	$⊢ (C (i) \in ℂ \land D (i) \in ℂ) \to C (i) - D (i) \in ℂ$
27		subcl	$⊢ (B (i) \in ℂ \land C (i) - D (i) \in ℂ) \to B (i) - (C (i) - D (i)) \in ℂ$
28	26 27	sylan2	$⊢ (B (i) \in ℂ \land (C (i) \in ℂ \land D (i) \in ℂ)) \to B (i) - (C (i) - D (i)) \in ℂ$
29	28	3impb	$⊢ (B (i) \in ℂ \land C (i) \in ℂ \land D (i) \in ℂ) \to B (i) - (C (i) - D (i)) \in ℂ$
30	29	mul02d	$⊢ (B (i) \in ℂ \land C (i) \in ℂ \land D (i) \in ℂ) \to 0 \cdot (B (i) - (C (i) - D (i))) = 0$
31	25 30	oveq12d	$⊢ (B (i) \in ℂ \land C (i) \in ℂ \land D (i) \in ℂ) \to (1 - 0) B (i) + 0 \cdot (B (i) - (C (i) - D (i))) = B (i) + 0$
32		addrid	$⊢ B (i) \in ℂ \to B (i) + 0 = B (i)$
33	32	3ad2ant1	$⊢ (B (i) \in ℂ \land C (i) \in ℂ \land D (i) \in ℂ) \to B (i) + 0 = B (i)$
34	31 33	eqtr2d	$⊢ (B (i) \in ℂ \land C (i) \in ℂ \land D (i) \in ℂ) \to B (i) = (1 - 0) B (i) + 0 \cdot (B (i) - (C (i) - D (i)))$
35	16 18 20 34	syl3anc	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land i \in (1 \dots N)) \to B (i) = (1 - 0) B (i) + 0 \cdot (B (i) - (C (i) - D (i)))$
36	35	ralrimiva	$⊢ (B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \to \forall i \in (1 \dots N) B (i) = (1 - 0) B (i) + 0 \cdot (B (i) - (C (i) - D (i)))$
37	18 20	subcld	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land i \in (1 \dots N)) \to C (i) - D (i) \in ℂ$
38	16 37	nncand	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land i \in (1 \dots N)) \to B (i) - (B (i) - (C (i) - D (i))) = C (i) - D (i)$
39	38	oveq1d	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land i \in (1 \dots N)) \to {(B (i) - (B (i) - (C (i) - D (i))))}^{2} = {(C (i) - D (i))}^{2}$
40	39	sumeq2dv	$⊢ (B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \to \sum_{i = 1}^{N} {(B (i) - (B (i) - (C (i) - D (i))))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}$
41		0elunit	$⊢ 0 \in [0, 1]$
42		fveq1	$⊢ x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \to x (i) = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) (i)$
43		fveq2	$⊢ k = i \to B (k) = B (i)$
44		fveq2	$⊢ k = i \to C (k) = C (i)$
45		fveq2	$⊢ k = i \to D (k) = D (i)$
46	44 45	oveq12d	$⊢ k = i \to C (k) - D (k) = C (i) - D (i)$
47	43 46	oveq12d	$⊢ k = i \to B (k) - (C (k) - D (k)) = B (i) - (C (i) - D (i))$
48		eqid	$⊢ (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k)))$
49		ovex	$⊢ B (i) - (C (i) - D (i)) \in V$
50	47 48 49	fvmpt	$⊢ i \in (1 \dots N) \to (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) (i) = B (i) - (C (i) - D (i))$
51	42 50	sylan9eq	$⊢ (x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \land i \in (1 \dots N)) \to x (i) = B (i) - (C (i) - D (i))$
52	51	oveq2d	$⊢ (x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \land i \in (1 \dots N)) \to t x (i) = t (B (i) - (C (i) - D (i)))$
53	52	oveq2d	$⊢ (x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \land i \in (1 \dots N)) \to (1 - t) B (i) + t x (i) = (1 - t) B (i) + t (B (i) - (C (i) - D (i)))$
54	53	eqeq2d	$⊢ (x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \land i \in (1 \dots N)) \to (B (i) = (1 - t) B (i) + t x (i) \leftrightarrow B (i) = (1 - t) B (i) + t (B (i) - (C (i) - D (i))))$
55	54	ralbidva	$⊢ x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \to (\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t x (i) \leftrightarrow \forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t (B (i) - (C (i) - D (i))))$
56	51	oveq2d	$⊢ (x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \land i \in (1 \dots N)) \to B (i) - x (i) = B (i) - (B (i) - (C (i) - D (i)))$
57	56	oveq1d	$⊢ (x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \land i \in (1 \dots N)) \to {(B (i) - x (i))}^{2} = {(B (i) - (B (i) - (C (i) - D (i))))}^{2}$
58	57	sumeq2dv	$⊢ x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \to \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(B (i) - (B (i) - (C (i) - D (i))))}^{2}$
59	58	eqeq1d	$⊢ x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \to (\sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2} \leftrightarrow \sum_{i = 1}^{N} {(B (i) - (B (i) - (C (i) - D (i))))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
60	55 59	anbi12d	$⊢ x = (k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \to ((\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}) \leftrightarrow (\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t (B (i) - (C (i) - D (i))) \land \sum_{i = 1}^{N} {(B (i) - (B (i) - (C (i) - D (i))))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
61		oveq2	$⊢ t = 0 \to 1 - t = 1 - 0$
62	61	oveq1d	$⊢ t = 0 \to (1 - t) B (i) = (1 - 0) B (i)$
63		oveq1	$⊢ t = 0 \to t (B (i) - (C (i) - D (i))) = 0 \cdot (B (i) - (C (i) - D (i)))$
64	62 63	oveq12d	$⊢ t = 0 \to (1 - t) B (i) + t (B (i) - (C (i) - D (i))) = (1 - 0) B (i) + 0 \cdot (B (i) - (C (i) - D (i)))$
65	64	eqeq2d	$⊢ t = 0 \to (B (i) = (1 - t) B (i) + t (B (i) - (C (i) - D (i))) \leftrightarrow B (i) = (1 - 0) B (i) + 0 \cdot (B (i) - (C (i) - D (i))))$
66	65	ralbidv	$⊢ t = 0 \to (\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t (B (i) - (C (i) - D (i))) \leftrightarrow \forall i \in (1 \dots N) B (i) = (1 - 0) B (i) + 0 \cdot (B (i) - (C (i) - D (i))))$
67	66	anbi1d	$⊢ t = 0 \to ((\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t (B (i) - (C (i) - D (i))) \land \sum_{i = 1}^{N} {(B (i) - (B (i) - (C (i) - D (i))))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}) \leftrightarrow (\forall i \in (1 \dots N) B (i) = (1 - 0) B (i) + 0 \cdot (B (i) - (C (i) - D (i))) \land \sum_{i = 1}^{N} {(B (i) - (B (i) - (C (i) - D (i))))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
68	60 67	rspc2ev	$⊢ ((k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \in 𝔼 (N) \land 0 \in [0, 1] \land (\forall i \in (1 \dots N) B (i) = (1 - 0) B (i) + 0 \cdot (B (i) - (C (i) - D (i))) \land \sum_{i = 1}^{N} {(B (i) - (B (i) - (C (i) - D (i))))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
69	41 68	mp3an2	$⊢ ((k \in (1 \dots N) ⟼ B (k) - (C (k) - D (k))) \in 𝔼 (N) \land (\forall i \in (1 \dots N) B (i) = (1 - 0) B (i) + 0 \cdot (B (i) - (C (i) - D (i))) \land \sum_{i = 1}^{N} {(B (i) - (B (i) - (C (i) - D (i))))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
70	14 36 40 69	syl12anc	$⊢ (B \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
71	70	3expb	$⊢ (B \in 𝔼 (N) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
72	71	adantll	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$
73		fveq1	$⊢ A = B \to A (i) = B (i)$
74	73	oveq2d	$⊢ A = B \to (1 - t) A (i) = (1 - t) B (i)$
75	74	oveq1d	$⊢ A = B \to (1 - t) A (i) + t x (i) = (1 - t) B (i) + t x (i)$
76	75	eqeq2d	$⊢ A = B \to (B (i) = (1 - t) A (i) + t x (i) \leftrightarrow B (i) = (1 - t) B (i) + t x (i))$
77	76	ralbidv	$⊢ A = B \to (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \leftrightarrow \forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t x (i))$
78	77	anbi1d	$⊢ A = B \to ((\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}) \leftrightarrow (\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
79	78	2rexbidv	$⊢ A = B \to (\exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}) \leftrightarrow \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) B (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
80	72 79	imbitrrid	$⊢ A = B \to (((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2}))$
81	80	imp	$⊢ (A = B \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to \exists x \in 𝔼 (N) \exists t \in [0, 1] (\forall i \in (1 \dots N) B (i) = (1 - t) A (i) + t x (i) \land \sum_{i = 1}^{N} {(B (i) - x (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$

Metamath Proof Explorer

Theorem axsegconlem1

Proof