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 = {Base}_{W}$
	pjthlem.n	$⊢ N = norm (W)$
	pjthlem.p	$⊢ \underset{˙}{+} = +_{W}$
	pjthlem.m	$⊢ \underset{˙}{-} = -_{W}$
	pjthlem.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	pjthlem.l	$⊢ L = LSubSp (W)$
	pjthlem.1	$⊢ φ \to W \in ℂHil$
	pjthlem.2	$⊢ φ \to U \in L$
	pjthlem.4	$⊢ φ \to A \in V$
	pjthlem.5	$⊢ φ \to B \in U$
	pjthlem.7	$⊢ φ \to \forall x \in U N (A) \leq N (A \underset{˙}{-} x)$
	pjthlem.8	$⊢ T = \frac{A \underset{˙}{,} B}{(B \underset{˙}{,} B) + 1}$
Assertion	pjthlem1	$⊢ φ \to A \underset{˙}{,} B = 0$

Proof

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

Metamath Proof Explorer

Theorem pjthlem1

Proof