Metamath Proof Explorer

Theorem cdj1i

Description: Two ways to express " A and B are completely disjoint subspaces." (1) => (2) in Lemma 5 of Holland p. 1520. (Contributed by NM, 21-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdj1.1 ⊢A∈Sℋ
cdj1.2 ⊢B∈Sℋ
Assertion cdj1i ⊢∃w∈ℝ0<w∧∀y∈A∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→∃x∈ℝ0<x∧∀y∈A∀z∈Bnormℎ⁡y=1→x≤normℎ⁡y-ℎz

Proof

Step Hyp Ref Expression
1 cdj1.1 ⊢A∈Sℋ
2 cdj1.2 ⊢B∈Sℋ
3 gt0ne0 ⊢w∈ℝ∧0<w→w≠0
4 rereccl ⊢w∈ℝ∧w≠0→1w∈ℝ
5 3 4 syldan ⊢w∈ℝ∧0<w→1w∈ℝ
6 5 adantrr ⊢w∈ℝ∧0<w∧∀y∈A∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→1w∈ℝ
7 recgt0 ⊢w∈ℝ∧0<w→0<1w
8 7 adantrr ⊢w∈ℝ∧0<w∧∀y∈A∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→0<1w
9 1red ⊢w∈ℝ∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1∈ℝ
10 1re ⊢1∈ℝ
11 neg1cn ⊢−1∈ℂ
12 2 sheli ⊢z∈B→z∈ℋ
13 hvmulcl ⊢−1∈ℂ∧z∈ℋ→-1⋅ℎz∈ℋ
14 11 12 13 sylancr ⊢z∈B→-1⋅ℎz∈ℋ
15 normcl ⊢-1⋅ℎz∈ℋ→normℎ⁡-1⋅ℎz∈ℝ
16 14 15 syl ⊢z∈B→normℎ⁡-1⋅ℎz∈ℝ
17 16 adantl ⊢w∈ℝ∧y∈A∧z∈B→normℎ⁡-1⋅ℎz∈ℝ
18 readdcl ⊢1∈ℝ∧normℎ⁡-1⋅ℎz∈ℝ→1+normℎ⁡-1⋅ℎz∈ℝ
19 10 17 18 sylancr ⊢w∈ℝ∧y∈A∧z∈B→1+normℎ⁡-1⋅ℎz∈ℝ
20 19 adantr ⊢w∈ℝ∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1+normℎ⁡-1⋅ℎz∈ℝ
21 1 sheli ⊢y∈A→y∈ℋ
22 hvsubcl ⊢y∈ℋ∧z∈ℋ→y-ℎz∈ℋ
23 21 12 22 syl2an ⊢y∈A∧z∈B→y-ℎz∈ℋ
24 normcl ⊢y-ℎz∈ℋ→normℎ⁡y-ℎz∈ℝ
25 23 24 syl ⊢y∈A∧z∈B→normℎ⁡y-ℎz∈ℝ
26 remulcl ⊢w∈ℝ∧normℎ⁡y-ℎz∈ℝ→w⁢normℎ⁡y-ℎz∈ℝ
27 25 26 sylan2 ⊢w∈ℝ∧y∈A∧z∈B→w⁢normℎ⁡y-ℎz∈ℝ
28 27 anassrs ⊢w∈ℝ∧y∈A∧z∈B→w⁢normℎ⁡y-ℎz∈ℝ
29 28 adantr ⊢w∈ℝ∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→w⁢normℎ⁡y-ℎz∈ℝ
30 normge0 ⊢-1⋅ℎz∈ℋ→0≤normℎ⁡-1⋅ℎz
31 14 30 syl ⊢z∈B→0≤normℎ⁡-1⋅ℎz
32 addge01 ⊢1∈ℝ∧normℎ⁡-1⋅ℎz∈ℝ→0≤normℎ⁡-1⋅ℎz↔1≤1+normℎ⁡-1⋅ℎz
33 10 32 mpan ⊢normℎ⁡-1⋅ℎz∈ℝ→0≤normℎ⁡-1⋅ℎz↔1≤1+normℎ⁡-1⋅ℎz
34 33 biimpa ⊢normℎ⁡-1⋅ℎz∈ℝ∧0≤normℎ⁡-1⋅ℎz→1≤1+normℎ⁡-1⋅ℎz
35 16 31 34 syl2anc ⊢z∈B→1≤1+normℎ⁡-1⋅ℎz
36 35 ad2antlr ⊢w∈ℝ∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1≤1+normℎ⁡-1⋅ℎz
37 shmulcl ⊢B∈Sℋ∧−1∈ℂ∧z∈B→-1⋅ℎz∈B
38 2 11 37 mp3an12 ⊢z∈B→-1⋅ℎz∈B
39 fveq2 ⊢v=-1⋅ℎz→normℎ⁡v=normℎ⁡-1⋅ℎz
40 39 oveq2d ⊢v=-1⋅ℎz→normℎ⁡y+normℎ⁡v=normℎ⁡y+normℎ⁡-1⋅ℎz
41 oveq2 ⊢v=-1⋅ℎz→y+ℎv=y+ℎ-1⋅ℎz
42 41 fveq2d ⊢v=-1⋅ℎz→normℎ⁡y+ℎv=normℎ⁡y+ℎ-1⋅ℎz
43 42 oveq2d ⊢v=-1⋅ℎz→w⁢normℎ⁡y+ℎv=w⁢normℎ⁡y+ℎ-1⋅ℎz
44 40 43 breq12d ⊢v=-1⋅ℎz→normℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv↔normℎ⁡y+normℎ⁡-1⋅ℎz≤w⁢normℎ⁡y+ℎ-1⋅ℎz
45 44 rspcv ⊢-1⋅ℎz∈B→∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→normℎ⁡y+normℎ⁡-1⋅ℎz≤w⁢normℎ⁡y+ℎ-1⋅ℎz
46 38 45 syl ⊢z∈B→∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→normℎ⁡y+normℎ⁡-1⋅ℎz≤w⁢normℎ⁡y+ℎ-1⋅ℎz
47 46 imp ⊢z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→normℎ⁡y+normℎ⁡-1⋅ℎz≤w⁢normℎ⁡y+ℎ-1⋅ℎz
48 47 ad2ant2lr ⊢w∈ℝ∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→normℎ⁡y+normℎ⁡-1⋅ℎz≤w⁢normℎ⁡y+ℎ-1⋅ℎz
49 oveq1 ⊢1=normℎ⁡y→1+normℎ⁡-1⋅ℎz=normℎ⁡y+normℎ⁡-1⋅ℎz
50 49 eqcoms ⊢normℎ⁡y=1→1+normℎ⁡-1⋅ℎz=normℎ⁡y+normℎ⁡-1⋅ℎz
51 50 ad2antll ⊢w∈ℝ∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1+normℎ⁡-1⋅ℎz=normℎ⁡y+normℎ⁡-1⋅ℎz
52 hvsubval ⊢y∈ℋ∧z∈ℋ→y-ℎz=y+ℎ-1⋅ℎz
53 21 12 52 syl2an ⊢y∈A∧z∈B→y-ℎz=y+ℎ-1⋅ℎz
54 53 fveq2d ⊢y∈A∧z∈B→normℎ⁡y-ℎz=normℎ⁡y+ℎ-1⋅ℎz
55 54 oveq2d ⊢y∈A∧z∈B→w⁢normℎ⁡y-ℎz=w⁢normℎ⁡y+ℎ-1⋅ℎz
56 55 adantll ⊢w∈ℝ∧y∈A∧z∈B→w⁢normℎ⁡y-ℎz=w⁢normℎ⁡y+ℎ-1⋅ℎz
57 56 adantr ⊢w∈ℝ∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→w⁢normℎ⁡y-ℎz=w⁢normℎ⁡y+ℎ-1⋅ℎz
58 48 51 57 3brtr4d ⊢w∈ℝ∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1+normℎ⁡-1⋅ℎz≤w⁢normℎ⁡y-ℎz
59 9 20 29 36 58 letrd ⊢w∈ℝ∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1≤w⁢normℎ⁡y-ℎz
60 59 ex ⊢w∈ℝ∧y∈A∧z∈B→∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1≤w⁢normℎ⁡y-ℎz
61 60 adantllr ⊢w∈ℝ∧0<w∧y∈A∧z∈B→∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1≤w⁢normℎ⁡y-ℎz
62 simplll ⊢w∈ℝ∧0<w∧y∈A∧z∈B→w∈ℝ
63 23 adantll ⊢w∈ℝ∧0<w∧y∈A∧z∈B→y-ℎz∈ℋ
64 63 24 syl ⊢w∈ℝ∧0<w∧y∈A∧z∈B→normℎ⁡y-ℎz∈ℝ
65 62 64 26 syl2anc ⊢w∈ℝ∧0<w∧y∈A∧z∈B→w⁢normℎ⁡y-ℎz∈ℝ
66 simpllr ⊢w∈ℝ∧0<w∧y∈A∧z∈B→0<w
67 lediv1 ⊢1∈ℝ∧w⁢normℎ⁡y-ℎz∈ℝ∧w∈ℝ∧0<w→1≤w⁢normℎ⁡y-ℎz↔1w≤w⁢normℎ⁡y-ℎzw
68 10 67 mp3an1 ⊢w⁢normℎ⁡y-ℎz∈ℝ∧w∈ℝ∧0<w→1≤w⁢normℎ⁡y-ℎz↔1w≤w⁢normℎ⁡y-ℎzw
69 65 62 66 68 syl12anc ⊢w∈ℝ∧0<w∧y∈A∧z∈B→1≤w⁢normℎ⁡y-ℎz↔1w≤w⁢normℎ⁡y-ℎzw
70 61 69 sylibd ⊢w∈ℝ∧0<w∧y∈A∧z∈B→∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1w≤w⁢normℎ⁡y-ℎzw
71 70 imp ⊢w∈ℝ∧0<w∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1w≤w⁢normℎ⁡y-ℎzw
72 25 recnd ⊢y∈A∧z∈B→normℎ⁡y-ℎz∈ℂ
73 72 adantll ⊢w∈ℝ∧0<w∧y∈A∧z∈B→normℎ⁡y-ℎz∈ℂ
74 recn ⊢w∈ℝ→w∈ℂ
75 74 ad3antrrr ⊢w∈ℝ∧0<w∧y∈A∧z∈B→w∈ℂ
76 3 ad2antrr ⊢w∈ℝ∧0<w∧y∈A∧z∈B→w≠0
77 73 75 76 divcan3d ⊢w∈ℝ∧0<w∧y∈A∧z∈B→w⁢normℎ⁡y-ℎzw=normℎ⁡y-ℎz
78 77 adantr ⊢w∈ℝ∧0<w∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→w⁢normℎ⁡y-ℎzw=normℎ⁡y-ℎz
79 71 78 breqtrd ⊢w∈ℝ∧0<w∧y∈A∧z∈B∧∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv∧normℎ⁡y=1→1w≤normℎ⁡y-ℎz
80 79 exp43 ⊢w∈ℝ∧0<w∧y∈A→z∈B→∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→normℎ⁡y=1→1w≤normℎ⁡y-ℎz
81 80 com23 ⊢w∈ℝ∧0<w∧y∈A→∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→z∈B→normℎ⁡y=1→1w≤normℎ⁡y-ℎz
82 81 ralrimdv ⊢w∈ℝ∧0<w∧y∈A→∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→∀z∈Bnormℎ⁡y=1→1w≤normℎ⁡y-ℎz
83 82 ralimdva ⊢w∈ℝ∧0<w→∀y∈A∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→∀y∈A∀z∈Bnormℎ⁡y=1→1w≤normℎ⁡y-ℎz
84 83 impr ⊢w∈ℝ∧0<w∧∀y∈A∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→∀y∈A∀z∈Bnormℎ⁡y=1→1w≤normℎ⁡y-ℎz
85 6 8 84 jca32 ⊢w∈ℝ∧0<w∧∀y∈A∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→1w∈ℝ∧0<1w∧∀y∈A∀z∈Bnormℎ⁡y=1→1w≤normℎ⁡y-ℎz
86 85 ex ⊢w∈ℝ→0<w∧∀y∈A∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→1w∈ℝ∧0<1w∧∀y∈A∀z∈Bnormℎ⁡y=1→1w≤normℎ⁡y-ℎz
87 breq2 ⊢x=1w→0<x↔0<1w
88 breq1 ⊢x=1w→x≤normℎ⁡y-ℎz↔1w≤normℎ⁡y-ℎz
89 88 imbi2d ⊢x=1w→normℎ⁡y=1→x≤normℎ⁡y-ℎz↔normℎ⁡y=1→1w≤normℎ⁡y-ℎz
90 89 2ralbidv ⊢x=1w→∀y∈A∀z∈Bnormℎ⁡y=1→x≤normℎ⁡y-ℎz↔∀y∈A∀z∈Bnormℎ⁡y=1→1w≤normℎ⁡y-ℎz
91 87 90 anbi12d ⊢x=1w→0<x∧∀y∈A∀z∈Bnormℎ⁡y=1→x≤normℎ⁡y-ℎz↔0<1w∧∀y∈A∀z∈Bnormℎ⁡y=1→1w≤normℎ⁡y-ℎz
92 91 rspcev ⊢1w∈ℝ∧0<1w∧∀y∈A∀z∈Bnormℎ⁡y=1→1w≤normℎ⁡y-ℎz→∃x∈ℝ0<x∧∀y∈A∀z∈Bnormℎ⁡y=1→x≤normℎ⁡y-ℎz
93 86 92 syl6 ⊢w∈ℝ→0<w∧∀y∈A∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→∃x∈ℝ0<x∧∀y∈A∀z∈Bnormℎ⁡y=1→x≤normℎ⁡y-ℎz
94 93 rexlimiv ⊢∃w∈ℝ0<w∧∀y∈A∀v∈Bnormℎ⁡y+normℎ⁡v≤w⁢normℎ⁡y+ℎv→∃x∈ℝ0<x∧∀y∈A∀z∈Bnormℎ⁡y=1→x≤normℎ⁡y-ℎz