Metamath Proof Explorer

Theorem cdj3i

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

Ref Expression
Hypotheses cdj3.1 ⊢A∈Sℋ
cdj3.2 ⊢B∈Sℋ
cdj3.3 ⊢S=x∈A+ℋB⟼ιz∈A|∃w∈Bx=z+ℎw
cdj3.4 ⊢T=x∈A+ℋB⟼ιw∈B|∃z∈Ax=z+ℎw
cdj3.5 ⊢φ↔∃v∈ℝ0<v∧∀u∈A+ℋBnormℎ⁡S⁡u≤v⁢normℎ⁡u
cdj3.6 ⊢ψ↔∃v∈ℝ0<v∧∀u∈A+ℋBnormℎ⁡T⁡u≤v⁢normℎ⁡u
Assertion cdj3i ⊢∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔A∩B=0ℋ∧φ∧ψ

Proof

Step Hyp Ref Expression
1 cdj3.1 ⊢A∈Sℋ
2 cdj3.2 ⊢B∈Sℋ
3 cdj3.3 ⊢S=x∈A+ℋB⟼ιz∈A|∃w∈Bx=z+ℎw
4 cdj3.4 ⊢T=x∈A+ℋB⟼ιw∈B|∃z∈Ax=z+ℎw
5 cdj3.5 ⊢φ↔∃v∈ℝ0<v∧∀u∈A+ℋBnormℎ⁡S⁡u≤v⁢normℎ⁡u
6 cdj3.6 ⊢ψ↔∃v∈ℝ0<v∧∀u∈A+ℋBnormℎ⁡T⁡u≤v⁢normℎ⁡u
7 1 2 cdj3lem1 ⊢∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy→A∩B=0ℋ
8 1 2 3 cdj3lem2b ⊢∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy→∃v∈ℝ0<v∧∀u∈A+ℋBnormℎ⁡S⁡u≤v⁢normℎ⁡u
9 8 5 sylibr ⊢∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy→φ
10 1 2 4 cdj3lem3b ⊢∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy→∃v∈ℝ0<v∧∀u∈A+ℋBnormℎ⁡T⁡u≤v⁢normℎ⁡u
11 10 6 sylibr ⊢∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy→ψ
12 7 9 11 3jca ⊢∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy→A∩B=0ℋ∧φ∧ψ
13 breq2 ⊢v=f→0<v↔0<f
14 oveq1 ⊢v=f→v⁢normℎ⁡u=f⁢normℎ⁡u
15 14 breq2d ⊢v=f→normℎ⁡S⁡u≤v⁢normℎ⁡u↔normℎ⁡S⁡u≤f⁢normℎ⁡u
16 15 ralbidv ⊢v=f→∀u∈A+ℋBnormℎ⁡S⁡u≤v⁢normℎ⁡u↔∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u
17 13 16 anbi12d ⊢v=f→0<v∧∀u∈A+ℋBnormℎ⁡S⁡u≤v⁢normℎ⁡u↔0<f∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u
18 17 cbvrexvw ⊢∃v∈ℝ0<v∧∀u∈A+ℋBnormℎ⁡S⁡u≤v⁢normℎ⁡u↔∃f∈ℝ0<f∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u
19 5 18 bitri ⊢φ↔∃f∈ℝ0<f∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u
20 breq2 ⊢v=g→0<v↔0<g
21 oveq1 ⊢v=g→v⁢normℎ⁡u=g⁢normℎ⁡u
22 21 breq2d ⊢v=g→normℎ⁡T⁡u≤v⁢normℎ⁡u↔normℎ⁡T⁡u≤g⁢normℎ⁡u
23 22 ralbidv ⊢v=g→∀u∈A+ℋBnormℎ⁡T⁡u≤v⁢normℎ⁡u↔∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u
24 20 23 anbi12d ⊢v=g→0<v∧∀u∈A+ℋBnormℎ⁡T⁡u≤v⁢normℎ⁡u↔0<g∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u
25 24 cbvrexvw ⊢∃v∈ℝ0<v∧∀u∈A+ℋBnormℎ⁡T⁡u≤v⁢normℎ⁡u↔∃g∈ℝ0<g∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u
26 6 25 bitri ⊢ψ↔∃g∈ℝ0<g∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u
27 19 26 anbi12i ⊢φ∧ψ↔∃f∈ℝ0<f∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧∃g∈ℝ0<g∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u
28 reeanv ⊢∃f∈ℝ∃g∈ℝ0<f∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧0<g∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u↔∃f∈ℝ0<f∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧∃g∈ℝ0<g∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u
29 27 28 bitr4i ⊢φ∧ψ↔∃f∈ℝ∃g∈ℝ0<f∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧0<g∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u
30 an4 ⊢0<f∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧0<g∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u↔0<f∧0<g∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u
31 addgt0 ⊢f∈ℝ∧g∈ℝ∧0<f∧0<g→0<f+g
32 31 ex ⊢f∈ℝ∧g∈ℝ→0<f∧0<g→0<f+g
33 32 adantl ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ→0<f∧0<g→0<f+g
34 1 2 shsvai ⊢t∈A∧h∈B→t+ℎh∈A+ℋB
35 2fveq3 ⊢u=t+ℎh→normℎ⁡S⁡u=normℎ⁡S⁡t+ℎh
36 fveq2 ⊢u=t+ℎh→normℎ⁡u=normℎ⁡t+ℎh
37 36 oveq2d ⊢u=t+ℎh→f⁢normℎ⁡u=f⁢normℎ⁡t+ℎh
38 35 37 breq12d ⊢u=t+ℎh→normℎ⁡S⁡u≤f⁢normℎ⁡u↔normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh
39 38 rspcv ⊢t+ℎh∈A+ℋB→∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u→normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh
40 2fveq3 ⊢u=t+ℎh→normℎ⁡T⁡u=normℎ⁡T⁡t+ℎh
41 36 oveq2d ⊢u=t+ℎh→g⁢normℎ⁡u=g⁢normℎ⁡t+ℎh
42 40 41 breq12d ⊢u=t+ℎh→normℎ⁡T⁡u≤g⁢normℎ⁡u↔normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh
43 42 rspcv ⊢t+ℎh∈A+ℋB→∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u→normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh
44 39 43 anim12d ⊢t+ℎh∈A+ℋB→∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u→normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh∧normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh
45 34 44 syl ⊢t∈A∧h∈B→∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u→normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh∧normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh
46 45 adantl ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ∧t∈A∧h∈B→∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u→normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh∧normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh
47 1 sheli ⊢t∈A→t∈ℋ
48 normcl ⊢t∈ℋ→normℎ⁡t∈ℝ
49 47 48 syl ⊢t∈A→normℎ⁡t∈ℝ
50 2 sheli ⊢h∈B→h∈ℋ
51 normcl ⊢h∈ℋ→normℎ⁡h∈ℝ
52 50 51 syl ⊢h∈B→normℎ⁡h∈ℝ
53 49 52 anim12i ⊢t∈A∧h∈B→normℎ⁡t∈ℝ∧normℎ⁡h∈ℝ
54 53 adantl ⊢f∈ℝ∧g∈ℝ∧t∈A∧h∈B→normℎ⁡t∈ℝ∧normℎ⁡h∈ℝ
55 hvaddcl ⊢t∈ℋ∧h∈ℋ→t+ℎh∈ℋ
56 47 50 55 syl2an ⊢t∈A∧h∈B→t+ℎh∈ℋ
57 normcl ⊢t+ℎh∈ℋ→normℎ⁡t+ℎh∈ℝ
58 56 57 syl ⊢t∈A∧h∈B→normℎ⁡t+ℎh∈ℝ
59 remulcl ⊢f∈ℝ∧normℎ⁡t+ℎh∈ℝ→f⁢normℎ⁡t+ℎh∈ℝ
60 58 59 sylan2 ⊢f∈ℝ∧t∈A∧h∈B→f⁢normℎ⁡t+ℎh∈ℝ
61 60 adantlr ⊢f∈ℝ∧g∈ℝ∧t∈A∧h∈B→f⁢normℎ⁡t+ℎh∈ℝ
62 remulcl ⊢g∈ℝ∧normℎ⁡t+ℎh∈ℝ→g⁢normℎ⁡t+ℎh∈ℝ
63 58 62 sylan2 ⊢g∈ℝ∧t∈A∧h∈B→g⁢normℎ⁡t+ℎh∈ℝ
64 63 adantll ⊢f∈ℝ∧g∈ℝ∧t∈A∧h∈B→g⁢normℎ⁡t+ℎh∈ℝ
65 le2add ⊢normℎ⁡t∈ℝ∧normℎ⁡h∈ℝ∧f⁢normℎ⁡t+ℎh∈ℝ∧g⁢normℎ⁡t+ℎh∈ℝ→normℎ⁡t≤f⁢normℎ⁡t+ℎh∧normℎ⁡h≤g⁢normℎ⁡t+ℎh→normℎ⁡t+normℎ⁡h≤f⁢normℎ⁡t+ℎh+g⁢normℎ⁡t+ℎh
66 54 61 64 65 syl12anc ⊢f∈ℝ∧g∈ℝ∧t∈A∧h∈B→normℎ⁡t≤f⁢normℎ⁡t+ℎh∧normℎ⁡h≤g⁢normℎ⁡t+ℎh→normℎ⁡t+normℎ⁡h≤f⁢normℎ⁡t+ℎh+g⁢normℎ⁡t+ℎh
67 66 adantll ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ∧t∈A∧h∈B→normℎ⁡t≤f⁢normℎ⁡t+ℎh∧normℎ⁡h≤g⁢normℎ⁡t+ℎh→normℎ⁡t+normℎ⁡h≤f⁢normℎ⁡t+ℎh+g⁢normℎ⁡t+ℎh
68 1 2 3 cdj3lem2 ⊢t∈A∧h∈B∧A∩B=0ℋ→S⁡t+ℎh=t
69 68 fveq2d ⊢t∈A∧h∈B∧A∩B=0ℋ→normℎ⁡S⁡t+ℎh=normℎ⁡t
70 69 breq1d ⊢t∈A∧h∈B∧A∩B=0ℋ→normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh↔normℎ⁡t≤f⁢normℎ⁡t+ℎh
71 1 2 4 cdj3lem3 ⊢t∈A∧h∈B∧A∩B=0ℋ→T⁡t+ℎh=h
72 71 fveq2d ⊢t∈A∧h∈B∧A∩B=0ℋ→normℎ⁡T⁡t+ℎh=normℎ⁡h
73 72 breq1d ⊢t∈A∧h∈B∧A∩B=0ℋ→normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh↔normℎ⁡h≤g⁢normℎ⁡t+ℎh
74 70 73 anbi12d ⊢t∈A∧h∈B∧A∩B=0ℋ→normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh∧normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh↔normℎ⁡t≤f⁢normℎ⁡t+ℎh∧normℎ⁡h≤g⁢normℎ⁡t+ℎh
75 74 3expa ⊢t∈A∧h∈B∧A∩B=0ℋ→normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh∧normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh↔normℎ⁡t≤f⁢normℎ⁡t+ℎh∧normℎ⁡h≤g⁢normℎ⁡t+ℎh
76 75 ancoms ⊢A∩B=0ℋ∧t∈A∧h∈B→normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh∧normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh↔normℎ⁡t≤f⁢normℎ⁡t+ℎh∧normℎ⁡h≤g⁢normℎ⁡t+ℎh
77 76 adantlr ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ∧t∈A∧h∈B→normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh∧normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh↔normℎ⁡t≤f⁢normℎ⁡t+ℎh∧normℎ⁡h≤g⁢normℎ⁡t+ℎh
78 recn ⊢f∈ℝ→f∈ℂ
79 recn ⊢g∈ℝ→g∈ℂ
80 58 recnd ⊢t∈A∧h∈B→normℎ⁡t+ℎh∈ℂ
81 adddir ⊢f∈ℂ∧g∈ℂ∧normℎ⁡t+ℎh∈ℂ→f+g⁢normℎ⁡t+ℎh=f⁢normℎ⁡t+ℎh+g⁢normℎ⁡t+ℎh
82 78 79 80 81 syl3an ⊢f∈ℝ∧g∈ℝ∧t∈A∧h∈B→f+g⁢normℎ⁡t+ℎh=f⁢normℎ⁡t+ℎh+g⁢normℎ⁡t+ℎh
83 82 3expa ⊢f∈ℝ∧g∈ℝ∧t∈A∧h∈B→f+g⁢normℎ⁡t+ℎh=f⁢normℎ⁡t+ℎh+g⁢normℎ⁡t+ℎh
84 83 breq2d ⊢f∈ℝ∧g∈ℝ∧t∈A∧h∈B→normℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh↔normℎ⁡t+normℎ⁡h≤f⁢normℎ⁡t+ℎh+g⁢normℎ⁡t+ℎh
85 84 adantll ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ∧t∈A∧h∈B→normℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh↔normℎ⁡t+normℎ⁡h≤f⁢normℎ⁡t+ℎh+g⁢normℎ⁡t+ℎh
86 67 77 85 3imtr4d ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ∧t∈A∧h∈B→normℎ⁡S⁡t+ℎh≤f⁢normℎ⁡t+ℎh∧normℎ⁡T⁡t+ℎh≤g⁢normℎ⁡t+ℎh→normℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh
87 46 86 syld ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ∧t∈A∧h∈B→∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u→normℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh
88 87 ralrimdvva ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ→∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u→∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh
89 readdcl ⊢f∈ℝ∧g∈ℝ→f+g∈ℝ
90 breq2 ⊢v=f+g→0<v↔0<f+g
91 fveq2 ⊢x=t→normℎ⁡x=normℎ⁡t
92 91 oveq1d ⊢x=t→normℎ⁡x+normℎ⁡y=normℎ⁡t+normℎ⁡y
93 fvoveq1 ⊢x=t→normℎ⁡x+ℎy=normℎ⁡t+ℎy
94 93 oveq2d ⊢x=t→v⁢normℎ⁡x+ℎy=v⁢normℎ⁡t+ℎy
95 92 94 breq12d ⊢x=t→normℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔normℎ⁡t+normℎ⁡y≤v⁢normℎ⁡t+ℎy
96 fveq2 ⊢y=h→normℎ⁡y=normℎ⁡h
97 96 oveq2d ⊢y=h→normℎ⁡t+normℎ⁡y=normℎ⁡t+normℎ⁡h
98 oveq2 ⊢y=h→t+ℎy=t+ℎh
99 98 fveq2d ⊢y=h→normℎ⁡t+ℎy=normℎ⁡t+ℎh
100 99 oveq2d ⊢y=h→v⁢normℎ⁡t+ℎy=v⁢normℎ⁡t+ℎh
101 97 100 breq12d ⊢y=h→normℎ⁡t+normℎ⁡y≤v⁢normℎ⁡t+ℎy↔normℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh
102 95 101 cbvral2vw ⊢∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh
103 oveq1 ⊢v=f+g→v⁢normℎ⁡t+ℎh=f+g⁢normℎ⁡t+ℎh
104 103 breq2d ⊢v=f+g→normℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh↔normℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh
105 104 2ralbidv ⊢v=f+g→∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh↔∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh
106 102 105 bitrid ⊢v=f+g→∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh
107 90 106 anbi12d ⊢v=f+g→0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔0<f+g∧∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh
108 107 rspcev ⊢f+g∈ℝ∧0<f+g∧∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh→∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
109 108 ex ⊢f+g∈ℝ→0<f+g∧∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh→∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
110 89 109 syl ⊢f∈ℝ∧g∈ℝ→0<f+g∧∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh→∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
111 110 adantl ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ→0<f+g∧∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤f+g⁢normℎ⁡t+ℎh→∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
112 33 88 111 syl2and ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ→0<f∧0<g∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u→∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
113 30 112 biimtrid ⊢A∩B=0ℋ∧f∈ℝ∧g∈ℝ→0<f∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧0<g∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u→∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
114 113 rexlimdvva ⊢A∩B=0ℋ→∃f∈ℝ∃g∈ℝ0<f∧∀u∈A+ℋBnormℎ⁡S⁡u≤f⁢normℎ⁡u∧0<g∧∀u∈A+ℋBnormℎ⁡T⁡u≤g⁢normℎ⁡u→∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
115 29 114 biimtrid ⊢A∩B=0ℋ→φ∧ψ→∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
116 115 3impib ⊢A∩B=0ℋ∧φ∧ψ→∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
117 12 116 impbii ⊢∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔A∩B=0ℋ∧φ∧ψ