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⋅ihy
cnlnadjlem.4 ⊢B=ιw∈ℋ|∀v∈ℋT⁡v⋅ihy=v⋅ihw
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⋅ihy
4 cnlnadjlem.4 ⊢B=ιw∈ℋ|∀v∈ℋT⁡v⋅ihy=v⋅ihw
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⋅ihw
9 7 8 syl ⊢y∈ℋ→∃!w∈ℋ∀v∈ℋG⁡v=v⋅ihw
10 1 2 3 cnlnadjlem1 ⊢v∈ℋ→G⁡v=T⁡v⋅ihy
11 10 eqeq1d ⊢v∈ℋ→G⁡v=v⋅ihw↔T⁡v⋅ihy=v⋅ihw
12 11 ralbiia ⊢∀v∈ℋG⁡v=v⋅ihw↔∀v∈ℋT⁡v⋅ihy=v⋅ihw
13 12 reubii ⊢∃!w∈ℋ∀v∈ℋG⁡v=v⋅ihw↔∃!w∈ℋ∀v∈ℋT⁡v⋅ihy=v⋅ihw
14 9 13 sylib ⊢y∈ℋ→∃!w∈ℋ∀v∈ℋT⁡v⋅ihy=v⋅ihw
15 riotacl ⊢∃!w∈ℋ∀v∈ℋT⁡v⋅ihy=v⋅ihw→ιw∈ℋ|∀v∈ℋT⁡v⋅ihy=v⋅ihw∈ℋ
16 14 15 syl ⊢y∈ℋ→ιw∈ℋ|∀v∈ℋT⁡v⋅ihy=v⋅ihw∈ℋ
17 4 16 eqeltrid ⊢y∈ℋ→B∈ℋ