siii

Description: Inference from sii . (Contributed by NM, 20-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	siii.1	$⊢ X = BaseSet (U)$
	siii.6	$⊢ N = {norm}_{CV} (U)$
	siii.7	$⊢ P = \cdot_{𝑖OLD} (U)$
	siii.9	$⊢ U \in {CPreHil}_{OLD}$
	siii.a	$⊢ A \in X$
	siii.b	$⊢ B \in X$
Assertion	siii	$⊢ \|A P B\| \leq N (A) N (B)$

Proof

Step	Hyp	Ref	Expression
1		siii.1	$⊢ X = BaseSet (U)$
2		siii.6	$⊢ N = {norm}_{CV} (U)$
3		siii.7	$⊢ P = \cdot_{𝑖OLD} (U)$
4		siii.9	$⊢ U \in {CPreHil}_{OLD}$
5		siii.a	$⊢ A \in X$
6		siii.b	$⊢ B \in X$
7		oveq2	$⊢ B = 0_{vec} (U) \to A P B = A P 0_{vec} (U)$
8	4	phnvi	$⊢ U \in NrmCVec$
9		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
10	1 9 3	dip0r	$⊢ (U \in NrmCVec \land A \in X) \to A P 0_{vec} (U) = 0$
11	8 5 10	mp2an	$⊢ A P 0_{vec} (U) = 0$
12	7 11	eqtrdi	$⊢ B = 0_{vec} (U) \to A P B = 0$
13	12	abs00bd	$⊢ B = 0_{vec} (U) \to \|A P B\| = 0$
14	1 2	nvge0	$⊢ (U \in NrmCVec \land A \in X) \to 0 \leq N (A)$
15	8 5 14	mp2an	$⊢ 0 \leq N (A)$
16	1 2	nvge0	$⊢ (U \in NrmCVec \land B \in X) \to 0 \leq N (B)$
17	8 6 16	mp2an	$⊢ 0 \leq N (B)$
18	1 2 8 5	nvcli	$⊢ N (A) \in ℝ$
19	1 2 8 6	nvcli	$⊢ N (B) \in ℝ$
20	18 19	mulge0i	$⊢ (0 \leq N (A) \land 0 \leq N (B)) \to 0 \leq N (A) N (B)$
21	15 17 20	mp2an	$⊢ 0 \leq N (A) N (B)$
22	13 21	eqbrtrdi	$⊢ B = 0_{vec} (U) \to \|A P B\| \leq N (A) N (B)$
23	1 3	dipcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B \in ℂ$
24	8 5 6 23	mp3an	$⊢ A P B \in ℂ$
25		absval	$⊢ A P B \in ℂ \to \|A P B\| = \sqrt{(A P B) \overline{A P B}}$
26	24 25	ax-mp	$⊢ \|A P B\| = \sqrt{(A P B) \overline{A P B}}$
27	19	recni	$⊢ N (B) \in ℂ$
28	27	sqeq0i	$⊢ {N (B)}^{2} = 0 \leftrightarrow N (B) = 0$
29	1 9 2	nvz	$⊢ (U \in NrmCVec \land B \in X) \to (N (B) = 0 \leftrightarrow B = 0_{vec} (U))$
30	8 6 29	mp2an	$⊢ N (B) = 0 \leftrightarrow B = 0_{vec} (U)$
31	28 30	bitri	$⊢ {N (B)}^{2} = 0 \leftrightarrow B = 0_{vec} (U)$
32	31	necon3bii	$⊢ {N (B)}^{2} \neq 0 \leftrightarrow B \neq 0_{vec} (U)$
33	1 3	dipcl	$⊢ (U \in NrmCVec \land B \in X \land A \in X) \to B P A \in ℂ$
34	8 6 5 33	mp3an	$⊢ B P A \in ℂ$
35	19	resqcli	$⊢ {N (B)}^{2} \in ℝ$
36	35	recni	$⊢ {N (B)}^{2} \in ℂ$
37	34 36	divcan1zi	$⊢ {N (B)}^{2} \neq 0 \to (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2} = B P A$
38	32 37	sylbir	$⊢ B \neq 0_{vec} (U) \to (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2} = B P A$
39	1 3	dipcj	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to \overline{A P B} = B P A$
40	8 5 6 39	mp3an	$⊢ \overline{A P B} = B P A$
41	38 40	eqtr4di	$⊢ B \neq 0_{vec} (U) \to (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2} = \overline{A P B}$
42	41	oveq2d	$⊢ B \neq 0_{vec} (U) \to (A P B) (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2} = (A P B) \overline{A P B}$
43	42	fveq2d	$⊢ B \neq 0_{vec} (U) \to \sqrt{(A P B) (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2}} = \sqrt{(A P B) \overline{A P B}}$
44	26 43	eqtr4id	$⊢ B \neq 0_{vec} (U) \to \|A P B\| = \sqrt{(A P B) (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2}}$
45	38	eqcomd	$⊢ B \neq 0_{vec} (U) \to B P A = (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2}$
46	34 36	divclzi	$⊢ {N (B)}^{2} \neq 0 \to \frac{B P A}{{N (B)}^{2}} \in ℂ$
47	32 46	sylbir	$⊢ B \neq 0_{vec} (U) \to \frac{B P A}{{N (B)}^{2}} \in ℂ$
48	1 3	ipipcj	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (A P B) (B P A) = {\|A P B\|}^{2}$
49	8 5 6 48	mp3an	$⊢ (A P B) (B P A) = {\|A P B\|}^{2}$
50	24 34 49	mulcomli	$⊢ (B P A) (A P B) = {\|A P B\|}^{2}$
51	50	oveq1i	$⊢ \frac{(B P A) (A P B)}{{N (B)}^{2}} = \frac{{\|A P B\|}^{2}}{{N (B)}^{2}}$
52		div23	$⊢ (B P A \in ℂ \land A P B \in ℂ \land ({N (B)}^{2} \in ℂ \land {N (B)}^{2} \neq 0)) \to \frac{(B P A) (A P B)}{{N (B)}^{2}} = (\frac{B P A}{{N (B)}^{2}}) (A P B)$
53	34 24 52	mp3an12	$⊢ ({N (B)}^{2} \in ℂ \land {N (B)}^{2} \neq 0) \to \frac{(B P A) (A P B)}{{N (B)}^{2}} = (\frac{B P A}{{N (B)}^{2}}) (A P B)$
54	36 53	mpan	$⊢ {N (B)}^{2} \neq 0 \to \frac{(B P A) (A P B)}{{N (B)}^{2}} = (\frac{B P A}{{N (B)}^{2}}) (A P B)$
55	32 54	sylbir	$⊢ B \neq 0_{vec} (U) \to \frac{(B P A) (A P B)}{{N (B)}^{2}} = (\frac{B P A}{{N (B)}^{2}}) (A P B)$
56	51 55	syl5reqr	$⊢ B \neq 0_{vec} (U) \to (\frac{B P A}{{N (B)}^{2}}) (A P B) = \frac{{\|A P B\|}^{2}}{{N (B)}^{2}}$
57	24	abscli	$⊢ \|A P B\| \in ℝ$
58	57	resqcli	$⊢ {\|A P B\|}^{2} \in ℝ$
59	58 35	redivclzi	$⊢ {N (B)}^{2} \neq 0 \to \frac{{\|A P B\|}^{2}}{{N (B)}^{2}} \in ℝ$
60	32 59	sylbir	$⊢ B \neq 0_{vec} (U) \to \frac{{\|A P B\|}^{2}}{{N (B)}^{2}} \in ℝ$
61	56 60	eqeltrd	$⊢ B \neq 0_{vec} (U) \to (\frac{B P A}{{N (B)}^{2}}) (A P B) \in ℝ$
62	30	necon3bii	$⊢ N (B) \neq 0 \leftrightarrow B \neq 0_{vec} (U)$
63	19	sqgt0i	$⊢ N (B) \neq 0 \to 0 < {N (B)}^{2}$
64	62 63	sylbir	$⊢ B \neq 0_{vec} (U) \to 0 < {N (B)}^{2}$
65	57	sqge0i	$⊢ 0 \leq {\|A P B\|}^{2}$
66		divge0	$⊢ (({\|A P B\|}^{2} \in ℝ \land 0 \leq {\|A P B\|}^{2}) \land ({N (B)}^{2} \in ℝ \land 0 < {N (B)}^{2})) \to 0 \leq \frac{{\|A P B\|}^{2}}{{N (B)}^{2}}$
67	58 65 66	mpanl12	$⊢ ({N (B)}^{2} \in ℝ \land 0 < {N (B)}^{2}) \to 0 \leq \frac{{\|A P B\|}^{2}}{{N (B)}^{2}}$
68	35 64 67	sylancr	$⊢ B \neq 0_{vec} (U) \to 0 \leq \frac{{\|A P B\|}^{2}}{{N (B)}^{2}}$
69	68 56	breqtrrd	$⊢ B \neq 0_{vec} (U) \to 0 \leq (\frac{B P A}{{N (B)}^{2}}) (A P B)$
70		eqid	$⊢ -_{v} (U) = -_{v} (U)$
71		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
72	1 2 3 4 5 6 70 71	siilem2	$⊢ (\frac{B P A}{{N (B)}^{2}} \in ℂ \land (\frac{B P A}{{N (B)}^{2}}) (A P B) \in ℝ \land 0 \leq (\frac{B P A}{{N (B)}^{2}}) (A P B)) \to (B P A = (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2} \to \sqrt{(A P B) (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2}} \leq N (A) N (B))$
73	47 61 69 72	syl3anc	$⊢ B \neq 0_{vec} (U) \to (B P A = (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2} \to \sqrt{(A P B) (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2}} \leq N (A) N (B))$
74	45 73	mpd	$⊢ B \neq 0_{vec} (U) \to \sqrt{(A P B) (\frac{B P A}{{N (B)}^{2}}) {N (B)}^{2}} \leq N (A) N (B)$
75	44 74	eqbrtrd	$⊢ B \neq 0_{vec} (U) \to \|A P B\| \leq N (A) N (B)$
76	22 75	pm2.61ine	$⊢ \|A P B\| \leq N (A) N (B)$

Metamath Proof Explorer

Theorem siii

Proof