Metamath Proof Explorer

Theorem cdj3lem3b

Description: Lemma for cdj3i . The second-component function T is bounded if the subspaces are completely disjoint. (Contributed by NM, 31-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdj3lem2.1 ⊢A∈Sℋ
cdj3lem2.2 ⊢B∈Sℋ
cdj3lem3.3 ⊢T=x∈A+ℋB⟼ιw∈B|∃z∈Ax=z+ℎw
Assertion 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

Proof

Step Hyp Ref Expression
1 cdj3lem2.1 ⊢A∈Sℋ
2 cdj3lem2.2 ⊢B∈Sℋ
3 cdj3lem3.3 ⊢T=x∈A+ℋB⟼ιw∈B|∃z∈Ax=z+ℎw
4 2 1 shscomi ⊢B+ℋA=A+ℋB
5 2 sheli ⊢w∈B→w∈ℋ
6 1 sheli ⊢z∈A→z∈ℋ
7 ax-hvcom ⊢w∈ℋ∧z∈ℋ→w+ℎz=z+ℎw
8 5 6 7 syl2an ⊢w∈B∧z∈A→w+ℎz=z+ℎw
9 8 eqeq2d ⊢w∈B∧z∈A→x=w+ℎz↔x=z+ℎw
10 9 rexbidva ⊢w∈B→∃z∈Ax=w+ℎz↔∃z∈Ax=z+ℎw
11 10 riotabiia ⊢ιw∈B|∃z∈Ax=w+ℎz=ιw∈B|∃z∈Ax=z+ℎw
12 4 11 mpteq12i ⊢x∈B+ℋA⟼ιw∈B|∃z∈Ax=w+ℎz=x∈A+ℋB⟼ιw∈B|∃z∈Ax=z+ℎw
13 3 12 eqtr4i ⊢T=x∈B+ℋA⟼ιw∈B|∃z∈Ax=w+ℎz
14 2 1 13 cdj3lem2b ⊢∃v∈ℝ0<v∧∀x∈B∀y∈Anormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy→∃v∈ℝ0<v∧∀u∈B+ℋAnormℎ⁡T⁡u≤v⁢normℎ⁡u
15 fveq2 ⊢x=t→normℎ⁡x=normℎ⁡t
16 15 oveq1d ⊢x=t→normℎ⁡x+normℎ⁡y=normℎ⁡t+normℎ⁡y
17 fvoveq1 ⊢x=t→normℎ⁡x+ℎy=normℎ⁡t+ℎy
18 17 oveq2d ⊢x=t→v⁢normℎ⁡x+ℎy=v⁢normℎ⁡t+ℎy
19 16 18 breq12d ⊢x=t→normℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔normℎ⁡t+normℎ⁡y≤v⁢normℎ⁡t+ℎy
20 fveq2 ⊢y=h→normℎ⁡y=normℎ⁡h
21 20 oveq2d ⊢y=h→normℎ⁡t+normℎ⁡y=normℎ⁡t+normℎ⁡h
22 oveq2 ⊢y=h→t+ℎy=t+ℎh
23 22 fveq2d ⊢y=h→normℎ⁡t+ℎy=normℎ⁡t+ℎh
24 23 oveq2d ⊢y=h→v⁢normℎ⁡t+ℎy=v⁢normℎ⁡t+ℎh
25 21 24 breq12d ⊢y=h→normℎ⁡t+normℎ⁡y≤v⁢normℎ⁡t+ℎy↔normℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh
26 19 25 cbvral2vw ⊢∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh
27 ralcom ⊢∀t∈A∀h∈Bnormℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh↔∀h∈B∀t∈Anormℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh
28 2 sheli ⊢x∈B→x∈ℋ
29 normcl ⊢x∈ℋ→normℎ⁡x∈ℝ
30 28 29 syl ⊢x∈B→normℎ⁡x∈ℝ
31 30 recnd ⊢x∈B→normℎ⁡x∈ℂ
32 1 sheli ⊢y∈A→y∈ℋ
33 normcl ⊢y∈ℋ→normℎ⁡y∈ℝ
34 32 33 syl ⊢y∈A→normℎ⁡y∈ℝ
35 34 recnd ⊢y∈A→normℎ⁡y∈ℂ
36 addcom ⊢normℎ⁡x∈ℂ∧normℎ⁡y∈ℂ→normℎ⁡x+normℎ⁡y=normℎ⁡y+normℎ⁡x
37 31 35 36 syl2an ⊢x∈B∧y∈A→normℎ⁡x+normℎ⁡y=normℎ⁡y+normℎ⁡x
38 ax-hvcom ⊢x∈ℋ∧y∈ℋ→x+ℎy=y+ℎx
39 28 32 38 syl2an ⊢x∈B∧y∈A→x+ℎy=y+ℎx
40 39 fveq2d ⊢x∈B∧y∈A→normℎ⁡x+ℎy=normℎ⁡y+ℎx
41 40 oveq2d ⊢x∈B∧y∈A→v⁢normℎ⁡x+ℎy=v⁢normℎ⁡y+ℎx
42 37 41 breq12d ⊢x∈B∧y∈A→normℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔normℎ⁡y+normℎ⁡x≤v⁢normℎ⁡y+ℎx
43 42 ralbidva ⊢x∈B→∀y∈Anormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔∀y∈Anormℎ⁡y+normℎ⁡x≤v⁢normℎ⁡y+ℎx
44 43 ralbiia ⊢∀x∈B∀y∈Anormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔∀x∈B∀y∈Anormℎ⁡y+normℎ⁡x≤v⁢normℎ⁡y+ℎx
45 fveq2 ⊢x=h→normℎ⁡x=normℎ⁡h
46 45 oveq2d ⊢x=h→normℎ⁡y+normℎ⁡x=normℎ⁡y+normℎ⁡h
47 oveq2 ⊢x=h→y+ℎx=y+ℎh
48 47 fveq2d ⊢x=h→normℎ⁡y+ℎx=normℎ⁡y+ℎh
49 48 oveq2d ⊢x=h→v⁢normℎ⁡y+ℎx=v⁢normℎ⁡y+ℎh
50 46 49 breq12d ⊢x=h→normℎ⁡y+normℎ⁡x≤v⁢normℎ⁡y+ℎx↔normℎ⁡y+normℎ⁡h≤v⁢normℎ⁡y+ℎh
51 fveq2 ⊢y=t→normℎ⁡y=normℎ⁡t
52 51 oveq1d ⊢y=t→normℎ⁡y+normℎ⁡h=normℎ⁡t+normℎ⁡h
53 fvoveq1 ⊢y=t→normℎ⁡y+ℎh=normℎ⁡t+ℎh
54 53 oveq2d ⊢y=t→v⁢normℎ⁡y+ℎh=v⁢normℎ⁡t+ℎh
55 52 54 breq12d ⊢y=t→normℎ⁡y+normℎ⁡h≤v⁢normℎ⁡y+ℎh↔normℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh
56 50 55 cbvral2vw ⊢∀x∈B∀y∈Anormℎ⁡y+normℎ⁡x≤v⁢normℎ⁡y+ℎx↔∀h∈B∀t∈Anormℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh
57 44 56 bitr2i ⊢∀h∈B∀t∈Anormℎ⁡t+normℎ⁡h≤v⁢normℎ⁡t+ℎh↔∀x∈B∀y∈Anormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
58 26 27 57 3bitri ⊢∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔∀x∈B∀y∈Anormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
59 58 anbi2i ⊢0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔0<v∧∀x∈B∀y∈Anormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
60 59 rexbii ⊢∃v∈ℝ0<v∧∀x∈A∀y∈Bnormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy↔∃v∈ℝ0<v∧∀x∈B∀y∈Anormℎ⁡x+normℎ⁡y≤v⁢normℎ⁡x+ℎy
61 1 2 shscomi ⊢A+ℋB=B+ℋA
62 61 raleqi ⊢∀u∈A+ℋBnormℎ⁡T⁡u≤v⁢normℎ⁡u↔∀u∈B+ℋAnormℎ⁡T⁡u≤v⁢normℎ⁡u
63 62 anbi2i ⊢0<v∧∀u∈A+ℋBnormℎ⁡T⁡u≤v⁢normℎ⁡u↔0<v∧∀u∈B+ℋAnormℎ⁡T⁡u≤v⁢normℎ⁡u
64 63 rexbii ⊢∃v∈ℝ0<v∧∀u∈A+ℋBnormℎ⁡T⁡u≤v⁢normℎ⁡u↔∃v∈ℝ0<v∧∀u∈B+ℋAnormℎ⁡T⁡u≤v⁢normℎ⁡u
65 14 60 64 3imtr4i ⊢∃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