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 ⋅ ih y
cnlnadjlem.4 ⊢ B = ι w ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w
cnlnadjlem.5 ⊢ F = y ∈ ℋ ⟼ B
Assertion cnlnadjlem9 ⊢ ∃ t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 ⊢ T ∈ LinOp
2 cnlnadjlem.2 ⊢ T ∈ ContOp
3 cnlnadjlem.3 ⊢ G = g ∈ ℋ ⟼ T ⁡ g ⋅ ih y
4 cnlnadjlem.4 ⊢ B = ι w ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w
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 ⋅ ih z = x ⋅ ih F ⁡ z
11 10 ancoms ⊢ x ∈ ℋ ∧ z ∈ ℋ → T ⁡ x ⋅ ih z = x ⋅ ih F ⁡ z
12 11 rgen2 ⊢ ∀ x ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ih z = x ⋅ ih F ⁡ z
13 fveq1 ⊢ t = F → t ⁡ z = F ⁡ z
14 13 oveq2d ⊢ t = F → x ⋅ ih t ⁡ z = x ⋅ ih F ⁡ z
15 14 eqeq2d ⊢ t = F → T ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z ↔ T ⁡ x ⋅ ih z = x ⋅ ih F ⁡ z
16 15 2ralbidv ⊢ t = F → ∀ x ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z ↔ ∀ x ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ih z = x ⋅ ih F ⁡ z
17 16 rspcev ⊢ F ∈ LinOp ∩ ContOp ∧ ∀ x ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ih z = x ⋅ ih F ⁡ z → ∃ t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z
18 9 12 17 mp2an ⊢ ∃ t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ z ∈ ℋ T ⁡ x ⋅ ih z = x ⋅ ih t ⁡ z