Theorem pjthlem1

Description: Lemma for pjth . (Contributed by NM, 10-Oct-1999) (Revised by Mario Carneiro, 17-Oct-2015) (Proof shortened by AV, 10-Jul-2022)

	Ref	Expression
Hypotheses	pjthlem.v	$$⊢V={\mathrm{Base}}_W$$
	pjthlem.n	$$⊢N=\mathrm{norm}\left(W\right)$$
	pjthlem.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	pjthlem.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	pjthlem.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	pjthlem.l	$$⊢L=\mathrm{LSubSp}\left(W\right)$$
	pjthlem.1	$$⊢\phi \to W\in \mathrm{ℂHil}$$
	pjthlem.2	$$⊢\phi \to U\in L$$
	pjthlem.4	$$⊢\phi \to A\in V$$
	pjthlem.5	$$⊢\phi \to B\in U$$
	pjthlem.7	$$⊢\phi \to \forall x\in UN\left(A\right)\le N\left(A\underset{\dot{}}{-}x\right)$$
	pjthlem.8	$$⊢T=\frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}$$
Assertion	pjthlem1	$$⊢\phi \to A\underset{\dot{}}{,}B=0$$

Proof

Step	Hyp	Ref	Expression
1		pjthlem.v	$$⊢V={\mathrm{Base}}_W$$
2		pjthlem.n	$$⊢N=\mathrm{norm}\left(W\right)$$
3		pjthlem.p	$$⊢\underset{\dot{}}{+}={+}_W$$
4		pjthlem.m	$$⊢\underset{\dot{}}{-}={-}_W$$
5		pjthlem.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
6		pjthlem.l	$$⊢L=\mathrm{LSubSp}\left(W\right)$$
7		pjthlem.1	$$⊢\phi \to W\in \mathrm{ℂHil}$$
8		pjthlem.2	$$⊢\phi \to U\in L$$
9		pjthlem.4	$$⊢\phi \to A\in V$$
10		pjthlem.5	$$⊢\phi \to B\in U$$
11		pjthlem.7	$$⊢\phi \to \forall x\in UN\left(A\right)\le N\left(A\underset{\dot{}}{-}x\right)$$
12		pjthlem.8	$$⊢T=\frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}$$
13		hlcph	$$⊢W\in \mathrm{ℂHil}\to W\in \mathrm{CPreHil}$$
14	7 13	syl	$$⊢\phi \to W\in \mathrm{CPreHil}$$
15	1 6	lssss	$$⊢U\in L\to U\subseteq V$$
16	8 15	syl	$$⊢\phi \to U\subseteq V$$
17	16 10	sseldd	$$⊢\phi \to B\in V$$
18	1 5	cphipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{,}B\in ℂ$$
19	14 9 17 18	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}B\in ℂ$$
20	19	abscld	$$⊢\phi \to \left|A\underset{\dot{}}{,}B\right|\in ℝ$$
21	20	recnd	$$⊢\phi \to \left|A\underset{\dot{}}{,}B\right|\in ℂ$$
22	20	resqcld	$$⊢\phi \to {\left|A\underset{\dot{}}{,}B\right|}^2\in ℝ$$
23	22	renegcld	$$⊢\phi \to -{\left|A\underset{\dot{}}{,}B\right|}^2\in ℝ$$
24	1 5	reipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge B\in V\right)\to B\underset{\dot{}}{,}B\in ℝ$$
25	14 17 24	syl2anc	$$⊢\phi \to B\underset{\dot{}}{,}B\in ℝ$$
26		2re	$$⊢2\in ℝ$$
27		readdcl	$$⊢\left(B\underset{\dot{}}{,}B\in ℝ\wedge 2\in ℝ\right)\to \left(B\underset{\dot{}}{,}B\right)+2\in ℝ$$
28	25 26 27	sylancl	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+2\in ℝ$$
29		0red	$$⊢\phi \to 0\in ℝ$$
30		peano2re	$$⊢B\underset{\dot{}}{,}B\in ℝ\to \left(B\underset{\dot{}}{,}B\right)+1\in ℝ$$
31	25 30	syl	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+1\in ℝ$$
32	1 5	ipge0	$$⊢\left(W\in \mathrm{CPreHil}\wedge B\in V\right)\to 0\le B\underset{\dot{}}{,}B$$
33	14 17 32	syl2anc	$$⊢\phi \to 0\le B\underset{\dot{}}{,}B$$
34	25	ltp1d	$$⊢\phi \to B\underset{\dot{}}{,}B<\left(B\underset{\dot{}}{,}B\right)+1$$
35	29 25 31 33 34	lelttrd	$$⊢\phi \to 0<\left(B\underset{\dot{}}{,}B\right)+1$$
36	31	ltp1d	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+1<\left(B\underset{\dot{}}{,}B\right)+1+1$$
37	25	recnd	$$⊢\phi \to B\underset{\dot{}}{,}B\in ℂ$$
38		ax-1cn	$$⊢1\in ℂ$$
39		addass	$$⊢\left(B\underset{\dot{}}{,}B\in ℂ\wedge 1\in ℂ\wedge 1\in ℂ\right)\to \left(B\underset{\dot{}}{,}B\right)+1+1=\left(B\underset{\dot{}}{,}B\right)+1+1$$
40	38 38 39	mp3an23	$$⊢B\underset{\dot{}}{,}B\in ℂ\to \left(B\underset{\dot{}}{,}B\right)+1+1=\left(B\underset{\dot{}}{,}B\right)+1+1$$
41	37 40	syl	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+1+1=\left(B\underset{\dot{}}{,}B\right)+1+1$$
42		df-2	$$⊢2=1+1$$
43	42	oveq2i	$$⊢\left(B\underset{\dot{}}{,}B\right)+2=\left(B\underset{\dot{}}{,}B\right)+1+1$$
44	41 43	syl6reqr	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+2=\left(B\underset{\dot{}}{,}B\right)+1+1$$
45	36 44	breqtrrd	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+1<\left(B\underset{\dot{}}{,}B\right)+2$$
46	29 31 28 35 45	lttrd	$$⊢\phi \to 0<\left(B\underset{\dot{}}{,}B\right)+2$$
47	28 46	elrpd	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+2\in {ℝ}^{+}$$
48		oveq2	$$⊢x=T{\cdot }_{W}B\to A\underset{\dot{}}{-}x=A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)$$
49	48	fveq2d	$$⊢x=T{\cdot }_{W}B\to N\left(A\underset{\dot{}}{-}x\right)=N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)$$
50	49	breq2d	$$⊢x=T{\cdot }_{W}B\to \left(N\left(A\right)\le N\left(A\underset{\dot{}}{-}x\right)\leftrightarrow N\left(A\right)\le N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)$$
51		cphlmod	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{LMod}$$
52	14 51	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
53		hlphl	$$⊢W\in \mathrm{ℂHil}\to W\in \mathrm{PreHil}$$
54	7 53	syl	$$⊢\phi \to W\in \mathrm{PreHil}$$
55		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
56		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
57	55 5 1 56	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{,}B\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
58	54 9 17 57	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}B\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
59	55 56	hlress	$$⊢W\in \mathrm{ℂHil}\to ℝ\subseteq {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
60	7 59	syl	$$⊢\phi \to ℝ\subseteq {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
61	60 31	sseldd	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
62	25 33	ge0p1rpd	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+1\in {ℝ}^{+}$$
63	62	rpne0d	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+1\ne 0$$
64	55 56	cphdivcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge \left(A\underset{\dot{}}{,}B\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge \left(B\underset{\dot{}}{,}B\right)+1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge \left(B\underset{\dot{}}{,}B\right)+1\ne 0\right)\right)\to \frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
65	14 58 61 63 64	syl13anc	$$⊢\phi \to \frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
66	12 65	eqeltrid	$$⊢\phi \to T\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
67		eqid	$$⊢{\cdot }_W={\cdot }_W$$
68	55 67 56 6	lssvscl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge U\in L\right)\wedge \left(T\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge B\in U\right)\right)\to T{\cdot }_{W}B\in U$$
69	52 8 66 10 68	syl22anc	$$⊢\phi \to T{\cdot }_{W}B\in U$$
70	50 11 69	rspcdva	$$⊢\phi \to N\left(A\right)\le N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)$$
71		cphngp	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{NrmGrp}$$
72	14 71	syl	$$⊢\phi \to W\in \mathrm{NrmGrp}$$
73	1 2	nmcl	$$⊢\left(W\in \mathrm{NrmGrp}\wedge A\in V\right)\to N\left(A\right)\in ℝ$$
74	72 9 73	syl2anc	$$⊢\phi \to N\left(A\right)\in ℝ$$
75	1 55 67 56	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge T\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge B\in V\right)\to T{\cdot }_{W}B\in V$$
76	52 66 17 75	syl3anc	$$⊢\phi \to T{\cdot }_{W}B\in V$$
77	1 4	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in V\wedge T{\cdot }_{W}B\in V\right)\to A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\in V$$
78	52 9 76 77	syl3anc	$$⊢\phi \to A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\in V$$
79	1 2	nmcl	$$⊢\left(W\in \mathrm{NrmGrp}\wedge A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\in V\right)\to N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\in ℝ$$
80	72 78 79	syl2anc	$$⊢\phi \to N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\in ℝ$$
81	1 2	nmge0	$$⊢\left(W\in \mathrm{NrmGrp}\wedge A\in V\right)\to 0\le N\left(A\right)$$
82	72 9 81	syl2anc	$$⊢\phi \to 0\le N\left(A\right)$$
83	1 2	nmge0	$$⊢\left(W\in \mathrm{NrmGrp}\wedge A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\in V\right)\to 0\le N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)$$
84	72 78 83	syl2anc	$$⊢\phi \to 0\le N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)$$
85	74 80 82 84	le2sqd	$$⊢\phi \to \left(N\left(A\right)\le N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\leftrightarrow {N\left(A\right)}^2\le {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2\right)$$
86	70 85	mpbid	$$⊢\phi \to {N\left(A\right)}^2\le {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2$$
87	80	resqcld	$$⊢\phi \to {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2\in ℝ$$
88	74	resqcld	$$⊢\phi \to {N\left(A\right)}^2\in ℝ$$
89	87 88	subge0d	$$⊢\phi \to \left(0\le {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2-{N\left(A\right)}^2\leftrightarrow {N\left(A\right)}^2\le {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2\right)$$
90	86 89	mpbird	$$⊢\phi \to 0\le {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2-{N\left(A\right)}^2$$
91		2z	$$⊢2\in \mathbb{Z}$$
92		rpexpcl	$$⊢\left(\left(B\underset{\dot{}}{,}B\right)+1\in {ℝ}^{+}\wedge 2\in \mathbb{Z}\right)\to {\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2\in {ℝ}^{+}$$
93	62 91 92	sylancl	$$⊢\phi \to {\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2\in {ℝ}^{+}$$
94	22 93	rerpdivcld	$$⊢\phi \to \frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\in ℝ$$
95	94 28	remulcld	$$⊢\phi \to \left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\in ℝ$$
96	95	recnd	$$⊢\phi \to \left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\in ℂ$$
97	96	negcld	$$⊢\phi \to -\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\in ℂ$$
98	1 5	cphipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge A\in V\right)\to A\underset{\dot{}}{,}A\in ℂ$$
99	14 9 9 98	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}A\in ℂ$$
100	97 99	pncand	$$⊢\phi \to \left(-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)+\left(A\underset{\dot{}}{,}A\right)-\left(A\underset{\dot{}}{,}A\right)=-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)$$
101	1 5 2	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\in V\right)\to {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2=\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)$$
102	14 78 101	syl2anc	$$⊢\phi \to {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2=\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)$$
103	5 1 4	cphsubdir	$$⊢\left(W\in \mathrm{CPreHil}\wedge \left(A\in V\wedge T{\cdot }_{W}B\in V\wedge A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\in V\right)\right)\to \left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)=\left(A\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)-\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)$$
104	14 9 76 78 103	syl13anc	$$⊢\phi \to \left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)=\left(A\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)-\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)$$
105	5 1 4	cphsubdi	$$⊢\left(W\in \mathrm{CPreHil}\wedge \left(A\in V\wedge A\in V\wedge T{\cdot }_{W}B\in V\right)\right)\to A\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)=\left(A\underset{\dot{}}{,}A\right)-\left(A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)$$
106	14 9 9 76 105	syl13anc	$$⊢\phi \to A\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)=\left(A\underset{\dot{}}{,}A\right)-\left(A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)$$
107	106	oveq1d	$$⊢\phi \to \left(A\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)-\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)=\left(A\underset{\dot{}}{,}A\right)-\left(A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)-\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)$$
108	1 5	cphipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge T{\cdot }_{W}B\in V\right)\to A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\in ℂ$$
109	14 9 76 108	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\in ℂ$$
110	5 1 4	cphsubdi	$$⊢\left(W\in \mathrm{CPreHil}\wedge \left(T{\cdot }_{W}B\in V\wedge A\in V\wedge T{\cdot }_{W}B\in V\right)\right)\to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)=\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}A\right)-\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)$$
111	14 76 9 76 110	syl13anc	$$⊢\phi \to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)=\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}A\right)-\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)$$
112	1 5	cphipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge T{\cdot }_{W}B\in V\wedge A\in V\right)\to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}A\in ℂ$$
113	14 76 9 112	syl3anc	$$⊢\phi \to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}A\in ℂ$$
114	1 5	cphipcl	$$⊢\left(W\in \mathrm{CPreHil}\wedge T{\cdot }_{W}B\in V\wedge T{\cdot }_{W}B\in V\right)\to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\in ℂ$$
115	14 76 76 114	syl3anc	$$⊢\phi \to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\in ℂ$$
116	113 115	subcld	$$⊢\phi \to \left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}A\right)-\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)\in ℂ$$
117	111 116	eqeltrd	$$⊢\phi \to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\in ℂ$$
118	99 109 117	subsub4d	$$⊢\phi \to \left(A\underset{\dot{}}{,}A\right)-\left(A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)-\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)=\left(A\underset{\dot{}}{,}A\right)-\left(\left(A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)+\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)\right)$$
119	94	recnd	$$⊢\phi \to \frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\in ℂ$$
120	31	recnd	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+1\in ℂ$$
121		1cnd	$$⊢\phi \to 1\in ℂ$$
122	119 120 121	adddid	$$⊢\phi \to \left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1+1\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)+\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\cdot 1$$
123	44	oveq2d	$$⊢\phi \to \left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1+1\right)$$
124	5 1 55 56 67	cphassr	$$⊢\left(W\in \mathrm{CPreHil}\wedge \left(T\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge A\in V\wedge B\in V\right)\right)\to A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)=\bar{T}\left(A\underset{\dot{}}{,}B\right)$$
125	14 66 9 17 124	syl13anc	$$⊢\phi \to A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)=\bar{T}\left(A\underset{\dot{}}{,}B\right)$$
126	19 120 63	divcld	$$⊢\phi \to \frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}\in ℂ$$
127	12 126	eqeltrid	$$⊢\phi \to T\in ℂ$$
128	127	cjcld	$$⊢\phi \to \bar{T}\in ℂ$$
129	128 19	mulcomd	$$⊢\phi \to \bar{T}\left(A\underset{\dot{}}{,}B\right)=\left(A\underset{\dot{}}{,}B\right)\bar{T}$$
130	19	cjcld	$$⊢\phi \to \overline{A\underset{\dot{}}{,}B}\in ℂ$$
131	19 130 120 63	divassd	$$⊢\phi \to \frac{\left(A\underset{\dot{}}{,}B\right)\overline{A\underset{\dot{}}{,}B}}{\left(B\underset{\dot{}}{,}B\right)+1}=\left(A\underset{\dot{}}{,}B\right)\left(\frac{\overline{A\underset{\dot{}}{,}B}}{\left(B\underset{\dot{}}{,}B\right)+1}\right)$$
132	19	absvalsqd	$$⊢\phi \to {\left|A\underset{\dot{}}{,}B\right|}^2=\left(A\underset{\dot{}}{,}B\right)\overline{A\underset{\dot{}}{,}B}$$
133	132	oveq1d	$$⊢\phi \to \frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{\left(B\underset{\dot{}}{,}B\right)+1}=\frac{\left(A\underset{\dot{}}{,}B\right)\overline{A\underset{\dot{}}{,}B}}{\left(B\underset{\dot{}}{,}B\right)+1}$$
134	12	fveq2i	$$⊢\bar{T}=\stackrel{‾}{\frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}}$$
135	19 120 63	cjdivd	$$⊢\phi \to \stackrel{‾}{\frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}}=\frac{\overline{A\underset{\dot{}}{,}B}}{\overline{\left(B\underset{\dot{}}{,}B\right)+1}}$$
136	31	cjred	$$⊢\phi \to \overline{\left(B\underset{\dot{}}{,}B\right)+1}=\left(B\underset{\dot{}}{,}B\right)+1$$
137	136	oveq2d	$$⊢\phi \to \frac{\overline{A\underset{\dot{}}{,}B}}{\overline{\left(B\underset{\dot{}}{,}B\right)+1}}=\frac{\overline{A\underset{\dot{}}{,}B}}{\left(B\underset{\dot{}}{,}B\right)+1}$$
138	135 137	eqtrd	$$⊢\phi \to \stackrel{‾}{\frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}}=\frac{\overline{A\underset{\dot{}}{,}B}}{\left(B\underset{\dot{}}{,}B\right)+1}$$
139	134 138	syl5eq	$$⊢\phi \to \bar{T}=\frac{\overline{A\underset{\dot{}}{,}B}}{\left(B\underset{\dot{}}{,}B\right)+1}$$
140	139	oveq2d	$$⊢\phi \to \left(A\underset{\dot{}}{,}B\right)\bar{T}=\left(A\underset{\dot{}}{,}B\right)\left(\frac{\overline{A\underset{\dot{}}{,}B}}{\left(B\underset{\dot{}}{,}B\right)+1}\right)$$
141	131 133 140	3eqtr4rd	$$⊢\phi \to \left(A\underset{\dot{}}{,}B\right)\bar{T}=\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{\left(B\underset{\dot{}}{,}B\right)+1}$$
142	125 129 141	3eqtrd	$$⊢\phi \to A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)=\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{\left(B\underset{\dot{}}{,}B\right)+1}$$
143	22	recnd	$$⊢\phi \to {\left|A\underset{\dot{}}{,}B\right|}^2\in ℂ$$
144	143 120	mulcomd	$$⊢\phi \to {\left|A\underset{\dot{}}{,}B\right|}^2\left(\left(B\underset{\dot{}}{,}B\right)+1\right)=\left(\left(B\underset{\dot{}}{,}B\right)+1\right){\left|A\underset{\dot{}}{,}B\right|}^2$$
145	120	sqvald	$$⊢\phi \to {\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2=\left(\left(B\underset{\dot{}}{,}B\right)+1\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)$$
146	144 145	oveq12d	$$⊢\phi \to \frac{{\left|A\underset{\dot{}}{,}B\right|}^2\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}=\frac{\left(\left(B\underset{\dot{}}{,}B\right)+1\right){\left|A\underset{\dot{}}{,}B\right|}^2}{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}$$
147	143 120 120 63 63	divcan5d	$$⊢\phi \to \frac{\left(\left(B\underset{\dot{}}{,}B\right)+1\right){\left|A\underset{\dot{}}{,}B\right|}^2}{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}=\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{\left(B\underset{\dot{}}{,}B\right)+1}$$
148	146 147	eqtr2d	$$⊢\phi \to \frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{\left(B\underset{\dot{}}{,}B\right)+1}=\frac{{\left|A\underset{\dot{}}{,}B\right|}^2\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}$$
149	93	rpcnd	$$⊢\phi \to {\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2\in ℂ$$
150	93	rpne0d	$$⊢\phi \to {\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2\ne 0$$
151	143 120 149 150	div23d	$$⊢\phi \to \frac{{\left|A\underset{\dot{}}{,}B\right|}^2\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)$$
152	142 148 151	3eqtrd	$$⊢\phi \to A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)$$
153	94 31	remulcld	$$⊢\phi \to \left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)\in ℝ$$
154	152 153	eqeltrd	$$⊢\phi \to A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\in ℝ$$
155	154	cjred	$$⊢\phi \to \overline{A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)}=A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)$$
156	5 1	cphipcj	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge T{\cdot }_{W}B\in V\right)\to \overline{A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)}=\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}A$$
157	14 9 76 156	syl3anc	$$⊢\phi \to \overline{A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)}=\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}A$$
158	155 157 152	3eqtr3d	$$⊢\phi \to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}A=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)$$
159	5 1 55 56 67	cph2ass	$$⊢\left(W\in \mathrm{CPreHil}\wedge \left(T\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge T\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\wedge \left(B\in V\wedge B\in V\right)\right)\to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)=T\bar{T}\left(B\underset{\dot{}}{,}B\right)$$
160	14 66 66 17 17 159	syl122anc	$$⊢\phi \to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)=T\bar{T}\left(B\underset{\dot{}}{,}B\right)$$
161	12	fveq2i	$$⊢\left|T\right|=\left|\frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}\right|$$
162	19 120 63	absdivd	$$⊢\phi \to \left|\frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}\right|=\frac{\left|A\underset{\dot{}}{,}B\right|}{\left|\left(B\underset{\dot{}}{,}B\right)+1\right|}$$
163	62	rpge0d	$$⊢\phi \to 0\le \left(B\underset{\dot{}}{,}B\right)+1$$
164	31 163	absidd	$$⊢\phi \to \left|\left(B\underset{\dot{}}{,}B\right)+1\right|=\left(B\underset{\dot{}}{,}B\right)+1$$
165	164	oveq2d	$$⊢\phi \to \frac{\left|A\underset{\dot{}}{,}B\right|}{\left|\left(B\underset{\dot{}}{,}B\right)+1\right|}=\frac{\left|A\underset{\dot{}}{,}B\right|}{\left(B\underset{\dot{}}{,}B\right)+1}$$
166	162 165	eqtrd	$$⊢\phi \to \left|\frac{A\underset{\dot{}}{,}B}{\left(B\underset{\dot{}}{,}B\right)+1}\right|=\frac{\left|A\underset{\dot{}}{,}B\right|}{\left(B\underset{\dot{}}{,}B\right)+1}$$
167	161 166	syl5eq	$$⊢\phi \to \left|T\right|=\frac{\left|A\underset{\dot{}}{,}B\right|}{\left(B\underset{\dot{}}{,}B\right)+1}$$
168	167	oveq1d	$$⊢\phi \to {\left|T\right|}^2={\left(\frac{\left|A\underset{\dot{}}{,}B\right|}{\left(B\underset{\dot{}}{,}B\right)+1}\right)}^2$$
169	127	absvalsqd	$$⊢\phi \to {\left|T\right|}^2=T\bar{T}$$
170	21 120 63	sqdivd	$$⊢\phi \to {\left(\frac{\left|A\underset{\dot{}}{,}B\right|}{\left(B\underset{\dot{}}{,}B\right)+1}\right)}^2=\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}$$
171	168 169 170	3eqtr3d	$$⊢\phi \to T\bar{T}=\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}$$
172	171	oveq1d	$$⊢\phi \to T\bar{T}\left(B\underset{\dot{}}{,}B\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(B\underset{\dot{}}{,}B\right)$$
173	160 172	eqtrd	$$⊢\phi \to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(B\underset{\dot{}}{,}B\right)$$
174	158 173	oveq12d	$$⊢\phi \to \left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}A\right)-\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(B\underset{\dot{}}{,}B\right)$$
175		pncan2	$$⊢\left(B\underset{\dot{}}{,}B\in ℂ\wedge 1\in ℂ\right)\to \left(B\underset{\dot{}}{,}B\right)+1-\left(B\underset{\dot{}}{,}B\right)=1$$
176	37 38 175	sylancl	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+1-\left(B\underset{\dot{}}{,}B\right)=1$$
177	176	oveq2d	$$⊢\phi \to \left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1-\left(B\underset{\dot{}}{,}B\right)\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\cdot 1$$
178	119 120 37	subdid	$$⊢\phi \to \left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1-\left(B\underset{\dot{}}{,}B\right)\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(B\underset{\dot{}}{,}B\right)$$
179	177 178	eqtr3d	$$⊢\phi \to \left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\cdot 1=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(B\underset{\dot{}}{,}B\right)$$
180	174 111 179	3eqtr4d	$$⊢\phi \to \left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\cdot 1$$
181	152 180	oveq12d	$$⊢\phi \to \left(A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)+\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+1\right)+\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\cdot 1$$
182	122 123 181	3eqtr4rd	$$⊢\phi \to \left(A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)+\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)$$
183	182	oveq2d	$$⊢\phi \to \left(A\underset{\dot{}}{,}A\right)-\left(\left(A\underset{\dot{}}{,}\left(T{\cdot }_{W}B\right)\right)+\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)\right)=\left(A\underset{\dot{}}{,}A\right)-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)$$
184	107 118 183	3eqtrd	$$⊢\phi \to \left(A\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)-\left(\left(T{\cdot }_{W}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)\right)=\left(A\underset{\dot{}}{,}A\right)-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)$$
185	102 104 184	3eqtrd	$$⊢\phi \to {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2=\left(A\underset{\dot{}}{,}A\right)-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)$$
186	99 96	negsubd	$$⊢\phi \to \left(A\underset{\dot{}}{,}A\right)+\left(-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)=\left(A\underset{\dot{}}{,}A\right)-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)$$
187	99 97	addcomd	$$⊢\phi \to \left(A\underset{\dot{}}{,}A\right)+\left(-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)=-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)+\left(A\underset{\dot{}}{,}A\right)$$
188	185 186 187	3eqtr2d	$$⊢\phi \to {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2=-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)+\left(A\underset{\dot{}}{,}A\right)$$
189	1 5 2	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to {N\left(A\right)}^2=A\underset{\dot{}}{,}A$$
190	14 9 189	syl2anc	$$⊢\phi \to {N\left(A\right)}^2=A\underset{\dot{}}{,}A$$
191	188 190	oveq12d	$$⊢\phi \to {N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2-{N\left(A\right)}^2=\left(-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)+\left(A\underset{\dot{}}{,}A\right)-\left(A\underset{\dot{}}{,}A\right)$$
192	28	renegcld	$$⊢\phi \to -\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\in ℝ$$
193	192	recnd	$$⊢\phi \to -\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\in ℂ$$
194	143 193 149 150	div23d	$$⊢\phi \to \frac{{\left|A\underset{\dot{}}{,}B\right|}^2\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}=\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)$$
195	28	recnd	$$⊢\phi \to \left(B\underset{\dot{}}{,}B\right)+2\in ℂ$$
196	119 195	mulneg2d	$$⊢\phi \to \left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)=-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)$$
197	194 196	eqtrd	$$⊢\phi \to \frac{{\left|A\underset{\dot{}}{,}B\right|}^2\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}=-\left(\frac{{\left|A\underset{\dot{}}{,}B\right|}^2}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)$$
198	100 191 197	3eqtr4rd	$$⊢\phi \to \frac{{\left|A\underset{\dot{}}{,}B\right|}^2\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}={N\left(A\underset{\dot{}}{-}\left(T{\cdot }_{W}B\right)\right)}^2-{N\left(A\right)}^2$$
199	90 198	breqtrrd	$$⊢\phi \to 0\le \frac{{\left|A\underset{\dot{}}{,}B\right|}^2\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}$$
200	22 192	remulcld	$$⊢\phi \to {\left|A\underset{\dot{}}{,}B\right|}^2\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)\in ℝ$$
201	200 93	ge0divd	$$⊢\phi \to \left(0\le {\left|A\underset{\dot{}}{,}B\right|}^2\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)\leftrightarrow 0\le \frac{{\left|A\underset{\dot{}}{,}B\right|}^2\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)}{{\left(\left(B\underset{\dot{}}{,}B\right)+1\right)}^2}\right)$$
202	199 201	mpbird	$$⊢\phi \to 0\le {\left|A\underset{\dot{}}{,}B\right|}^2\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)$$
203		mulneg12	$$⊢\left({\left|A\underset{\dot{}}{,}B\right|}^2\in ℂ\wedge \left(B\underset{\dot{}}{,}B\right)+2\in ℂ\right)\to \left(-{\left|A\underset{\dot{}}{,}B\right|}^2\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)={\left|A\underset{\dot{}}{,}B\right|}^2\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)$$
204	143 195 203	syl2anc	$$⊢\phi \to \left(-{\left|A\underset{\dot{}}{,}B\right|}^2\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)={\left|A\underset{\dot{}}{,}B\right|}^2\left(-\left(\left(B\underset{\dot{}}{,}B\right)+2\right)\right)$$
205	202 204	breqtrrd	$$⊢\phi \to 0\le \left(-{\left|A\underset{\dot{}}{,}B\right|}^2\right)\left(\left(B\underset{\dot{}}{,}B\right)+2\right)$$
206	23 47 205	prodge0ld	$$⊢\phi \to 0\le -{\left|A\underset{\dot{}}{,}B\right|}^2$$
207	22	le0neg1d	$$⊢\phi \to \left({\left|A\underset{\dot{}}{,}B\right|}^2\le 0\leftrightarrow 0\le -{\left|A\underset{\dot{}}{,}B\right|}^2\right)$$
208	206 207	mpbird	$$⊢\phi \to {\left|A\underset{\dot{}}{,}B\right|}^2\le 0$$
209	20	sqge0d	$$⊢\phi \to 0\le {\left|A\underset{\dot{}}{,}B\right|}^2$$
210		0re	$$⊢0\in ℝ$$
211		letri3	$$⊢\left({\left|A\underset{\dot{}}{,}B\right|}^2\in ℝ\wedge 0\in ℝ\right)\to \left({\left|A\underset{\dot{}}{,}B\right|}^2=0\leftrightarrow \left({\left|A\underset{\dot{}}{,}B\right|}^2\le 0\wedge 0\le {\left|A\underset{\dot{}}{,}B\right|}^2\right)\right)$$
212	22 210 211	sylancl	$$⊢\phi \to \left({\left|A\underset{\dot{}}{,}B\right|}^2=0\leftrightarrow \left({\left|A\underset{\dot{}}{,}B\right|}^2\le 0\wedge 0\le {\left|A\underset{\dot{}}{,}B\right|}^2\right)\right)$$
213	208 209 212	mpbir2and	$$⊢\phi \to {\left|A\underset{\dot{}}{,}B\right|}^2=0$$
214	21 213	sqeq0d	$$⊢\phi \to \left|A\underset{\dot{}}{,}B\right|=0$$
215	19 214	abs00d	$$⊢\phi \to A\underset{\dot{}}{,}B=0$$