Theorem 2itscplem3

Description: Lemma D for 2itscp . (Contributed by AV, 4-Mar-2023)

	Ref	Expression
Hypotheses	2itscp.a	$$⊢\phi \to A\in ℝ$$
	2itscp.b	$$⊢\phi \to B\in ℝ$$
	2itscp.x	$$⊢\phi \to X\in ℝ$$
	2itscp.y	$$⊢\phi \to Y\in ℝ$$
	2itscp.d	$$⊢D=X-A$$
	2itscp.e	$$⊢E=B-Y$$
	2itscp.c	$$⊢C=DB+EA$$
	2itscp.r	$$⊢\phi \to R\in ℝ$$
	2itscplem3.q	$$⊢Q=E^2+D^2$$
	2itscplem3.s	$$⊢S=R^{2}Q-C^2$$
Assertion	2itscplem3	$$⊢\phi \to S=E^2\left(R^2-A^2\right)+D^2\left(R^2-B^2\right)-2DAEB$$

Proof

Step	Hyp	Ref	Expression
1		2itscp.a	$$⊢\phi \to A\in ℝ$$
2		2itscp.b	$$⊢\phi \to B\in ℝ$$
3		2itscp.x	$$⊢\phi \to X\in ℝ$$
4		2itscp.y	$$⊢\phi \to Y\in ℝ$$
5		2itscp.d	$$⊢D=X-A$$
6		2itscp.e	$$⊢E=B-Y$$
7		2itscp.c	$$⊢C=DB+EA$$
8		2itscp.r	$$⊢\phi \to R\in ℝ$$
9		2itscplem3.q	$$⊢Q=E^2+D^2$$
10		2itscplem3.s	$$⊢S=R^{2}Q-C^2$$
11	10	a1i	$$⊢\phi \to S=R^{2}Q-C^2$$
12	9	a1i	$$⊢\phi \to Q=E^2+D^2$$
13	12	oveq2d	$$⊢\phi \to R^{2}Q=R^2\left(E^2+D^2\right)$$
14	8	recnd	$$⊢\phi \to R\in ℂ$$
15	14	sqcld	$$⊢\phi \to R^2\in ℂ$$
16	2	recnd	$$⊢\phi \to B\in ℂ$$
17	4	recnd	$$⊢\phi \to Y\in ℂ$$
18	16 17	subcld	$$⊢\phi \to B-Y\in ℂ$$
19	6 18	eqeltrid	$$⊢\phi \to E\in ℂ$$
20	19	sqcld	$$⊢\phi \to E^2\in ℂ$$
21	3	recnd	$$⊢\phi \to X\in ℂ$$
22	1	recnd	$$⊢\phi \to A\in ℂ$$
23	21 22	subcld	$$⊢\phi \to X-A\in ℂ$$
24	5 23	eqeltrid	$$⊢\phi \to D\in ℂ$$
25	24	sqcld	$$⊢\phi \to D^2\in ℂ$$
26	20 25	addcld	$$⊢\phi \to E^2+D^2\in ℂ$$
27	15 26	mulcomd	$$⊢\phi \to R^2\left(E^2+D^2\right)=\left(E^2+D^2\right)R^2$$
28	20 25 15	adddird	$$⊢\phi \to \left(E^2+D^2\right)R^2=E^2{R}^2+D^2{R}^2$$
29	13 27 28	3eqtrd	$$⊢\phi \to R^{2}Q=E^2{R}^2+D^2{R}^2$$
30	1 2 3 4 5 6 7	2itscplem2	$$⊢\phi \to C^2=D^2{B}^2+2DAEB+E^2{A}^2$$
31	29 30	oveq12d	$$⊢\phi \to R^{2}Q-C^2=E^2{R}^2+D^2{R}^2-\left(D^2{B}^2+2DAEB+E^2{A}^2\right)$$
32	20 15	mulcld	$$⊢\phi \to E^2{R}^2\in ℂ$$
33	25 15	mulcld	$$⊢\phi \to D^2{R}^2\in ℂ$$
34	32 33	addcld	$$⊢\phi \to E^2{R}^2+D^2{R}^2\in ℂ$$
35	16	sqcld	$$⊢\phi \to B^2\in ℂ$$
36	25 35	mulcld	$$⊢\phi \to D^2{B}^2\in ℂ$$
37		2cnd	$$⊢\phi \to 2\in ℂ$$
38	24 22	mulcld	$$⊢\phi \to DA\in ℂ$$
39	19 16	mulcld	$$⊢\phi \to EB\in ℂ$$
40	38 39	mulcld	$$⊢\phi \to DAEB\in ℂ$$
41	37 40	mulcld	$$⊢\phi \to 2DAEB\in ℂ$$
42	34 36 41	subsub4d	$$⊢\phi \to \left(E^2{R}^2+D^2{R}^2\right)-D^2{B}^2-2DAEB=E^2{R}^2+D^2{R}^2-\left(D^2{B}^2+2DAEB\right)$$
43	42	eqcomd	$$⊢\phi \to E^2{R}^2+D^2{R}^2-\left(D^2{B}^2+2DAEB\right)=\left(E^2{R}^2+D^2{R}^2\right)-D^2{B}^2-2DAEB$$
44	43	oveq1d	$$⊢\phi \to \left(E^2{R}^2+D^2{R}^2\right)-\left(D^2{B}^2+2DAEB\right)-E^2{A}^2=\left(E^2{R}^2+D^2{R}^2-D^2{B}^2\right)-2DAEB-E^2{A}^2$$
45	34 36	subcld	$$⊢\phi \to E^2{R}^2+D^2{R}^2-D^2{B}^2\in ℂ$$
46	22	sqcld	$$⊢\phi \to A^2\in ℂ$$
47	20 46	mulcld	$$⊢\phi \to E^2{A}^2\in ℂ$$
48	45 41 47	sub32d	$$⊢\phi \to \left(E^2{R}^2+D^2{R}^2-D^2{B}^2\right)-2DAEB-E^2{A}^2=\left(E^2{R}^2+D^2{R}^2-D^2{B}^2\right)-E^2{A}^2-2DAEB$$
49	44 48	eqtrd	$$⊢\phi \to \left(E^2{R}^2+D^2{R}^2\right)-\left(D^2{B}^2+2DAEB\right)-E^2{A}^2=\left(E^2{R}^2+D^2{R}^2-D^2{B}^2\right)-E^2{A}^2-2DAEB$$
50	36 41	addcld	$$⊢\phi \to D^2{B}^2+2DAEB\in ℂ$$
51	34 50 47	subsub4d	$$⊢\phi \to \left(E^2{R}^2+D^2{R}^2\right)-\left(D^2{B}^2+2DAEB\right)-E^2{A}^2=E^2{R}^2+D^2{R}^2-\left(D^2{B}^2+2DAEB+E^2{A}^2\right)$$
52	32 33 36	addsubassd	$$⊢\phi \to E^2{R}^2+D^2{R}^2-D^2{B}^2=E^2{R}^2+D^2{R}^2-D^2{B}^2$$
53	25 15 35	subdid	$$⊢\phi \to D^2\left(R^2-B^2\right)=D^2{R}^2-D^2{B}^2$$
54	53	eqcomd	$$⊢\phi \to D^2{R}^2-D^2{B}^2=D^2\left(R^2-B^2\right)$$
55	54	oveq2d	$$⊢\phi \to E^2{R}^2+D^2{R}^2-D^2{B}^2=E^2{R}^2+D^2\left(R^2-B^2\right)$$
56	52 55	eqtrd	$$⊢\phi \to E^2{R}^2+D^2{R}^2-D^2{B}^2=E^2{R}^2+D^2\left(R^2-B^2\right)$$
57	56	oveq1d	$$⊢\phi \to \left(E^2{R}^2+D^2{R}^2\right)-D^2{B}^2-E^2{A}^2=E^2{R}^2+D^2\left(R^2-B^2\right)-E^2{A}^2$$
58	15 35	subcld	$$⊢\phi \to R^2-B^2\in ℂ$$
59	25 58	mulcld	$$⊢\phi \to D^2\left(R^2-B^2\right)\in ℂ$$
60	32 59 47	addsubd	$$⊢\phi \to E^2{R}^2+D^2\left(R^2-B^2\right)-E^2{A}^2=E^2{R}^2-E^2{A}^2+D^2\left(R^2-B^2\right)$$
61	20 15 46	subdid	$$⊢\phi \to E^2\left(R^2-A^2\right)=E^2{R}^2-E^2{A}^2$$
62	61	eqcomd	$$⊢\phi \to E^2{R}^2-E^2{A}^2=E^2\left(R^2-A^2\right)$$
63	62	oveq1d	$$⊢\phi \to E^2{R}^2-E^2{A}^2+D^2\left(R^2-B^2\right)=E^2\left(R^2-A^2\right)+D^2\left(R^2-B^2\right)$$
64	57 60 63	3eqtrd	$$⊢\phi \to \left(E^2{R}^2+D^2{R}^2\right)-D^2{B}^2-E^2{A}^2=E^2\left(R^2-A^2\right)+D^2\left(R^2-B^2\right)$$
65	64	oveq1d	$$⊢\phi \to \left(E^2{R}^2+D^2{R}^2-D^2{B}^2\right)-E^2{A}^2-2DAEB=E^2\left(R^2-A^2\right)+D^2\left(R^2-B^2\right)-2DAEB$$
66	49 51 65	3eqtr3d	$$⊢\phi \to E^2{R}^2+D^2{R}^2-\left(D^2{B}^2+2DAEB+E^2{A}^2\right)=E^2\left(R^2-A^2\right)+D^2\left(R^2-B^2\right)-2DAEB$$
67	11 31 66	3eqtrd	$$⊢\phi \to S=E^2\left(R^2-A^2\right)+D^2\left(R^2-B^2\right)-2DAEB$$