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 ⋅ ih y
cnlnadjlem.4 ⊢ B = ι w ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w
cnlnadjlem.5 ⊢ F = y ∈ ℋ ⟼ B
Assertion cnlnadjlem5 ⊢ A ∈ ℋ ∧ C ∈ ℋ → T ⁡ C ⋅ ih A = C ⋅ ih F ⁡ A

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