ax5seglem1

Description: Lemma for ax5seg . Rexpress a one congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013)

		Ref	Expression
	Assertion	ax5seglem1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \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} {(A (j) - B (j))}^{2} = T^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$

Proof

Step	Hyp	Ref	Expression
1		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \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)$
2		fveecn	$⊢ (A \in 𝔼 (N) \land j \in (1 \dots N)) \to A (j) \in ℂ$
3	1 2	sylancom	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \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 ℂ$
4		simpl2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \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)$
5		fveecn	$⊢ (C \in 𝔼 (N) \land j \in (1 \dots N)) \to C (j) \in ℂ$
6	4 5	sylancom	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \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 ℂ$
7		elicc01	$⊢ T \in [0, 1] \leftrightarrow (T \in ℝ \land 0 \leq T \land T \leq 1)$
8	7	simp1bi	$⊢ T \in [0, 1] \to T \in ℝ$
9	8	adantr	$⊢ (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i)) \to T \in ℝ$
10	9	3ad2ant3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \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 ℝ$
11	10	recnd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \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 ℂ$
12	11	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \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 ℂ$
13		fveq2	$⊢ i = j \to B (i) = B (j)$
14		fveq2	$⊢ i = j \to A (i) = A (j)$
15	14	oveq2d	$⊢ i = j \to (1 - T) A (i) = (1 - T) A (j)$
16		fveq2	$⊢ i = j \to C (i) = C (j)$
17	16	oveq2d	$⊢ i = j \to T C (i) = T C (j)$
18	15 17	oveq12d	$⊢ i = j \to (1 - T) A (i) + T C (i) = (1 - T) A (j) + T C (j)$
19	13 18	eqeq12d	$⊢ i = j \to (B (i) = (1 - T) A (i) + T C (i) \leftrightarrow B (j) = (1 - T) A (j) + T C (j))$
20	19	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)$
21	20	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)$
22	21	3ad2antl3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \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)$
23		oveq2	$⊢ B (j) = (1 - T) A (j) + T C (j) \to A (j) - B (j) = A (j) - ((1 - T) A (j) + T C (j))$
24	23	oveq1d	$⊢ B (j) = (1 - T) A (j) + T C (j) \to {(A (j) - B (j))}^{2} = {(A (j) - ((1 - T) A (j) + T C (j)))}^{2}$
25		subdi	$⊢ (T \in ℂ \land A (j) \in ℂ \land C (j) \in ℂ) \to T (A (j) - C (j)) = T A (j) - T C (j)$
26	25	3coml	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to T (A (j) - C (j)) = T A (j) - T C (j)$
27		ax-1cn	$⊢ 1 \in ℂ$
28		subcl	$⊢ (1 \in ℂ \land T \in ℂ) \to 1 - T \in ℂ$
29	27 28	mpan	$⊢ T \in ℂ \to 1 - T \in ℂ$
30	29	adantl	$⊢ (A (j) \in ℂ \land T \in ℂ) \to 1 - T \in ℂ$
31		simpl	$⊢ (A (j) \in ℂ \land T \in ℂ) \to A (j) \in ℂ$
32		subdir	$⊢ (1 \in ℂ \land 1 - T \in ℂ \land A (j) \in ℂ) \to (1 - (1 - T)) A (j) = 1 A (j) - (1 - T) A (j)$
33	27 30 31 32	mp3an2i	$⊢ (A (j) \in ℂ \land T \in ℂ) \to (1 - (1 - T)) A (j) = 1 A (j) - (1 - T) A (j)$
34		nncan	$⊢ (1 \in ℂ \land T \in ℂ) \to 1 - (1 - T) = T$
35	27 34	mpan	$⊢ T \in ℂ \to 1 - (1 - T) = T$
36	35	oveq1d	$⊢ T \in ℂ \to (1 - (1 - T)) A (j) = T A (j)$
37	36	adantl	$⊢ (A (j) \in ℂ \land T \in ℂ) \to (1 - (1 - T)) A (j) = T A (j)$
38		mulid2	$⊢ A (j) \in ℂ \to 1 A (j) = A (j)$
39	38	oveq1d	$⊢ A (j) \in ℂ \to 1 A (j) - (1 - T) A (j) = A (j) - (1 - T) A (j)$
40	39	adantr	$⊢ (A (j) \in ℂ \land T \in ℂ) \to 1 A (j) - (1 - T) A (j) = A (j) - (1 - T) A (j)$
41	33 37 40	3eqtr3rd	$⊢ (A (j) \in ℂ \land T \in ℂ) \to A (j) - (1 - T) A (j) = T A (j)$
42	41	oveq1d	$⊢ (A (j) \in ℂ \land T \in ℂ) \to A (j) - (1 - T) A (j) - T C (j) = T A (j) - T C (j)$
43	42	3adant2	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to A (j) - (1 - T) A (j) - T C (j) = T A (j) - T C (j)$
44		simp1	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to A (j) \in ℂ$
45		mulcl	$⊢ (1 - T \in ℂ \land A (j) \in ℂ) \to (1 - T) A (j) \in ℂ$
46	29 45	sylan	$⊢ (T \in ℂ \land A (j) \in ℂ) \to (1 - T) A (j) \in ℂ$
47	46	ancoms	$⊢ (A (j) \in ℂ \land T \in ℂ) \to (1 - T) A (j) \in ℂ$
48	47	3adant2	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to (1 - T) A (j) \in ℂ$
49		mulcl	$⊢ (T \in ℂ \land C (j) \in ℂ) \to T C (j) \in ℂ$
50	49	ancoms	$⊢ (C (j) \in ℂ \land T \in ℂ) \to T C (j) \in ℂ$
51	50	3adant1	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to T C (j) \in ℂ$
52	44 48 51	subsub4d	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to A (j) - (1 - T) A (j) - T C (j) = A (j) - ((1 - T) A (j) + T C (j))$
53	26 43 52	3eqtr2rd	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to A (j) - ((1 - T) A (j) + T C (j)) = T (A (j) - C (j))$
54	53	oveq1d	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to {(A (j) - ((1 - T) A (j) + T C (j)))}^{2} = {T (A (j) - C (j))}^{2}$
55		simp3	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to T \in ℂ$
56		subcl	$⊢ (A (j) \in ℂ \land C (j) \in ℂ) \to A (j) - C (j) \in ℂ$
57	56	3adant3	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to A (j) - C (j) \in ℂ$
58	55 57	sqmuld	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to {T (A (j) - C (j))}^{2} = T^{2} {(A (j) - C (j))}^{2}$
59	54 58	eqtrd	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to {(A (j) - ((1 - T) A (j) + T C (j)))}^{2} = T^{2} {(A (j) - C (j))}^{2}$
60	24 59	sylan9eqr	$⊢ ((A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \land B (j) = (1 - T) A (j) + T C (j)) \to {(A (j) - B (j))}^{2} = T^{2} {(A (j) - C (j))}^{2}$
61	3 6 12 22 60	syl31anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \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) - B (j))}^{2} = T^{2} {(A (j) - C (j))}^{2}$
62	61	sumeq2dv	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \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} {(A (j) - B (j))}^{2} = \sum_{j = 1}^{N} T^{2} {(A (j) - C (j))}^{2}$
63		fzfid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \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$
64	8	resqcld	$⊢ T \in [0, 1] \to T^{2} \in ℝ$
65	64	recnd	$⊢ T \in [0, 1] \to T^{2} \in ℂ$
66	65	adantr	$⊢ (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i)) \to T^{2} \in ℂ$
67	66	3ad2ant3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \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^{2} \in ℂ$
68	2	3adant1	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land j \in (1 \dots N)) \to A (j) \in ℂ$
69	68	3adant2r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land j \in (1 \dots N)) \to A (j) \in ℂ$
70	5	3adant1	$⊢ (N \in ℕ \land C \in 𝔼 (N) \land j \in (1 \dots N)) \to C (j) \in ℂ$
71	70	3adant2l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land j \in (1 \dots N)) \to C (j) \in ℂ$
72	69 71	subcld	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land j \in (1 \dots N)) \to A (j) - C (j) \in ℂ$
73	72	sqcld	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land j \in (1 \dots N)) \to {(A (j) - C (j))}^{2} \in ℂ$
74	73	3expa	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N))) \land j \in (1 \dots N)) \to {(A (j) - C (j))}^{2} \in ℂ$
75	74	3adantl3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \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 ℂ$
76	63 67 75	fsummulc2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \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^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = \sum_{j = 1}^{N} T^{2} {(A (j) - C (j))}^{2}$
77	62 76	eqtr4d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \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} {(A (j) - B (j))}^{2} = T^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$

Metamath Proof Explorer

Theorem ax5seglem1

Proof