Metamath Proof Explorer

Theorem cnlnadjlem9

Description: Lemma for cnlnadji . F provides an example showing the existence of a continuous linear adjoint. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 ⊢T∈LinOp
cnlnadjlem.2 ⊢T∈ContOp
cnlnadjlem.3 ⊢G=g∈ℋ⟼T⁡g⋅ihy
cnlnadjlem.4 ⊢B=ιw∈ℋ|∀v∈ℋT⁡v⋅ihy=v⋅ihw
cnlnadjlem.5 ⊢F=y∈ℋ⟼B
Assertion cnlnadjlem9 ⊢∃t∈LinOp∩ContOp∀x∈ℋ∀z∈ℋT⁡x⋅ihz=x⋅iht⁡z

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 ⊢T∈LinOp
2 cnlnadjlem.2 ⊢T∈ContOp
3 cnlnadjlem.3 ⊢G=g∈ℋ⟼T⁡g⋅ihy
4 cnlnadjlem.4 ⊢B=ιw∈ℋ|∀v∈ℋT⁡v⋅ihy=v⋅ihw
5 cnlnadjlem.5 ⊢F=y∈ℋ⟼B
6 1 2 3 4 5 cnlnadjlem6 ⊢F∈LinOp
7 1 2 3 4 5 cnlnadjlem8 ⊢F∈ContOp
8 elin ⊢F∈LinOp∩ContOp↔F∈LinOp∧F∈ContOp
9 6 7 8 mpbir2an ⊢F∈LinOp∩ContOp
10 1 2 3 4 5 cnlnadjlem5 ⊢z∈ℋ∧x∈ℋ→T⁡x⋅ihz=x⋅ihF⁡z
11 10 ancoms ⊢x∈ℋ∧z∈ℋ→T⁡x⋅ihz=x⋅ihF⁡z
12 11 rgen2 ⊢∀x∈ℋ∀z∈ℋT⁡x⋅ihz=x⋅ihF⁡z
13 fveq1 ⊢t=F→t⁡z=F⁡z
14 13 oveq2d ⊢t=F→x⋅iht⁡z=x⋅ihF⁡z
15 14 eqeq2d ⊢t=F→T⁡x⋅ihz=x⋅iht⁡z↔T⁡x⋅ihz=x⋅ihF⁡z
16 15 2ralbidv ⊢t=F→∀x∈ℋ∀z∈ℋT⁡x⋅ihz=x⋅iht⁡z↔∀x∈ℋ∀z∈ℋT⁡x⋅ihz=x⋅ihF⁡z
17 16 rspcev ⊢F∈LinOp∩ContOp∧∀x∈ℋ∀z∈ℋT⁡x⋅ihz=x⋅ihF⁡z→∃t∈LinOp∩ContOp∀x∈ℋ∀z∈ℋT⁡x⋅ihz=x⋅iht⁡z
18 9 12 17 mp2an ⊢∃t∈LinOp∩ContOp∀x∈ℋ∀z∈ℋT⁡x⋅ihz=x⋅iht⁡z