Metamath Proof Explorer


Theorem 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 = 𝑖OLD U
siii.9 U CPreHil OLD
siii.a A X
siii.b B X
sii1.3 M = - v U
sii1.4 S = 𝑠OLD U
sii1.c C
sii1.r C A P B
sii1.z 0 C A P B
Assertion siilem1 B P A = C N B 2 A P B C N B 2 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 = 𝑖OLD U
4 siii.9 U CPreHil OLD
5 siii.a A X
6 siii.b B X
7 sii1.3 M = - v U
8 sii1.4 S = 𝑠OLD U
9 sii1.c C
10 sii1.r C A P B
11 sii1.z 0 C A P B
12 4 phnvi U NrmCVec
13 9 cjcli C
14 1 8 nvscl U NrmCVec C B X C S B X
15 12 13 6 14 mp3an C S B X
16 1 7 nvmcl U NrmCVec A X C S B X A M C S B X
17 12 5 15 16 mp3an A M C S B X
18 1 2 12 17 nvcli N A M C S B
19 18 sqge0i 0 N A M C S B 2
20 17 5 15 3pm3.2i A M C S B X A X C S B X
21 1 7 3 dipsubdi U CPreHil OLD A M C S B X A X C S B X A M C S B P A M C S B = A M C S B P A A M C S B P C S B
22 4 20 21 mp2an A M C S B P A M C S B = A M C S B P A A M C S B P C S B
23 1 2 3 ipidsq U NrmCVec A M C S B X A M C S B P A M C S B = N A M C S B 2
24 12 17 23 mp2an A M C S B P A M C S B = N A M C S B 2
25 13 6 15 3pm3.2i C B X C S B X
26 1 8 3 dipass U CPreHil OLD C B X C S B X C S B P C S B = C B P C S B
27 4 25 26 mp2an C S B P C S B = C B P C S B
28 6 9 6 3pm3.2i B X C B X
29 1 8 3 dipassr2 U CPreHil OLD B X C B X B P C S B = C B P B
30 4 28 29 mp2an B P C S B = C B P B
31 1 2 3 ipidsq U NrmCVec B X 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 C S B = C N B 2
35 34 oveq2i C B P C S B = C C N B 2
36 27 35 eqtri C S B P C S B = C C N B 2
37 36 oveq2i C A P B C S B P C S B = C A P B C C N B 2
38 37 oveq2i N A 2 - C B P A - C A P B C S B P C S B = N A 2 - C B P A - C A P B C C N B 2
39 1 2 12 5 nvcli N A
40 39 recni N A
41 40 sqcli N A 2
42 1 3 dipcl U NrmCVec B X A X B P A
43 12 6 5 42 mp3an B P A
44 13 43 mulcli C B P A
45 10 recni C A P B
46 1 2 12 6 nvcli N B
47 46 recni N B
48 47 sqcli N B 2
49 9 48 mulcli C N B 2
50 13 49 mulcli C C N B 2
51 sub4 N A 2 C B P A C A P B C C N B 2 N A 2 - C B P A - C A P B C C N B 2 = N A 2 - C A P B - C B P A C C N B 2
52 41 44 45 50 51 mp4an N A 2 - C B P A - C A P B C C N B 2 = N A 2 - C A P B - C B P A C C N B 2
53 38 52 eqtri N A 2 - C B P A - C A P B C S B P C S B = N A 2 - C A P B - C B P A C C N B 2
54 5 15 5 3pm3.2i A X C S B X A X
55 1 7 3 dipsubdir U CPreHil OLD A X C S B X A X A M C S B P A = A P A C S B P A
56 4 54 55 mp2an A M C S B P A = A P A C S B P A
57 1 2 3 ipidsq U NrmCVec A X A P A = N A 2
58 12 5 57 mp2an A P A = N A 2
59 13 6 5 3pm3.2i C B X A X
60 1 8 3 dipass U CPreHil OLD C B X A X C S B P A = C B P A
61 4 59 60 mp2an C S B P A = C B P A
62 58 61 oveq12i A P A C S B P A = N A 2 C B P A
63 56 62 eqtri A M C S B P A = N A 2 C B P A
64 5 15 15 3pm3.2i A X C S B X C S B X
65 1 7 3 dipsubdir U CPreHil OLD A X C S B X C S B X A M C S B P C S B = A P C S B C S B P C S B
66 4 64 65 mp2an A M C S B P C S B = A P C S B C S B P C S B
67 5 9 6 3pm3.2i A X C B X
68 1 8 3 dipassr2 U CPreHil OLD A X C B X A P C S B = C A P B
69 4 67 68 mp2an A P C S B = C A P B
70 69 oveq1i A P C S B C S B P C S B = C A P B C S B P C S B
71 66 70 eqtri A M C S B P C S B = C A P B C S B P C S B
72 63 71 oveq12i A M C S B P A A M C S B P C S B = N A 2 - C B P A - C A P B C S B P C S B
73 13 43 49 subdii C B P A C N B 2 = C B P A C C N B 2
74 73 oveq2i N A 2 - C A P B - C B P A C N B 2 = N A 2 - C A P B - C B P A C C N B 2
75 53 72 74 3eqtr4i A M C S B P A A M C S B P C S B = N A 2 - C A P B - C B P A C N B 2
76 22 24 75 3eqtr3i N A M C S B 2 = N A 2 - C A P B - C B P A C N B 2
77 19 76 breqtri 0 N A 2 - C A P B - C B P A C N B 2
78 43 49 subeq0i B P A C N B 2 = 0 B P A = C N B 2
79 oveq2 B P A C N B 2 = 0 C B P A C N B 2 = C 0
80 13 mul01i C 0 = 0
81 79 80 eqtrdi B P A C N B 2 = 0 C B P A C N B 2 = 0
82 78 81 sylbir B P A = C N B 2 C B P A C N B 2 = 0
83 82 oveq2d B P A = C N B 2 N A 2 - C A P B - C B P A C N B 2 = N A 2 - C A P B - 0
84 39 resqcli N A 2
85 84 recni N A 2
86 85 45 subcli N A 2 C A P B
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 N A 2 - C A P B - 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 0 N A 2 C A P B
90 84 10 subge0i 0 N A 2 C A P B C A P B N A 2
91 89 90 sylib B P A = C N B 2 C A P B N A 2
92 46 resqcli N B 2
93 46 sqge0i 0 N B 2
94 92 93 pm3.2i N B 2 0 N B 2
95 10 84 94 3pm3.2i C A P B N A 2 N B 2 0 N B 2
96 lemul1a C A P B N A 2 N B 2 0 N B 2 C A P B N A 2 C A P B N B 2 N A 2 N B 2
97 95 96 mpan C A P B N A 2 C A P B N B 2 N A 2 N B 2
98 91 97 syl B P A = C N B 2 C A P B N B 2 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 C A P B N B 2 N A N B 2
101 10 92 mulge0i 0 C A P B 0 N B 2 0 C A P B N B 2
102 11 93 101 mp2an 0 C A P B N B 2
103 39 46 remulcli N A N B
104 103 sqge0i 0 N A N B 2
105 10 92 remulcli C A P B N B 2
106 103 resqcli N A N B 2
107 105 106 sqrtlei 0 C A P B N B 2 0 N A N B 2 C A P B N B 2 N A N B 2 C A P B N B 2 N A N B 2
108 102 104 107 mp2an C A P B N B 2 N A N B 2 C A P B N B 2 N A N B 2
109 100 108 sylib B P A = C N B 2 C A P B N B 2 N A N B 2
110 1 3 dipcl U NrmCVec A X B X A P B
111 12 5 6 110 mp3an A P B
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
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 C A P B N B 2 = A P B C N B 2
118 1 2 nvge0 U NrmCVec A X 0 N A
119 12 5 118 mp2an 0 N A
120 1 2 nvge0 U NrmCVec B X 0 N B
121 12 6 120 mp2an 0 N B
122 39 46 mulge0i 0 N A 0 N B 0 N A N B
123 119 121 122 mp2an 0 N A N B
124 103 sqrtsqi 0 N A N B N A N B 2 = N A N B
125 123 124 ax-mp N A N B 2 = N A N B
126 109 117 125 3brtr3g B P A = C N B 2 A P B C N B 2 N A N B