Metamath Proof Explorer

Theorem cnlnadjlem3

Description: Lemma for cnlnadji . By riesz4 , B is the unique vector such that ( Tv ) .ih y ) = ( v .ih w ) for all v . (Contributed by NM, 17-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
Assertion cnlnadjlem3 ⊢ y ∈ ℋ → B ∈ ℋ

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 1 2 3 cnlnadjlem2 ⊢ y ∈ ℋ → G ∈ LinFn ∧ G ∈ ContFn
6 elin ⊢ G ∈ LinFn ∩ ContFn ↔ G ∈ LinFn ∧ G ∈ ContFn
7 5 6 sylibr ⊢ y ∈ ℋ → G ∈ LinFn ∩ ContFn
8 riesz4 ⊢ G ∈ LinFn ∩ ContFn → ∃! w ∈ ℋ ∀ v ∈ ℋ G ⁡ v = v ⋅ ih w
9 7 8 syl ⊢ y ∈ ℋ → ∃! w ∈ ℋ ∀ v ∈ ℋ G ⁡ v = v ⋅ ih w
10 1 2 3 cnlnadjlem1 ⊢ v ∈ ℋ → G ⁡ v = T ⁡ v ⋅ ih y
11 10 eqeq1d ⊢ v ∈ ℋ → G ⁡ v = v ⋅ ih w ↔ T ⁡ v ⋅ ih y = v ⋅ ih w
12 11 ralbiia ⊢ ∀ v ∈ ℋ G ⁡ v = v ⋅ ih w ↔ ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w
13 12 reubii ⊢ ∃! w ∈ ℋ ∀ v ∈ ℋ G ⁡ v = v ⋅ ih w ↔ ∃! w ∈ ℋ ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w
14 9 13 sylib ⊢ y ∈ ℋ → ∃! w ∈ ℋ ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w
15 riotacl ⊢ ∃! w ∈ ℋ ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w → ι w ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w ∈ ℋ
16 14 15 syl ⊢ y ∈ ℋ → ι w ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w ∈ ℋ
17 4 16 eqeltrid ⊢ y ∈ ℋ → B ∈ ℋ