# Metamath Proof Explorer

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$