Metamath Proof Explorer


Theorem cdj3lem1

Description: A property of " A and B are completely disjoint subspaces." Part of Lemma 5 of Holland p. 1520. (Contributed by NM, 23-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdj1.1 A S
cdj1.2 B S
Assertion cdj3lem1 x 0 < x y A z B norm y + norm z x norm y + z A B = 0

Proof

Step Hyp Ref Expression
1 cdj1.1 A S
2 cdj1.2 B S
3 elin w A B w A w B
4 neg1cn 1
5 shmulcl B S 1 w B -1 w B
6 2 4 5 mp3an12 w B -1 w B
7 6 anim2i w A w B w A -1 w B
8 3 7 sylbi w A B w A -1 w B
9 fveq2 y = w norm y = norm w
10 9 oveq1d y = w norm y + norm z = norm w + norm z
11 fvoveq1 y = w norm y + z = norm w + z
12 11 oveq2d y = w x norm y + z = x norm w + z
13 10 12 breq12d y = w norm y + norm z x norm y + z norm w + norm z x norm w + z
14 fveq2 z = -1 w norm z = norm -1 w
15 14 oveq2d z = -1 w norm w + norm z = norm w + norm -1 w
16 oveq2 z = -1 w w + z = w + -1 w
17 16 fveq2d z = -1 w norm w + z = norm w + -1 w
18 17 oveq2d z = -1 w x norm w + z = x norm w + -1 w
19 15 18 breq12d z = -1 w norm w + norm z x norm w + z norm w + norm -1 w x norm w + -1 w
20 13 19 rspc2v w A -1 w B y A z B norm y + norm z x norm y + z norm w + norm -1 w x norm w + -1 w
21 8 20 syl w A B y A z B norm y + norm z x norm y + z norm w + norm -1 w x norm w + -1 w
22 21 adantl x w A B y A z B norm y + norm z x norm y + z norm w + norm -1 w x norm w + -1 w
23 1 2 shincli A B S
24 23 sheli w A B w
25 normneg w norm -1 w = norm w
26 25 oveq2d w norm w + norm -1 w = norm w + norm w
27 normcl w norm w
28 27 recnd w norm w
29 28 2timesd w 2 norm w = norm w + norm w
30 26 29 eqtr4d w norm w + norm -1 w = 2 norm w
31 30 adantl x w norm w + norm -1 w = 2 norm w
32 hvnegid w w + -1 w = 0
33 32 fveq2d w norm w + -1 w = norm 0
34 norm0 norm 0 = 0
35 33 34 eqtrdi w norm w + -1 w = 0
36 35 oveq2d w x norm w + -1 w = x 0
37 recn x x
38 37 mul01d x x 0 = 0
39 36 38 sylan9eqr x w x norm w + -1 w = 0
40 2t0e0 2 0 = 0
41 39 40 eqtr4di x w x norm w + -1 w = 2 0
42 31 41 breq12d x w norm w + norm -1 w x norm w + -1 w 2 norm w 2 0
43 0re 0
44 letri3 norm w 0 norm w = 0 norm w 0 0 norm w
45 27 43 44 sylancl w norm w = 0 norm w 0 0 norm w
46 normge0 w 0 norm w
47 46 biantrud w norm w 0 norm w 0 0 norm w
48 2re 2
49 2pos 0 < 2
50 48 49 pm3.2i 2 0 < 2
51 lemul2 norm w 0 2 0 < 2 norm w 0 2 norm w 2 0
52 43 50 51 mp3an23 norm w norm w 0 2 norm w 2 0
53 27 52 syl w norm w 0 2 norm w 2 0
54 45 47 53 3bitr2rd w 2 norm w 2 0 norm w = 0
55 norm-i w norm w = 0 w = 0
56 54 55 bitrd w 2 norm w 2 0 w = 0
57 56 adantl x w 2 norm w 2 0 w = 0
58 42 57 bitrd x w norm w + norm -1 w x norm w + -1 w w = 0
59 24 58 sylan2 x w A B norm w + norm -1 w x norm w + -1 w w = 0
60 22 59 sylibd x w A B y A z B norm y + norm z x norm y + z w = 0
61 60 impancom x y A z B norm y + norm z x norm y + z w A B w = 0
62 elch0 w 0 w = 0
63 61 62 syl6ibr x y A z B norm y + norm z x norm y + z w A B w 0
64 63 ssrdv x y A z B norm y + norm z x norm y + z A B 0
65 64 ex x y A z B norm y + norm z x norm y + z A B 0
66 shle0 A B S A B 0 A B = 0
67 23 66 ax-mp A B 0 A B = 0
68 65 67 syl6ib x y A z B norm y + norm z x norm y + z A B = 0
69 68 adantld x 0 < x y A z B norm y + norm z x norm y + z A B = 0
70 69 rexlimiv x 0 < x y A z B norm y + norm z x norm y + z A B = 0