Theorem ax5seglem8

Description: Lemma for ax5seg . Use the weak deduction theorem to eliminate the hypotheses from ax5seglem7 . (Contributed by Scott Fenton, 11-Jun-2013)

	Ref	Expression
Assertion	ax5seglem8	$$⊢\left(\left(A\in ℂ\wedge T\in ℂ\right)\wedge \left(C\in ℂ\wedge D\in ℂ\right)\right)\to 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		oveq2	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(1-T\right)A=\left(1-T\right)if\left(A\in ℂ,A,0\right)$$
2	1	oveq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(1-T\right)A+TC=\left(1-T\right)if\left(A\in ℂ,A,0\right)+TC$$
3	2	oveq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(1-T\right)A+TC-D=\left(1-T\right)if\left(A\in ℂ,A,0\right)+TC-D$$
4	3	oveq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to {\left(\left(1-T\right)A+TC-D\right)}^2={\left(\left(1-T\right)if\left(A\in ℂ,A,0\right)+TC-D\right)}^2$$
5		oveq1	$$⊢A=if\left(A\in ℂ,A,0\right)\to A-C=if\left(A\in ℂ,A,0\right)-C$$
6	5	oveq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to {\left(A-C\right)}^2={\left(if\left(A\in ℂ,A,0\right)-C\right)}^2$$
7	6	oveq2d	$$⊢A=if\left(A\in ℂ,A,0\right)\to T{\left(A-C\right)}^2=T{\left(if\left(A\in ℂ,A,0\right)-C\right)}^2$$
8		oveq1	$$⊢A=if\left(A\in ℂ,A,0\right)\to A-D=if\left(A\in ℂ,A,0\right)-D$$
9	8	oveq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to {\left(A-D\right)}^2={\left(if\left(A\in ℂ,A,0\right)-D\right)}^2$$
10	7 9	oveq12d	$$⊢A=if\left(A\in ℂ,A,0\right)\to T{\left(A-C\right)}^2-{\left(A-D\right)}^2=T{\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2$$
11	10	oveq2d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(1-T\right)\left(T{\left(A-C\right)}^2-{\left(A-D\right)}^2\right)=\left(1-T\right)\left(T{\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)$$
12	4 11	oveq12d	$$⊢A=if\left(A\in ℂ,A,0\right)\to {\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)if\left(A\in ℂ,A,0\right)+TC-D\right)}^2+\left(1-T\right)\left(T{\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)$$
13	12	eqeq2d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(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)\leftrightarrow T{\left(C-D\right)}^2={\left(\left(1-T\right)if\left(A\in ℂ,A,0\right)+TC-D\right)}^2+\left(1-T\right)\left(T{\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)\right)$$
14		oveq1	$$⊢T=if\left(T\in ℂ,T,0\right)\to T{\left(C-D\right)}^2=if\left(T\in ℂ,T,0\right){\left(C-D\right)}^2$$
15		oveq2	$$⊢T=if\left(T\in ℂ,T,0\right)\to 1-T=1-if\left(T\in ℂ,T,0\right)$$
16	15	oveq1d	$$⊢T=if\left(T\in ℂ,T,0\right)\to \left(1-T\right)if\left(A\in ℂ,A,0\right)=\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)$$
17		oveq1	$$⊢T=if\left(T\in ℂ,T,0\right)\to TC=if\left(T\in ℂ,T,0\right)C$$
18	16 17	oveq12d	$$⊢T=if\left(T\in ℂ,T,0\right)\to \left(1-T\right)if\left(A\in ℂ,A,0\right)+TC=\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)C$$
19	18	oveq1d	$$⊢T=if\left(T\in ℂ,T,0\right)\to \left(1-T\right)if\left(A\in ℂ,A,0\right)+TC-D=\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)C-D$$
20	19	oveq1d	$$⊢T=if\left(T\in ℂ,T,0\right)\to {\left(\left(1-T\right)if\left(A\in ℂ,A,0\right)+TC-D\right)}^2={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)C-D\right)}^2$$
21		oveq1	$$⊢T=if\left(T\in ℂ,T,0\right)\to T{\left(if\left(A\in ℂ,A,0\right)-C\right)}^2=if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-C\right)}^2$$
22	21	oveq1d	$$⊢T=if\left(T\in ℂ,T,0\right)\to T{\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2=if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2$$
23	15 22	oveq12d	$$⊢T=if\left(T\in ℂ,T,0\right)\to \left(1-T\right)\left(T{\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)=\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)$$
24	20 23	oveq12d	$$⊢T=if\left(T\in ℂ,T,0\right)\to {\left(\left(1-T\right)if\left(A\in ℂ,A,0\right)+TC-D\right)}^2+\left(1-T\right)\left(T{\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)C-D\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)$$
25	14 24	eqeq12d	$$⊢T=if\left(T\in ℂ,T,0\right)\to \left(T{\left(C-D\right)}^2={\left(\left(1-T\right)if\left(A\in ℂ,A,0\right)+TC-D\right)}^2+\left(1-T\right)\left(T{\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)\leftrightarrow if\left(T\in ℂ,T,0\right){\left(C-D\right)}^2={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)C-D\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)\right)$$
26		oveq1	$$⊢C=if\left(C\in ℂ,C,0\right)\to C-D=if\left(C\in ℂ,C,0\right)-D$$
27	26	oveq1d	$$⊢C=if\left(C\in ℂ,C,0\right)\to {\left(C-D\right)}^2={\left(if\left(C\in ℂ,C,0\right)-D\right)}^2$$
28	27	oveq2d	$$⊢C=if\left(C\in ℂ,C,0\right)\to if\left(T\in ℂ,T,0\right){\left(C-D\right)}^2=if\left(T\in ℂ,T,0\right){\left(if\left(C\in ℂ,C,0\right)-D\right)}^2$$
29		oveq2	$$⊢C=if\left(C\in ℂ,C,0\right)\to if\left(T\in ℂ,T,0\right)C=if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)$$
30	29	oveq2d	$$⊢C=if\left(C\in ℂ,C,0\right)\to \left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)C=\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)$$
31	30	oveq1d	$$⊢C=if\left(C\in ℂ,C,0\right)\to \left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)C-D=\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-D$$
32	31	oveq1d	$$⊢C=if\left(C\in ℂ,C,0\right)\to {\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)C-D\right)}^2={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-D\right)}^2$$
33		oveq2	$$⊢C=if\left(C\in ℂ,C,0\right)\to if\left(A\in ℂ,A,0\right)-C=if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)$$
34	33	oveq1d	$$⊢C=if\left(C\in ℂ,C,0\right)\to {\left(if\left(A\in ℂ,A,0\right)-C\right)}^2={\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2$$
35	34	oveq2d	$$⊢C=if\left(C\in ℂ,C,0\right)\to if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-C\right)}^2=if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2$$
36	35	oveq1d	$$⊢C=if\left(C\in ℂ,C,0\right)\to if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2=if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2$$
37	36	oveq2d	$$⊢C=if\left(C\in ℂ,C,0\right)\to \left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)=\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)$$
38	32 37	oveq12d	$$⊢C=if\left(C\in ℂ,C,0\right)\to {\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)C-D\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-D\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)$$
39	28 38	eqeq12d	$$⊢C=if\left(C\in ℂ,C,0\right)\to \left(if\left(T\in ℂ,T,0\right){\left(C-D\right)}^2={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)C-D\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-C\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)\leftrightarrow if\left(T\in ℂ,T,0\right){\left(if\left(C\in ℂ,C,0\right)-D\right)}^2={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-D\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)\right)$$
40		oveq2	$$⊢D=if\left(D\in ℂ,D,0\right)\to if\left(C\in ℂ,C,0\right)-D=if\left(C\in ℂ,C,0\right)-if\left(D\in ℂ,D,0\right)$$
41	40	oveq1d	$$⊢D=if\left(D\in ℂ,D,0\right)\to {\left(if\left(C\in ℂ,C,0\right)-D\right)}^2={\left(if\left(C\in ℂ,C,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2$$
42	41	oveq2d	$$⊢D=if\left(D\in ℂ,D,0\right)\to if\left(T\in ℂ,T,0\right){\left(if\left(C\in ℂ,C,0\right)-D\right)}^2=if\left(T\in ℂ,T,0\right){\left(if\left(C\in ℂ,C,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2$$
43		oveq2	$$⊢D=if\left(D\in ℂ,D,0\right)\to \left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-D=\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-if\left(D\in ℂ,D,0\right)$$
44	43	oveq1d	$$⊢D=if\left(D\in ℂ,D,0\right)\to {\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-D\right)}^2={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2$$
45		oveq2	$$⊢D=if\left(D\in ℂ,D,0\right)\to if\left(A\in ℂ,A,0\right)-D=if\left(A\in ℂ,A,0\right)-if\left(D\in ℂ,D,0\right)$$
46	45	oveq1d	$$⊢D=if\left(D\in ℂ,D,0\right)\to {\left(if\left(A\in ℂ,A,0\right)-D\right)}^2={\left(if\left(A\in ℂ,A,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2$$
47	46	oveq2d	$$⊢D=if\left(D\in ℂ,D,0\right)\to if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2=if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2$$
48	47	oveq2d	$$⊢D=if\left(D\in ℂ,D,0\right)\to \left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)=\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2\right)$$
49	44 48	oveq12d	$$⊢D=if\left(D\in ℂ,D,0\right)\to {\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-D\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2\right)$$
50	42 49	eqeq12d	$$⊢D=if\left(D\in ℂ,D,0\right)\to \left(if\left(T\in ℂ,T,0\right){\left(if\left(C\in ℂ,C,0\right)-D\right)}^2={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-D\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-D\right)}^2\right)\leftrightarrow if\left(T\in ℂ,T,0\right){\left(if\left(C\in ℂ,C,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2\right)\right)$$
51		0cn	$$⊢0\in ℂ$$
52	51	elimel	$$⊢if\left(A\in ℂ,A,0\right)\in ℂ$$
53	51	elimel	$$⊢if\left(T\in ℂ,T,0\right)\in ℂ$$
54	51	elimel	$$⊢if\left(C\in ℂ,C,0\right)\in ℂ$$
55	51	elimel	$$⊢if\left(D\in ℂ,D,0\right)\in ℂ$$
56	52 53 54 55	ax5seglem7	$$⊢if\left(T\in ℂ,T,0\right){\left(if\left(C\in ℂ,C,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2={\left(\left(1-if\left(T\in ℂ,T,0\right)\right)if\left(A\in ℂ,A,0\right)+if\left(T\in ℂ,T,0\right)if\left(C\in ℂ,C,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2+\left(1-if\left(T\in ℂ,T,0\right)\right)\left(if\left(T\in ℂ,T,0\right){\left(if\left(A\in ℂ,A,0\right)-if\left(C\in ℂ,C,0\right)\right)}^2-{\left(if\left(A\in ℂ,A,0\right)-if\left(D\in ℂ,D,0\right)\right)}^2\right)$$
57	13 25 39 50 56	dedth4h	$$⊢\left(\left(A\in ℂ\wedge T\in ℂ\right)\wedge \left(C\in ℂ\wedge D\in ℂ\right)\right)\to 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)$$