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∈Bnormℎ⁡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∈Bnormℎ⁡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∈Bnormℎ⁡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∈Bnormℎ⁡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∈Bnormℎ⁡y+normℎ⁡z≤x⁢normℎ⁡y+ℎz→w=0ℎ
61 60 impancom ⊢x∈ℝ∧∀y∈A∀z∈Bnormℎ⁡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∈Bnormℎ⁡y+normℎ⁡z≤x⁢normℎ⁡y+ℎz→w∈A∩B→w∈0ℋ
64 63 ssrdv ⊢x∈ℝ∧∀y∈A∀z∈Bnormℎ⁡y+normℎ⁡z≤x⁢normℎ⁡y+ℎz→A∩B⊆0ℋ
65 64 ex ⊢x∈ℝ→∀y∈A∀z∈Bnormℎ⁡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 imbitrdi ⊢x∈ℝ→∀y∈A∀z∈Bnormℎ⁡y+normℎ⁡z≤x⁢normℎ⁡y+ℎz→A∩B=0ℋ
69 68 adantld ⊢x∈ℝ→0<x∧∀y∈A∀z∈Bnormℎ⁡y+normℎ⁡z≤x⁢normℎ⁡y+ℎz→A∩B=0ℋ
70 69 rexlimiv ⊢∃x∈ℝ0<x∧∀y∈A∀z∈Bnormℎ⁡y+normℎ⁡z≤x⁢normℎ⁡y+ℎz→A∩B=0ℋ