siilem1

Description: Lemma for sii . (Contributed by NM, 23-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$
	sii1.3	$⊢ M = -_{v} (U)$
	sii1.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	sii1.c	$⊢ C \in ℂ$
	sii1.r	$⊢ C (A P B) \in ℝ$
	sii1.z	$⊢ 0 \leq C (A P B)$
Assertion	siilem1	$⊢ B P A = C {N (B)}^{2} \to \sqrt{(A P B) C {N (B)}^{2}} \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		sii1.3	$⊢ M = -_{v} (U)$
8		sii1.4	$⊢ S = \cdot_{𝑠OLD} (U)$
9		sii1.c	$⊢ C \in ℂ$
10		sii1.r	$⊢ C (A P B) \in ℝ$
11		sii1.z	$⊢ 0 \leq C (A P B)$
12	4	phnvi	$⊢ U \in NrmCVec$
13	9	cjcli	$⊢ \overline{C} \in ℂ$
14	1 8	nvscl	$⊢ (U \in NrmCVec \land \overline{C} \in ℂ \land B \in X) \to \overline{C} S B \in X$
15	12 13 6 14	mp3an	$⊢ \overline{C} S B \in X$
16	1 7	nvmcl	$⊢ (U \in NrmCVec \land A \in X \land \overline{C} S B \in X) \to A M (\overline{C} S B) \in X$
17	12 5 15 16	mp3an	$⊢ A M (\overline{C} S B) \in X$
18	1 2 12 17	nvcli	$⊢ N (A M (\overline{C} S B)) \in ℝ$
19	18	sqge0i	$⊢ 0 \leq {N (A M (\overline{C} S B))}^{2}$
20	17 5 15	3pm3.2i	$⊢ (A M (\overline{C} S B) \in X \land A \in X \land \overline{C} S B \in X)$
21	1 7 3	dipsubdi	$⊢ (U \in {CPreHil}_{OLD} \land (A M (\overline{C} S B) \in X \land A \in X \land \overline{C} S B \in X)) \to (A M (\overline{C} S B)) P (A M (\overline{C} S B)) = ((A M (\overline{C} S B)) P A) - ((A M (\overline{C} S B)) P (\overline{C} S B))$
22	4 20 21	mp2an	$⊢ (A M (\overline{C} S B)) P (A M (\overline{C} S B)) = ((A M (\overline{C} S B)) P A) - ((A M (\overline{C} S B)) P (\overline{C} S B))$
23	1 2 3	ipidsq	$⊢ (U \in NrmCVec \land A M (\overline{C} S B) \in X) \to (A M (\overline{C} S B)) P (A M (\overline{C} S B)) = {N (A M (\overline{C} S B))}^{2}$
24	12 17 23	mp2an	$⊢ (A M (\overline{C} S B)) P (A M (\overline{C} S B)) = {N (A M (\overline{C} S B))}^{2}$
25	13 6 15	3pm3.2i	$⊢ (\overline{C} \in ℂ \land B \in X \land \overline{C} S B \in X)$
26	1 8 3	dipass	$⊢ (U \in {CPreHil}_{OLD} \land (\overline{C} \in ℂ \land B \in X \land \overline{C} S B \in X)) \to (\overline{C} S B) P (\overline{C} S B) = \overline{C} (B P (\overline{C} S B))$
27	4 25 26	mp2an	$⊢ (\overline{C} S B) P (\overline{C} S B) = \overline{C} (B P (\overline{C} S B))$
28	6 9 6	3pm3.2i	$⊢ (B \in X \land C \in ℂ \land B \in X)$
29	1 8 3	dipassr2	$⊢ (U \in {CPreHil}_{OLD} \land (B \in X \land C \in ℂ \land B \in X)) \to B P (\overline{C} S B) = C (B P B)$
30	4 28 29	mp2an	$⊢ B P (\overline{C} S B) = C (B P B)$
31	1 2 3	ipidsq	$⊢ (U \in NrmCVec \land B \in X) \to B P B = {N (B)}^{2}$
32	12 6 31	mp2an	$⊢ B P B = {N (B)}^{2}$
33	32	oveq2i	$⊢ C (B P B) = C {N (B)}^{2}$
34	30 33	eqtri	$⊢ B P (\overline{C} S B) = C {N (B)}^{2}$
35	34	oveq2i	$⊢ \overline{C} (B P (\overline{C} S B)) = \overline{C} C {N (B)}^{2}$
36	27 35	eqtri	$⊢ (\overline{C} S B) P (\overline{C} S B) = \overline{C} C {N (B)}^{2}$
37	36	oveq2i	$⊢ C (A P B) - ((\overline{C} S B) P (\overline{C} S B)) = C (A P B) - \overline{C} C {N (B)}^{2}$
38	37	oveq2i	$⊢ {N (A)}^{2} - \overline{C} (B P A) - (C (A P B) - ((\overline{C} S B) P (\overline{C} S B))) = {N (A)}^{2} - \overline{C} (B P A) - (C (A P B) - \overline{C} C {N (B)}^{2})$
39	1 2 12 5	nvcli	$⊢ N (A) \in ℝ$
40	39	recni	$⊢ N (A) \in ℂ$
41	40	sqcli	$⊢ {N (A)}^{2} \in ℂ$
42	1 3	dipcl	$⊢ (U \in NrmCVec \land B \in X \land A \in X) \to B P A \in ℂ$
43	12 6 5 42	mp3an	$⊢ B P A \in ℂ$
44	13 43	mulcli	$⊢ \overline{C} (B P A) \in ℂ$
45	10	recni	$⊢ C (A P B) \in ℂ$
46	1 2 12 6	nvcli	$⊢ N (B) \in ℝ$
47	46	recni	$⊢ N (B) \in ℂ$
48	47	sqcli	$⊢ {N (B)}^{2} \in ℂ$
49	9 48	mulcli	$⊢ C {N (B)}^{2} \in ℂ$
50	13 49	mulcli	$⊢ \overline{C} C {N (B)}^{2} \in ℂ$
51		sub4	$⊢ (({N (A)}^{2} \in ℂ \land \overline{C} (B P A) \in ℂ) \land (C (A P B) \in ℂ \land \overline{C} C {N (B)}^{2} \in ℂ)) \to {N (A)}^{2} - \overline{C} (B P A) - (C (A P B) - \overline{C} C {N (B)}^{2}) = {N (A)}^{2} - C (A P B) - (\overline{C} (B P A) - \overline{C} C {N (B)}^{2})$
52	41 44 45 50 51	mp4an	$⊢ {N (A)}^{2} - \overline{C} (B P A) - (C (A P B) - \overline{C} C {N (B)}^{2}) = {N (A)}^{2} - C (A P B) - (\overline{C} (B P A) - \overline{C} C {N (B)}^{2})$
53	38 52	eqtri	$⊢ {N (A)}^{2} - \overline{C} (B P A) - (C (A P B) - ((\overline{C} S B) P (\overline{C} S B))) = {N (A)}^{2} - C (A P B) - (\overline{C} (B P A) - \overline{C} C {N (B)}^{2})$
54	5 15 5	3pm3.2i	$⊢ (A \in X \land \overline{C} S B \in X \land A \in X)$
55	1 7 3	dipsubdir	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land \overline{C} S B \in X \land A \in X)) \to (A M (\overline{C} S B)) P A = (A P A) - ((\overline{C} S B) P A)$
56	4 54 55	mp2an	$⊢ (A M (\overline{C} S B)) P A = (A P A) - ((\overline{C} S B) P A)$
57	1 2 3	ipidsq	$⊢ (U \in NrmCVec \land A \in X) \to A P A = {N (A)}^{2}$
58	12 5 57	mp2an	$⊢ A P A = {N (A)}^{2}$
59	13 6 5	3pm3.2i	$⊢ (\overline{C} \in ℂ \land B \in X \land A \in X)$
60	1 8 3	dipass	$⊢ (U \in {CPreHil}_{OLD} \land (\overline{C} \in ℂ \land B \in X \land A \in X)) \to (\overline{C} S B) P A = \overline{C} (B P A)$
61	4 59 60	mp2an	$⊢ (\overline{C} S B) P A = \overline{C} (B P A)$
62	58 61	oveq12i	$⊢ (A P A) - ((\overline{C} S B) P A) = {N (A)}^{2} - \overline{C} (B P A)$
63	56 62	eqtri	$⊢ (A M (\overline{C} S B)) P A = {N (A)}^{2} - \overline{C} (B P A)$
64	5 15 15	3pm3.2i	$⊢ (A \in X \land \overline{C} S B \in X \land \overline{C} S B \in X)$
65	1 7 3	dipsubdir	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land \overline{C} S B \in X \land \overline{C} S B \in X)) \to (A M (\overline{C} S B)) P (\overline{C} S B) = (A P (\overline{C} S B)) - ((\overline{C} S B) P (\overline{C} S B))$
66	4 64 65	mp2an	$⊢ (A M (\overline{C} S B)) P (\overline{C} S B) = (A P (\overline{C} S B)) - ((\overline{C} S B) P (\overline{C} S B))$
67	5 9 6	3pm3.2i	$⊢ (A \in X \land C \in ℂ \land B \in X)$
68	1 8 3	dipassr2	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land C \in ℂ \land B \in X)) \to A P (\overline{C} S B) = C (A P B)$
69	4 67 68	mp2an	$⊢ A P (\overline{C} S B) = C (A P B)$
70	69	oveq1i	$⊢ (A P (\overline{C} S B)) - ((\overline{C} S B) P (\overline{C} S B)) = C (A P B) - ((\overline{C} S B) P (\overline{C} S B))$
71	66 70	eqtri	$⊢ (A M (\overline{C} S B)) P (\overline{C} S B) = C (A P B) - ((\overline{C} S B) P (\overline{C} S B))$
72	63 71	oveq12i	$⊢ ((A M (\overline{C} S B)) P A) - ((A M (\overline{C} S B)) P (\overline{C} S B)) = {N (A)}^{2} - \overline{C} (B P A) - (C (A P B) - ((\overline{C} S B) P (\overline{C} S B)))$
73	13 43 49	subdii	$⊢ \overline{C} ((B P A) - C {N (B)}^{2}) = \overline{C} (B P A) - \overline{C} C {N (B)}^{2}$
74	73	oveq2i	$⊢ {N (A)}^{2} - C (A P B) - \overline{C} ((B P A) - C {N (B)}^{2}) = {N (A)}^{2} - C (A P B) - (\overline{C} (B P A) - \overline{C} C {N (B)}^{2})$
75	53 72 74	3eqtr4i	$⊢ ((A M (\overline{C} S B)) P A) - ((A M (\overline{C} S B)) P (\overline{C} S B)) = {N (A)}^{2} - C (A P B) - \overline{C} ((B P A) - C {N (B)}^{2})$
76	22 24 75	3eqtr3i	$⊢ {N (A M (\overline{C} S B))}^{2} = {N (A)}^{2} - C (A P B) - \overline{C} ((B P A) - C {N (B)}^{2})$
77	19 76	breqtri	$⊢ 0 \leq {N (A)}^{2} - C (A P B) - \overline{C} ((B P A) - C {N (B)}^{2})$
78	43 49	subeq0i	$⊢ (B P A) - C {N (B)}^{2} = 0 \leftrightarrow B P A = C {N (B)}^{2}$
79		oveq2	$⊢ (B P A) - C {N (B)}^{2} = 0 \to \overline{C} ((B P A) - C {N (B)}^{2}) = \overline{C} \cdot 0$
80	13	mul01i	$⊢ \overline{C} \cdot 0 = 0$
81	79 80	eqtrdi	$⊢ (B P A) - C {N (B)}^{2} = 0 \to \overline{C} ((B P A) - C {N (B)}^{2}) = 0$
82	78 81	sylbir	$⊢ B P A = C {N (B)}^{2} \to \overline{C} ((B P A) - C {N (B)}^{2}) = 0$
83	82	oveq2d	$⊢ B P A = C {N (B)}^{2} \to {N (A)}^{2} - C (A P B) - \overline{C} ((B P A) - C {N (B)}^{2}) = {N (A)}^{2} - C (A P B) - 0$
84	39	resqcli	$⊢ {N (A)}^{2} \in ℝ$
85	84	recni	$⊢ {N (A)}^{2} \in ℂ$
86	85 45	subcli	$⊢ {N (A)}^{2} - C (A P B) \in ℂ$
87	86	subid1i	$⊢ {N (A)}^{2} - C (A P B) - 0 = {N (A)}^{2} - C (A P B)$
88	83 87	eqtrdi	$⊢ B P A = C {N (B)}^{2} \to {N (A)}^{2} - C (A P B) - \overline{C} ((B P A) - C {N (B)}^{2}) = {N (A)}^{2} - C (A P B)$
89	77 88	breqtrid	$⊢ B P A = C {N (B)}^{2} \to 0 \leq {N (A)}^{2} - C (A P B)$
90	84 10	subge0i	$⊢ 0 \leq {N (A)}^{2} - C (A P B) \leftrightarrow C (A P B) \leq {N (A)}^{2}$
91	89 90	sylib	$⊢ B P A = C {N (B)}^{2} \to C (A P B) \leq {N (A)}^{2}$
92	46	resqcli	$⊢ {N (B)}^{2} \in ℝ$
93	46	sqge0i	$⊢ 0 \leq {N (B)}^{2}$
94	92 93	pm3.2i	$⊢ ({N (B)}^{2} \in ℝ \land 0 \leq {N (B)}^{2})$
95	10 84 94	3pm3.2i	$⊢ (C (A P B) \in ℝ \land {N (A)}^{2} \in ℝ \land ({N (B)}^{2} \in ℝ \land 0 \leq {N (B)}^{2}))$
96		lemul1a	$⊢ ((C (A P B) \in ℝ \land {N (A)}^{2} \in ℝ \land ({N (B)}^{2} \in ℝ \land 0 \leq {N (B)}^{2})) \land C (A P B) \leq {N (A)}^{2}) \to C (A P B) {N (B)}^{2} \leq {N (A)}^{2} {N (B)}^{2}$
97	95 96	mpan	$⊢ C (A P B) \leq {N (A)}^{2} \to C (A P B) {N (B)}^{2} \leq {N (A)}^{2} {N (B)}^{2}$
98	91 97	syl	$⊢ B P A = C {N (B)}^{2} \to C (A P B) {N (B)}^{2} \leq {N (A)}^{2} {N (B)}^{2}$
99	40 47	sqmuli	$⊢ {N (A) N (B)}^{2} = {N (A)}^{2} {N (B)}^{2}$
100	98 99	breqtrrdi	$⊢ B P A = C {N (B)}^{2} \to C (A P B) {N (B)}^{2} \leq {N (A) N (B)}^{2}$
101	10 92	mulge0i	$⊢ (0 \leq C (A P B) \land 0 \leq {N (B)}^{2}) \to 0 \leq C (A P B) {N (B)}^{2}$
102	11 93 101	mp2an	$⊢ 0 \leq C (A P B) {N (B)}^{2}$
103	39 46	remulcli	$⊢ N (A) N (B) \in ℝ$
104	103	sqge0i	$⊢ 0 \leq {N (A) N (B)}^{2}$
105	10 92	remulcli	$⊢ C (A P B) {N (B)}^{2} \in ℝ$
106	103	resqcli	$⊢ {N (A) N (B)}^{2} \in ℝ$
107	105 106	sqrtlei	$⊢ (0 \leq C (A P B) {N (B)}^{2} \land 0 \leq {N (A) N (B)}^{2}) \to (C (A P B) {N (B)}^{2} \leq {N (A) N (B)}^{2} \leftrightarrow \sqrt{C (A P B) {N (B)}^{2}} \leq \sqrt{{N (A) N (B)}^{2}})$
108	102 104 107	mp2an	$⊢ C (A P B) {N (B)}^{2} \leq {N (A) N (B)}^{2} \leftrightarrow \sqrt{C (A P B) {N (B)}^{2}} \leq \sqrt{{N (A) N (B)}^{2}}$
109	100 108	sylib	$⊢ B P A = C {N (B)}^{2} \to \sqrt{C (A P B) {N (B)}^{2}} \leq \sqrt{{N (A) N (B)}^{2}}$
110	1 3	dipcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B \in ℂ$
111	12 5 6 110	mp3an	$⊢ A P B \in ℂ$
112	9 111	mulcomi	$⊢ C (A P B) = (A P B) C$
113	112	oveq1i	$⊢ C (A P B) {N (B)}^{2} = (A P B) C {N (B)}^{2}$
114	92	recni	$⊢ {N (B)}^{2} \in ℂ$
115	111 9 114	mulassi	$⊢ (A P B) C {N (B)}^{2} = (A P B) C {N (B)}^{2}$
116	113 115	eqtri	$⊢ C (A P B) {N (B)}^{2} = (A P B) C {N (B)}^{2}$
117	116	fveq2i	$⊢ \sqrt{C (A P B) {N (B)}^{2}} = \sqrt{(A P B) C {N (B)}^{2}}$
118	1 2	nvge0	$⊢ (U \in NrmCVec \land A \in X) \to 0 \leq N (A)$
119	12 5 118	mp2an	$⊢ 0 \leq N (A)$
120	1 2	nvge0	$⊢ (U \in NrmCVec \land B \in X) \to 0 \leq N (B)$
121	12 6 120	mp2an	$⊢ 0 \leq N (B)$
122	39 46	mulge0i	$⊢ (0 \leq N (A) \land 0 \leq N (B)) \to 0 \leq N (A) N (B)$
123	119 121 122	mp2an	$⊢ 0 \leq N (A) N (B)$
124	103	sqrtsqi	$⊢ 0 \leq N (A) N (B) \to \sqrt{{N (A) N (B)}^{2}} = N (A) N (B)$
125	123 124	ax-mp	$⊢ \sqrt{{N (A) N (B)}^{2}} = N (A) N (B)$
126	109 117 125	3brtr3g	$⊢ B P A = C {N (B)}^{2} \to \sqrt{(A P B) C {N (B)}^{2}} \leq N (A) N (B)$

Metamath Proof Explorer

Theorem siilem1

Proof