Theorem ax5seglem7

Description: Lemma for ax5seg . An algebraic calculation needed further down the line. (Contributed by Scott Fenton, 12-Jun-2013)

	Ref	Expression
Hypotheses	ax5seglem7.1	$$⊢A\in ℂ$$
	ax5seglem7.2	$$⊢T\in ℂ$$
	ax5seglem7.3	$$⊢C\in ℂ$$
	ax5seglem7.4	$$⊢D\in ℂ$$
Assertion	ax5seglem7	$$⊢T{\left(C-D\right)}^2={\left(\left(1-T\right)A+TC-D\right)}^2+\left(1-T\right)\left(T{\left(A-C\right)}^2-{\left(A-D\right)}^2\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax5seglem7.1	$$⊢A\in ℂ$$
2		ax5seglem7.2	$$⊢T\in ℂ$$
3		ax5seglem7.3	$$⊢C\in ℂ$$
4		ax5seglem7.4	$$⊢D\in ℂ$$
5	3 4	binom2subi	$$⊢{\left(C-D\right)}^2=C^2-2CD+D^2$$
6	5	oveq2i	$$⊢T{\left(C-D\right)}^2=T\left(C^2-2CD+D^2\right)$$
7	3	sqcli	$$⊢C^2\in ℂ$$
8		2cn	$$⊢2\in ℂ$$
9	3 4	mulcli	$$⊢CD\in ℂ$$
10	8 9	mulcli	$$⊢2CD\in ℂ$$
11	7 10	subcli	$$⊢C^2-2CD\in ℂ$$
12	4	sqcli	$$⊢D^2\in ℂ$$
13	2 11 12	adddii	$$⊢T\left(C^2-2CD+D^2\right)=T\left(C^2-2CD\right)+T{D}^2$$
14	2 7 10	subdii	$$⊢T\left(C^2-2CD\right)=T{C}^2-T2CD$$
15	14	oveq1i	$$⊢T\left(C^2-2CD\right)+T{D}^2=T{C}^2-T2CD+T{D}^2$$
16	6 13 15	3eqtri	$$⊢T{\left(C-D\right)}^2=T{C}^2-T2CD+T{D}^2$$
17		ax-1cn	$$⊢1\in ℂ$$
18	17 2	subcli	$$⊢1-T\in ℂ$$
19	18 1	mulcli	$$⊢\left(1-T\right)A\in ℂ$$
20	19	sqcli	$$⊢{\left(1-T\right)A}^2\in ℂ$$
21	2 3	mulcli	$$⊢TC\in ℂ$$
22	21 4	subcli	$$⊢TC-D\in ℂ$$
23	19 22	mulcli	$$⊢\left(1-T\right)A\left(TC-D\right)\in ℂ$$
24	8 23	mulcli	$$⊢2\left(1-T\right)A\left(TC-D\right)\in ℂ$$
25	20 24	addcli	$$⊢{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\in ℂ$$
26	21	sqcli	$$⊢{TC}^2\in ℂ$$
27	26 12	addcli	$$⊢{TC}^2+D^2\in ℂ$$
28	25 27	addcli	$$⊢{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2\in ℂ$$
29	21 4	mulcli	$$⊢TCD\in ℂ$$
30	8 29	mulcli	$$⊢2TCD\in ℂ$$
31	2 7	mulcli	$$⊢T{C}^2\in ℂ$$
32	2 12	mulcli	$$⊢T{D}^2\in ℂ$$
33	31 32	addcli	$$⊢T{C}^2+T{D}^2\in ℂ$$
34		subadd23	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2\in ℂ\wedge 2TCD\in ℂ\wedge T{C}^2+T{D}^2\in ℂ\right)\to \left(\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD\right)+T{C}^2+T{D}^2=\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)+\left(T{C}^2+T{D}^2-2TCD\right)$$
35	28 30 33 34	mp3an	$$⊢\left(\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD\right)+T{C}^2+T{D}^2=\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)+\left(T{C}^2+T{D}^2-2TCD\right)$$
36	35	oveq1i	$$⊢\left(\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD\right)+\left(T{C}^2+T{D}^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)=\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2\right)+\left(T{C}^2+T{D}^2-2TCD\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
37	19 22	binom2i	$$⊢{\left(\left(1-T\right)A+TC-D\right)}^2={\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{\left(TC-D\right)}^2$$
38	19 21 4	addsubassi	$$⊢\left(1-T\right)A+TC-D=\left(1-T\right)A+TC-D$$
39	38	oveq1i	$$⊢{\left(\left(1-T\right)A+TC-D\right)}^2={\left(\left(1-T\right)A+TC-D\right)}^2$$
40	25 27 30	addsubassi	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD={\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+\left({TC}^2+D^2-2TCD\right)$$
41	21 4	binom2subi	$$⊢{\left(TC-D\right)}^2={TC}^2-2TCD+D^2$$
42	26 12 30	addsubi	$$⊢{TC}^2+D^2-2TCD={TC}^2-2TCD+D^2$$
43	41 42	eqtr4i	$$⊢{\left(TC-D\right)}^2={TC}^2+D^2-2TCD$$
44	43	oveq2i	$$⊢{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{\left(TC-D\right)}^2={\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+\left({TC}^2+D^2-2TCD\right)$$
45	40 44	eqtr4i	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD={\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{\left(TC-D\right)}^2$$
46	37 39 45	3eqtr4i	$$⊢{\left(\left(1-T\right)A+TC-D\right)}^2=\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD$$
47	1 3	binom2subi	$$⊢{\left(A-C\right)}^2=A^2-2AC+C^2$$
48	47	oveq2i	$$⊢T{\left(A-C\right)}^2=T\left(A^2-2AC+C^2\right)$$
49	1	sqcli	$$⊢A^2\in ℂ$$
50	1 3	mulcli	$$⊢AC\in ℂ$$
51	8 50	mulcli	$$⊢2AC\in ℂ$$
52	49 51	subcli	$$⊢A^2-2AC\in ℂ$$
53	2 52 7	adddii	$$⊢T\left(A^2-2AC+C^2\right)=T\left(A^2-2AC\right)+T{C}^2$$
54	48 53	eqtri	$$⊢T{\left(A-C\right)}^2=T\left(A^2-2AC\right)+T{C}^2$$
55	1 4	binom2subi	$$⊢{\left(A-D\right)}^2=A^2-2AD+D^2$$
56	54 55	oveq12i	$$⊢T{\left(A-C\right)}^2-{\left(A-D\right)}^2=T\left(A^2-2AC\right)+T{C}^2-\left(A^2-2AD+D^2\right)$$
57	2 52	mulcli	$$⊢T\left(A^2-2AC\right)\in ℂ$$
58	1 4	mulcli	$$⊢AD\in ℂ$$
59	8 58	mulcli	$$⊢2AD\in ℂ$$
60	49 59	subcli	$$⊢A^2-2AD\in ℂ$$
61	57 31 60 12	addsub4i	$$⊢T\left(A^2-2AC\right)+T{C}^2-\left(A^2-2AD+D^2\right)=\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)+T{C}^2-D^2$$
62	56 61	eqtri	$$⊢T{\left(A-C\right)}^2-{\left(A-D\right)}^2=\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)+T{C}^2-D^2$$
63	62	oveq2i	$$⊢\left(1-T\right)\left(T{\left(A-C\right)}^2-{\left(A-D\right)}^2\right)=\left(1-T\right)\left(\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)+T{C}^2-D^2\right)$$
64	57 60	subcli	$$⊢T\left(A^2-2AC\right)-\left(A^2-2AD\right)\in ℂ$$
65	31 12	subcli	$$⊢T{C}^2-D^2\in ℂ$$
66	18 64 65	adddii	$$⊢\left(1-T\right)\left(\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)+T{C}^2-D^2\right)=\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)+\left(1-T\right)\left(T{C}^2-D^2\right)$$
67	17 2 65	subdiri	$$⊢\left(1-T\right)\left(T{C}^2-D^2\right)=1\left(T{C}^2-D^2\right)-T\left(T{C}^2-D^2\right)$$
68	65	mulid2i	$$⊢1\left(T{C}^2-D^2\right)=T{C}^2-D^2$$
69	2 31 12	subdii	$$⊢T\left(T{C}^2-D^2\right)=TT{C}^2-T{D}^2$$
70	68 69	oveq12i	$$⊢1\left(T{C}^2-D^2\right)-T\left(T{C}^2-D^2\right)=T{C}^2-D^2-\left(TT{C}^2-T{D}^2\right)$$
71	2 31	mulcli	$$⊢TT{C}^2\in ℂ$$
72		subsub3	$$⊢\left(T{C}^2-D^2\in ℂ\wedge TT{C}^2\in ℂ\wedge T{D}^2\in ℂ\right)\to T{C}^2-D^2-\left(TT{C}^2-T{D}^2\right)=\left(T{C}^2-D^2\right)+T{D}^2-TT{C}^2$$
73	65 71 32 72	mp3an	$$⊢T{C}^2-D^2-\left(TT{C}^2-T{D}^2\right)=\left(T{C}^2-D^2\right)+T{D}^2-TT{C}^2$$
74	31 32 12	addsubi	$$⊢T{C}^2+T{D}^2-D^2=T{C}^2-D^2+T{D}^2$$
75	74	oveq1i	$$⊢\left(T{C}^2+T{D}^2\right)-D^2-TT{C}^2=\left(T{C}^2-D^2\right)+T{D}^2-TT{C}^2$$
76		subsub4	$$⊢\left(T{C}^2+T{D}^2\in ℂ\wedge D^2\in ℂ\wedge TT{C}^2\in ℂ\right)\to \left(T{C}^2+T{D}^2\right)-D^2-TT{C}^2=T{C}^2+T{D}^2-\left(D^2+TT{C}^2\right)$$
77	33 12 71 76	mp3an	$$⊢\left(T{C}^2+T{D}^2\right)-D^2-TT{C}^2=T{C}^2+T{D}^2-\left(D^2+TT{C}^2\right)$$
78	73 75 77	3eqtr2i	$$⊢T{C}^2-D^2-\left(TT{C}^2-T{D}^2\right)=T{C}^2+T{D}^2-\left(D^2+TT{C}^2\right)$$
79	67 70 78	3eqtri	$$⊢\left(1-T\right)\left(T{C}^2-D^2\right)=T{C}^2+T{D}^2-\left(D^2+TT{C}^2\right)$$
80	79	oveq2i	$$⊢\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)+\left(1-T\right)\left(T{C}^2-D^2\right)=\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)+\left(T{C}^2+T{D}^2\right)-\left(D^2+TT{C}^2\right)$$
81	18 64	mulcli	$$⊢\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\in ℂ$$
82	12 71	addcli	$$⊢D^2+TT{C}^2\in ℂ$$
83		addsub12	$$⊢\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\in ℂ\wedge T{C}^2+T{D}^2\in ℂ\wedge D^2+TT{C}^2\in ℂ\right)\to \left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)+\left(T{C}^2+T{D}^2\right)-\left(D^2+TT{C}^2\right)=T{C}^2+T{D}^2+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
84	81 33 82 83	mp3an	$$⊢\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)+\left(T{C}^2+T{D}^2\right)-\left(D^2+TT{C}^2\right)=T{C}^2+T{D}^2+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
85	80 84	eqtri	$$⊢\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)+\left(1-T\right)\left(T{C}^2-D^2\right)=T{C}^2+T{D}^2+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
86	63 66 85	3eqtri	$$⊢\left(1-T\right)\left(T{\left(A-C\right)}^2-{\left(A-D\right)}^2\right)=T{C}^2+T{D}^2+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
87	46 86	oveq12i	$$⊢{\left(\left(1-T\right)A+TC-D\right)}^2+\left(1-T\right)\left(T{\left(A-C\right)}^2-{\left(A-D\right)}^2\right)=\left(\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD\right)+\left(T{C}^2+T{D}^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
88	28 30	subcli	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD\in ℂ$$
89	81 82	subcli	$$⊢\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\in ℂ$$
90	88 33 89	addassi	$$⊢\left(\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD\right)+\left(T{C}^2+T{D}^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)=\left(\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD\right)+\left(T{C}^2+T{D}^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
91	87 90	eqtr4i	$$⊢{\left(\left(1-T\right)A+TC-D\right)}^2+\left(1-T\right)\left(T{\left(A-C\right)}^2-{\left(A-D\right)}^2\right)=\left(\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-2TCD\right)+\left(T{C}^2+T{D}^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
92	33 30	subcli	$$⊢T{C}^2+T{D}^2-2TCD\in ℂ$$
93	28 89 92	add32i	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)+\left(T{C}^2+T{D}^2-2TCD\right)=\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2\right)+\left(T{C}^2+T{D}^2-2TCD\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
94	36 91 93	3eqtr4i	$$⊢{\left(\left(1-T\right)A+TC-D\right)}^2+\left(1-T\right)\left(T{\left(A-C\right)}^2-{\left(A-D\right)}^2\right)=\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)+\left(T{C}^2+T{D}^2-2TCD\right)$$
95		subsub2	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2\in ℂ\wedge D^2+TT{C}^2\in ℂ\wedge \left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\in ℂ\right)\to \left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-\left(D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\right)=\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
96	28 82 81 95	mp3an	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-\left(D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\right)=\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)$$
97	25 26 12	addassi	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+{TC}^2+D^2={\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2$$
98	25 26	addcomi	$$⊢{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2={TC}^2+{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)$$
99	2 3	sqmuli	$$⊢{TC}^2=T^2{C}^2$$
100	2	sqvali	$$⊢T^2=TT$$
101	100	oveq1i	$$⊢T^2{C}^2=TT{C}^2$$
102	2 2 7	mulassi	$$⊢TT{C}^2=TT{C}^2$$
103	99 101 102	3eqtri	$$⊢{TC}^2=TT{C}^2$$
104	18 1	sqmuli	$$⊢{\left(1-T\right)A}^2={\left(1-T\right)}^2{A}^2$$
105	18	sqvali	$$⊢{\left(1-T\right)}^2=\left(1-T\right)\left(1-T\right)$$
106	105	oveq1i	$$⊢{\left(1-T\right)}^2{A}^2=\left(1-T\right)\left(1-T\right)A^2$$
107	18 18 49	mulassi	$$⊢\left(1-T\right)\left(1-T\right)A^2=\left(1-T\right)\left(1-T\right)A^2$$
108	17 2 49	subdiri	$$⊢\left(1-T\right)A^2=1A^2-T{A}^2$$
109	49	mulid2i	$$⊢1A^2=A^2$$
110	109	oveq1i	$$⊢1A^2-T{A}^2=A^2-T{A}^2$$
111	108 110	eqtri	$$⊢\left(1-T\right)A^2=A^2-T{A}^2$$
112	111	oveq2i	$$⊢\left(1-T\right)\left(1-T\right)A^2=\left(1-T\right)\left(A^2-T{A}^2\right)$$
113	107 112	eqtri	$$⊢\left(1-T\right)\left(1-T\right)A^2=\left(1-T\right)\left(A^2-T{A}^2\right)$$
114	104 106 113	3eqtri	$$⊢{\left(1-T\right)A}^2=\left(1-T\right)\left(A^2-T{A}^2\right)$$
115	8 19 22	mul12i	$$⊢2\left(1-T\right)A\left(TC-D\right)=\left(1-T\right)A2\left(TC-D\right)$$
116	8 22	mulcli	$$⊢2\left(TC-D\right)\in ℂ$$
117	18 1 116	mulassi	$$⊢\left(1-T\right)A2\left(TC-D\right)=\left(1-T\right)A2\left(TC-D\right)$$
118	1 8	mulcomi	$$⊢A\cdot 2=2A$$
119	118	oveq1i	$$⊢A\cdot 2\left(TC-D\right)=2A\left(TC-D\right)$$
120	1 8 22	mulassi	$$⊢A\cdot 2\left(TC-D\right)=A2\left(TC-D\right)$$
121	119 120	eqtr3i	$$⊢2A\left(TC-D\right)=A2\left(TC-D\right)$$
122	8 1	mulcli	$$⊢2A\in ℂ$$
123	122 21 4	subdii	$$⊢2A\left(TC-D\right)=2ATC-2AD$$
124	122 2 3	mul12i	$$⊢2ATC=T2AC$$
125	8 1 3	mulassi	$$⊢2AC=2AC$$
126	125	oveq2i	$$⊢T2AC=T2AC$$
127	124 126	eqtri	$$⊢2ATC=T2AC$$
128	8 1 4	mulassi	$$⊢2AD=2AD$$
129	127 128	oveq12i	$$⊢2ATC-2AD=T2AC-2AD$$
130	123 129	eqtri	$$⊢2A\left(TC-D\right)=T2AC-2AD$$
131	121 130	eqtr3i	$$⊢A2\left(TC-D\right)=T2AC-2AD$$
132	131	oveq2i	$$⊢\left(1-T\right)A2\left(TC-D\right)=\left(1-T\right)\left(T2AC-2AD\right)$$
133	115 117 132	3eqtri	$$⊢2\left(1-T\right)A\left(TC-D\right)=\left(1-T\right)\left(T2AC-2AD\right)$$
134	114 133	oveq12i	$$⊢{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)=\left(1-T\right)\left(A^2-T{A}^2\right)+\left(1-T\right)\left(T2AC-2AD\right)$$
135	2 49	mulcli	$$⊢T{A}^2\in ℂ$$
136	49 135	subcli	$$⊢A^2-T{A}^2\in ℂ$$
137	2 51	mulcli	$$⊢T2AC\in ℂ$$
138	137 59	subcli	$$⊢T2AC-2AD\in ℂ$$
139	18 136 138	adddii	$$⊢\left(1-T\right)\left(\left(A^2-T{A}^2\right)+T2AC-2AD\right)=\left(1-T\right)\left(A^2-T{A}^2\right)+\left(1-T\right)\left(T2AC-2AD\right)$$
140	2 49 51	subdii	$$⊢T\left(A^2-2AC\right)=T{A}^2-T2AC$$
141	140	oveq2i	$$⊢A^2-2AD-T\left(A^2-2AC\right)=A^2-2AD-\left(T{A}^2-T2AC\right)$$
142	140 57	eqeltrri	$$⊢T{A}^2-T2AC\in ℂ$$
143		sub32	$$⊢\left(A^2\in ℂ\wedge T{A}^2-T2AC\in ℂ\wedge 2AD\in ℂ\right)\to A^2-\left(T{A}^2-T2AC\right)-2AD=A^2-2AD-\left(T{A}^2-T2AC\right)$$
144	49 142 59 143	mp3an	$$⊢A^2-\left(T{A}^2-T2AC\right)-2AD=A^2-2AD-\left(T{A}^2-T2AC\right)$$
145	141 144	eqtr4i	$$⊢A^2-2AD-T\left(A^2-2AC\right)=A^2-\left(T{A}^2-T2AC\right)-2AD$$
146		subsub	$$⊢\left(A^2\in ℂ\wedge T{A}^2\in ℂ\wedge T2AC\in ℂ\right)\to A^2-\left(T{A}^2-T2AC\right)=A^2-T{A}^2+T2AC$$
147	49 135 137 146	mp3an	$$⊢A^2-\left(T{A}^2-T2AC\right)=A^2-T{A}^2+T2AC$$
148	147	oveq1i	$$⊢A^2-\left(T{A}^2-T2AC\right)-2AD=\left(A^2-T{A}^2\right)+T2AC-2AD$$
149	136 137 59	addsubassi	$$⊢\left(A^2-T{A}^2\right)+T2AC-2AD=\left(A^2-T{A}^2\right)+T2AC-2AD$$
150	145 148 149	3eqtrri	$$⊢\left(A^2-T{A}^2\right)+T2AC-2AD=A^2-2AD-T\left(A^2-2AC\right)$$
151	150	oveq2i	$$⊢\left(1-T\right)\left(\left(A^2-T{A}^2\right)+T2AC-2AD\right)=\left(1-T\right)\left(A^2-2AD-T\left(A^2-2AC\right)\right)$$
152	134 139 151	3eqtr2i	$$⊢{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)=\left(1-T\right)\left(A^2-2AD-T\left(A^2-2AC\right)\right)$$
153	57 60	negsubdi2i	$$⊢-\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)=A^2-2AD-T\left(A^2-2AC\right)$$
154	153	oveq2i	$$⊢\left(1-T\right)\left(-\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\right)=\left(1-T\right)\left(A^2-2AD-T\left(A^2-2AC\right)\right)$$
155	18 64	mulneg2i	$$⊢\left(1-T\right)\left(-\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\right)=-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)$$
156	152 154 155	3eqtr2i	$$⊢{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)=-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)$$
157	103 156	oveq12i	$$⊢{TC}^2+{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)=TT{C}^2+\left(-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\right)$$
158	71 81	negsubi	$$⊢TT{C}^2+\left(-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\right)=TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)$$
159	98 157 158	3eqtri	$$⊢{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2=TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)$$
160	159	oveq2i	$$⊢D^2+\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+{TC}^2=D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)$$
161	25 26	addcli	$$⊢{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2\in ℂ$$
162	161 12	addcomi	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+{TC}^2+D^2=D^2+\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+{TC}^2$$
163	12 71 81	addsubassi	$$⊢D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)=D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)$$
164	160 162 163	3eqtr4i	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+{TC}^2+D^2=D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)$$
165	97 164	eqtr3i	$$⊢{\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2=D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)$$
166	82 81	subcli	$$⊢D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\in ℂ$$
167	28 166	subeq0i	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-\left(D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\right)=0\leftrightarrow {\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2=D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)$$
168	165 167	mpbir	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)-\left(D^2+TT{C}^2-\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)\right)=0$$
169	96 168	eqtr3i	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)\right)+\left({TC}^2+D^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)=0$$
170	2 3 4	mulassi	$$⊢TCD=TCD$$
171	170	oveq2i	$$⊢2TCD=2TCD$$
172	8 2 9	mul12i	$$⊢2TCD=T2CD$$
173	171 172	eqtri	$$⊢2TCD=T2CD$$
174	173	oveq2i	$$⊢T{C}^2+T{D}^2-2TCD=T{C}^2+T{D}^2-T2CD$$
175	2 10	mulcli	$$⊢T2CD\in ℂ$$
176	31 32 175	addsubi	$$⊢T{C}^2+T{D}^2-T2CD=T{C}^2-T2CD+T{D}^2$$
177	174 176	eqtri	$$⊢T{C}^2+T{D}^2-2TCD=T{C}^2-T2CD+T{D}^2$$
178	169 177	oveq12i	$$⊢\left({\left(1-T\right)A}^2+2\left(1-T\right)A\left(TC-D\right)+{TC}^2+D^2\right)+\left(\left(1-T\right)\left(T\left(A^2-2AC\right)-\left(A^2-2AD\right)\right)-\left(D^2+TT{C}^2\right)\right)+\left(T{C}^2+T{D}^2-2TCD\right)=0+\left(T{C}^2-T2CD\right)+T{D}^2$$
179	31 175	subcli	$$⊢T{C}^2-T2CD\in ℂ$$
180	179 32	addcli	$$⊢T{C}^2-T2CD+T{D}^2\in ℂ$$
181	180	addid2i	$$⊢0+\left(T{C}^2-T2CD\right)+T{D}^2=T{C}^2-T2CD+T{D}^2$$
182	94 178 181	3eqtri	$$⊢{\left(\left(1-T\right)A+TC-D\right)}^2+\left(1-T\right)\left(T{\left(A-C\right)}^2-{\left(A-D\right)}^2\right)=T{C}^2-T2CD+T{D}^2$$
183	16 182	eqtr4i	$$⊢T{\left(C-D\right)}^2={\left(\left(1-T\right)A+TC-D\right)}^2+\left(1-T\right)\left(T{\left(A-C\right)}^2-{\left(A-D\right)}^2\right)$$