Metamath Proof Explorer

Theorem cnlnadjlem5

Description: Lemma for cnlnadji . F is an adjoint of T (later, we will show it is unique). (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 cnlnadjlem5 ⊢A∈ℋ∧C∈ℋ→T⁡C⋅ihA=C⋅ihF⁡A

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 nfcv ⊢Ⅎ_yA
7 nfcv ⊢Ⅎ_yℋ
8 nfcv ⊢Ⅎ_yf
9 nfcv ⊢Ⅎ_y⋅ih
10 nfmpt1 ⊢Ⅎ_yy∈ℋ⟼B
11 5 10 nfcxfr ⊢Ⅎ_yF
12 11 6 nffv ⊢Ⅎ_yF⁡A
13 8 9 12 nfov ⊢Ⅎ_yf⋅ihF⁡A
14 13 nfeq2 ⊢ℲyT⁡f⋅ihA=f⋅ihF⁡A
15 7 14 nfralw ⊢Ⅎy∀f∈ℋT⁡f⋅ihA=f⋅ihF⁡A
16 oveq2 ⊢y=A→T⁡f⋅ihy=T⁡f⋅ihA
17 fveq2 ⊢y=A→F⁡y=F⁡A
18 17 oveq2d ⊢y=A→f⋅ihF⁡y=f⋅ihF⁡A
19 16 18 eqeq12d ⊢y=A→T⁡f⋅ihy=f⋅ihF⁡y↔T⁡f⋅ihA=f⋅ihF⁡A
20 19 ralbidv ⊢y=A→∀f∈ℋT⁡f⋅ihy=f⋅ihF⁡y↔∀f∈ℋT⁡f⋅ihA=f⋅ihF⁡A
21 riotaex ⊢ιw∈ℋ|∀v∈ℋT⁡v⋅ihy=v⋅ihw∈V
22 4 21 eqeltri ⊢B∈V
23 5 fvmpt2 ⊢y∈ℋ∧B∈V→F⁡y=B
24 22 23 mpan2 ⊢y∈ℋ→F⁡y=B
25 fveq2 ⊢v=f→T⁡v=T⁡f
26 25 oveq1d ⊢v=f→T⁡v⋅ihy=T⁡f⋅ihy
27 oveq1 ⊢v=f→v⋅ihw=f⋅ihw
28 26 27 eqeq12d ⊢v=f→T⁡v⋅ihy=v⋅ihw↔T⁡f⋅ihy=f⋅ihw
29 28 cbvralvw ⊢∀v∈ℋT⁡v⋅ihy=v⋅ihw↔∀f∈ℋT⁡f⋅ihy=f⋅ihw
30 29 a1i ⊢w∈ℋ→∀v∈ℋT⁡v⋅ihy=v⋅ihw↔∀f∈ℋT⁡f⋅ihy=f⋅ihw
31 1 2 3 cnlnadjlem1 ⊢f∈ℋ→G⁡f=T⁡f⋅ihy
32 31 eqeq1d ⊢f∈ℋ→G⁡f=f⋅ihw↔T⁡f⋅ihy=f⋅ihw
33 32 ralbiia ⊢∀f∈ℋG⁡f=f⋅ihw↔∀f∈ℋT⁡f⋅ihy=f⋅ihw
34 30 33 bitr4di ⊢w∈ℋ→∀v∈ℋT⁡v⋅ihy=v⋅ihw↔∀f∈ℋG⁡f=f⋅ihw
35 34 riotabiia ⊢ιw∈ℋ|∀v∈ℋT⁡v⋅ihy=v⋅ihw=ιw∈ℋ|∀f∈ℋG⁡f=f⋅ihw
36 4 35 eqtri ⊢B=ιw∈ℋ|∀f∈ℋG⁡f=f⋅ihw
37 1 2 3 cnlnadjlem2 ⊢y∈ℋ→G∈LinFn∧G∈ContFn
38 elin ⊢G∈LinFn∩ContFn↔G∈LinFn∧G∈ContFn
39 37 38 sylibr ⊢y∈ℋ→G∈LinFn∩ContFn
40 riesz4 ⊢G∈LinFn∩ContFn→∃!w∈ℋ∀f∈ℋG⁡f=f⋅ihw
41 riotacl2 ⊢∃!w∈ℋ∀f∈ℋG⁡f=f⋅ihw→ιw∈ℋ|∀f∈ℋG⁡f=f⋅ihw∈w∈ℋ|∀f∈ℋG⁡f=f⋅ihw
42 39 40 41 3syl ⊢y∈ℋ→ιw∈ℋ|∀f∈ℋG⁡f=f⋅ihw∈w∈ℋ|∀f∈ℋG⁡f=f⋅ihw
43 36 42 eqeltrid ⊢y∈ℋ→B∈w∈ℋ|∀f∈ℋG⁡f=f⋅ihw
44 24 43 eqeltrd ⊢y∈ℋ→F⁡y∈w∈ℋ|∀f∈ℋG⁡f=f⋅ihw
45 oveq2 ⊢w=F⁡y→f⋅ihw=f⋅ihF⁡y
46 45 eqeq2d ⊢w=F⁡y→T⁡f⋅ihy=f⋅ihw↔T⁡f⋅ihy=f⋅ihF⁡y
47 46 ralbidv ⊢w=F⁡y→∀f∈ℋT⁡f⋅ihy=f⋅ihw↔∀f∈ℋT⁡f⋅ihy=f⋅ihF⁡y
48 33 47 bitrid ⊢w=F⁡y→∀f∈ℋG⁡f=f⋅ihw↔∀f∈ℋT⁡f⋅ihy=f⋅ihF⁡y
49 48 elrab ⊢F⁡y∈w∈ℋ|∀f∈ℋG⁡f=f⋅ihw↔F⁡y∈ℋ∧∀f∈ℋT⁡f⋅ihy=f⋅ihF⁡y
50 49 simprbi ⊢F⁡y∈w∈ℋ|∀f∈ℋG⁡f=f⋅ihw→∀f∈ℋT⁡f⋅ihy=f⋅ihF⁡y
51 44 50 syl ⊢y∈ℋ→∀f∈ℋT⁡f⋅ihy=f⋅ihF⁡y
52 6 15 20 51 vtoclgaf ⊢A∈ℋ→∀f∈ℋT⁡f⋅ihA=f⋅ihF⁡A
53 fveq2 ⊢f=C→T⁡f=T⁡C
54 53 oveq1d ⊢f=C→T⁡f⋅ihA=T⁡C⋅ihA
55 oveq1 ⊢f=C→f⋅ihF⁡A=C⋅ihF⁡A
56 54 55 eqeq12d ⊢f=C→T⁡f⋅ihA=f⋅ihF⁡A↔T⁡C⋅ihA=C⋅ihF⁡A
57 56 rspccva ⊢∀f∈ℋT⁡f⋅ihA=f⋅ihF⁡A∧C∈ℋ→T⁡C⋅ihA=C⋅ihF⁡A
58 52 57 sylan ⊢A∈ℋ∧C∈ℋ→T⁡C⋅ihA=C⋅ihF⁡A