ax5seglem9

Description: Lemma for ax5seg . Take the calculation in ax5seglem8 and turn it into a series of measurements. (Contributed by Scott Fenton, 12-Jun-2013) (Revised by Mario Carneiro, 22-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simprll	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to A \in 𝔼 (N)$
2	1	ad2antrr	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to A \in 𝔼 (N)$
3		fveecn	$⊢ (A \in 𝔼 (N) \land j \in (1 \dots N)) \to A (j) \in ℂ$
4	2 3	sylancom	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to A (j) \in ℂ$
5		elicc01	$⊢ T \in [0, 1] \leftrightarrow (T \in ℝ \land 0 \leq T \land T \leq 1)$
6	5	simp1bi	$⊢ T \in [0, 1] \to T \in ℝ$
7	6	recnd	$⊢ T \in [0, 1] \to T \in ℂ$
8	7	ad2antrl	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to T \in ℂ$
9	8	adantr	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to T \in ℂ$
10		simprrl	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to C \in 𝔼 (N)$
11	10	ad2antrr	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to C \in 𝔼 (N)$
12		fveecn	$⊢ (C \in 𝔼 (N) \land j \in (1 \dots N)) \to C (j) \in ℂ$
13	11 12	sylancom	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to C (j) \in ℂ$
14		simprrr	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to D \in 𝔼 (N)$
15	14	ad2antrr	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to D \in 𝔼 (N)$
16		fveecn	$⊢ (D \in 𝔼 (N) \land j \in (1 \dots N)) \to D (j) \in ℂ$
17	15 16	sylancom	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to D (j) \in ℂ$
18		fveq2	$⊢ i = j \to B (i) = B (j)$
19		fveq2	$⊢ i = j \to A (i) = A (j)$
20	19	oveq2d	$⊢ i = j \to (1 - T) A (i) = (1 - T) A (j)$
21		fveq2	$⊢ i = j \to C (i) = C (j)$
22	21	oveq2d	$⊢ i = j \to T C (i) = T C (j)$
23	20 22	oveq12d	$⊢ i = j \to (1 - T) A (i) + T C (i) = (1 - T) A (j) + T C (j)$
24	18 23	eqeq12d	$⊢ i = j \to (B (i) = (1 - T) A (i) + T C (i) \leftrightarrow B (j) = (1 - T) A (j) + T C (j))$
25	24	rspccva	$⊢ (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land j \in (1 \dots N)) \to B (j) = (1 - T) A (j) + T C (j)$
26	25	adantll	$⊢ ((T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i)) \land j \in (1 \dots N)) \to B (j) = (1 - T) A (j) + T C (j)$
27	26	adantll	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to B (j) = (1 - T) A (j) + T C (j)$
28		ax5seglem8	$⊢ ((A (j) \in ℂ \land T \in ℂ) \land (C (j) \in ℂ \land D (j) \in ℂ)) \to T {(C (j) - D (j))}^{2} = {((1 - T) A (j) + T C (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
29		oveq1	$⊢ B (j) = (1 - T) A (j) + T C (j) \to B (j) - D (j) = (1 - T) A (j) + T C (j) - D (j)$
30	29	oveq1d	$⊢ B (j) = (1 - T) A (j) + T C (j) \to {(B (j) - D (j))}^{2} = {((1 - T) A (j) + T C (j) - D (j))}^{2}$
31	30	oveq1d	$⊢ B (j) = (1 - T) A (j) + T C (j) \to {(B (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2}) = {((1 - T) A (j) + T C (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
32	31	eqcomd	$⊢ B (j) = (1 - T) A (j) + T C (j) \to {((1 - T) A (j) + T C (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2}) = {(B (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
33	28 32	sylan9eq	$⊢ (((A (j) \in ℂ \land T \in ℂ) \land (C (j) \in ℂ \land D (j) \in ℂ)) \land B (j) = (1 - T) A (j) + T C (j)) \to T {(C (j) - D (j))}^{2} = {(B (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
34	33	3impa	$⊢ ((A (j) \in ℂ \land T \in ℂ) \land (C (j) \in ℂ \land D (j) \in ℂ) \land B (j) = (1 - T) A (j) + T C (j)) \to T {(C (j) - D (j))}^{2} = {(B (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
35	4 9 13 17 27 34	syl221anc	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to T {(C (j) - D (j))}^{2} = {(B (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
36	35	sumeq2dv	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to \sum_{j = 1}^{N} T {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} ({(B (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2}))$
37		fzfid	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to (1 \dots N) \in Fin$
38	13 17	subcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to C (j) - D (j) \in ℂ$
39	38	sqcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to {(C (j) - D (j))}^{2} \in ℂ$
40	37 8 39	fsummulc2	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to T \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} T {(C (j) - D (j))}^{2}$
41	4 13	subcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to A (j) - C (j) \in ℂ$
42	41	sqcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to {(A (j) - C (j))}^{2} \in ℂ$
43	37 8 42	fsummulc2	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to T \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = \sum_{j = 1}^{N} T {(A (j) - C (j))}^{2}$
44	43	oveq1d	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to T \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2} = \sum_{j = 1}^{N} T {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2}$
45	9 42	mulcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to T {(A (j) - C (j))}^{2} \in ℂ$
46	4 17	subcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to A (j) - D (j) \in ℂ$
47	46	sqcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to {(A (j) - D (j))}^{2} \in ℂ$
48	37 45 47	fsumsub	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to \sum_{j = 1}^{N} (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2}) = \sum_{j = 1}^{N} T {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2}$
49	44 48	eqtr4d	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to T \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2} = \sum_{j = 1}^{N} (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
50	49	oveq2d	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to (1 - T) (T \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2}) = (1 - T) \sum_{j = 1}^{N} (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
51		ax-1cn	$⊢ 1 \in ℂ$
52		subcl	$⊢ (1 \in ℂ \land T \in ℂ) \to 1 - T \in ℂ$
53	51 8 52	sylancr	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to 1 - T \in ℂ$
54	45 47	subcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2} \in ℂ$
55	37 53 54	fsummulc2	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to (1 - T) \sum_{j = 1}^{N} (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2}) = \sum_{j = 1}^{N} (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
56	50 55	eqtrd	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to (1 - T) (T \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2}) = \sum_{j = 1}^{N} (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
57	56	oveq2d	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} + (1 - T) (T \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2}) = \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} + \sum_{j = 1}^{N} (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
58		simprlr	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \to B \in 𝔼 (N)$
59	58	ad2antrr	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to B \in 𝔼 (N)$
60		fveecn	$⊢ (B \in 𝔼 (N) \land j \in (1 \dots N)) \to B (j) \in ℂ$
61	59 60	sylancom	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to B (j) \in ℂ$
62	61 17	subcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to B (j) - D (j) \in ℂ$
63	62	sqcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to {(B (j) - D (j))}^{2} \in ℂ$
64	51 9 52	sylancr	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to 1 - T \in ℂ$
65	64 54	mulcld	$⊢ (((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2}) \in ℂ$
66	37 63 65	fsumadd	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to \sum_{j = 1}^{N} ({(B (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})) = \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} + \sum_{j = 1}^{N} (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2})$
67	57 66	eqtr4d	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} + (1 - T) (T \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2}) = \sum_{j = 1}^{N} ({(B (j) - D (j))}^{2} + (1 - T) (T {(A (j) - C (j))}^{2} - {(A (j) - D (j))}^{2}))$
68	36 40 67	3eqtr4d	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)))) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to T \sum_{j = 1}^{N} {(C (j) - D (j))}^{2} = \sum_{j = 1}^{N} {(B (j) - D (j))}^{2} + (1 - T) (T \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} - \sum_{j = 1}^{N} {(A (j) - D (j))}^{2})$

Metamath Proof Explorer

Theorem ax5seglem9

Proof