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	⊢ 𝑇 ∈ LinOp
	cnlnadjlem.2	⊢ 𝑇 ∈ ContOp
	cnlnadjlem.3	⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
	cnlnadjlem.4	⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
	cnlnadjlem.5	⊢ 𝐹 = ( 𝑦 ∈ ℋ ↦ 𝐵 )
Assertion	cnlnadjlem5	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐶 ) ·ih 𝐴 ) = ( 𝐶 ·ih ( 𝐹 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnlnadjlem.1	⊢ 𝑇 ∈ LinOp
2		cnlnadjlem.2	⊢ 𝑇 ∈ ContOp
3		cnlnadjlem.3	⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
4		cnlnadjlem.4	⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
5		cnlnadjlem.5	⊢ 𝐹 = ( 𝑦 ∈ ℋ ↦ 𝐵 )
6		nfcv	⊢ Ⅎ 𝑦 𝐴
7		nfcv	⊢ Ⅎ 𝑦 ℋ
8		nfcv	⊢ Ⅎ 𝑦 𝑓
9		nfcv	⊢ Ⅎ 𝑦 ·ih
10		nfmpt1	⊢ Ⅎ 𝑦 ( 𝑦 ∈ ℋ ↦ 𝐵 )
11	5 10	nfcxfr	⊢ Ⅎ 𝑦 𝐹
12	11 6	nffv	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝐴 )
13	8 9 12	nfov	⊢ Ⅎ 𝑦 ( 𝑓 ·ih ( 𝐹 ‘ 𝐴 ) )
14	13	nfeq2	⊢ Ⅎ 𝑦 ( ( 𝑇 ‘ 𝑓 ) ·ih 𝐴 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝐴 ) )
15	7 14	nfralw	⊢ Ⅎ 𝑦 ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝐴 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝐴 ) )
16		oveq2	⊢ ( 𝑦 = 𝐴 → ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑓 ) ·ih 𝐴 ) )
17		fveq2	⊢ ( 𝑦 = 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
18	17	oveq2d	⊢ ( 𝑦 = 𝐴 → ( 𝑓 ·ih ( 𝐹 ‘ 𝑦 ) ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝐴 ) ) )
19	16 18	eqeq12d	⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝐴 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝐴 ) ) ) )
20	19	ralbidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝐴 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝐴 ) ) ) )
21		riotaex	⊢ ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) ) ∈ V
22	4 21	eqeltri	⊢ 𝐵 ∈ V
23	5	fvmpt2	⊢ ( ( 𝑦 ∈ ℋ ∧ 𝐵 ∈ V ) → ( 𝐹 ‘ 𝑦 ) = 𝐵 )
24	22 23	mpan2	⊢ ( 𝑦 ∈ ℋ → ( 𝐹 ‘ 𝑦 ) = 𝐵 )
25		fveq2	⊢ ( 𝑣 = 𝑓 → ( 𝑇 ‘ 𝑣 ) = ( 𝑇 ‘ 𝑓 ) )
26	25	oveq1d	⊢ ( 𝑣 = 𝑓 → ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) )
27		oveq1	⊢ ( 𝑣 = 𝑓 → ( 𝑣 ·ih 𝑤 ) = ( 𝑓 ·ih 𝑤 ) )
28	26 27	eqeq12d	⊢ ( 𝑣 = 𝑓 → ( ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) ↔ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih 𝑤 ) ) )
29	28	cbvralvw	⊢ ( ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih 𝑤 ) )
30	29	a1i	⊢ ( 𝑤 ∈ ℋ → ( ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih 𝑤 ) ) )
31	1 2 3	cnlnadjlem1	⊢ ( 𝑓 ∈ ℋ → ( 𝐺 ‘ 𝑓 ) = ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) )
32	31	eqeq1d	⊢ ( 𝑓 ∈ ℋ → ( ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) ↔ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih 𝑤 ) ) )
33	32	ralbiia	⊢ ( ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) ↔ ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih 𝑤 ) )
34	30 33	bitr4di	⊢ ( 𝑤 ∈ ℋ → ( ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) ) )
35	34	riotabiia	⊢ ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) ) = ( ℩ 𝑤 ∈ ℋ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) )
36	4 35	eqtri	⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) )
37	1 2 3	cnlnadjlem2	⊢ ( 𝑦 ∈ ℋ → ( 𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn ) )
38		elin	⊢ ( 𝐺 ∈ ( LinFn ∩ ContFn ) ↔ ( 𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn ) )
39	37 38	sylibr	⊢ ( 𝑦 ∈ ℋ → 𝐺 ∈ ( LinFn ∩ ContFn ) )
40		riesz4	⊢ ( 𝐺 ∈ ( LinFn ∩ ContFn ) → ∃! 𝑤 ∈ ℋ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) )
41		riotacl2	⊢ ( ∃! 𝑤 ∈ ℋ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) → ( ℩ 𝑤 ∈ ℋ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) ) ∈ { 𝑤 ∈ ℋ ∣ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) } )
42	39 40 41	3syl	⊢ ( 𝑦 ∈ ℋ → ( ℩ 𝑤 ∈ ℋ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) ) ∈ { 𝑤 ∈ ℋ ∣ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) } )
43	36 42	eqeltrid	⊢ ( 𝑦 ∈ ℋ → 𝐵 ∈ { 𝑤 ∈ ℋ ∣ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) } )
44	24 43	eqeltrd	⊢ ( 𝑦 ∈ ℋ → ( 𝐹 ‘ 𝑦 ) ∈ { 𝑤 ∈ ℋ ∣ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) } )
45		oveq2	⊢ ( 𝑤 = ( 𝐹 ‘ 𝑦 ) → ( 𝑓 ·ih 𝑤 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝑦 ) ) )
46	45	eqeq2d	⊢ ( 𝑤 = ( 𝐹 ‘ 𝑦 ) → ( ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih 𝑤 ) ↔ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝑦 ) ) ) )
47	46	ralbidv	⊢ ( 𝑤 = ( 𝐹 ‘ 𝑦 ) → ( ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih 𝑤 ) ↔ ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝑦 ) ) ) )
48	33 47	bitrid	⊢ ( 𝑤 = ( 𝐹 ‘ 𝑦 ) → ( ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) ↔ ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝑦 ) ) ) )
49	48	elrab	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ { 𝑤 ∈ ℋ ∣ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) } ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ ℋ ∧ ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝑦 ) ) ) )
50	49	simprbi	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ { 𝑤 ∈ ℋ ∣ ∀ 𝑓 ∈ ℋ ( 𝐺 ‘ 𝑓 ) = ( 𝑓 ·ih 𝑤 ) } → ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝑦 ) ) )
51	44 50	syl	⊢ ( 𝑦 ∈ ℋ → ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝑦 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝑦 ) ) )
52	6 15 20 51	vtoclgaf	⊢ ( 𝐴 ∈ ℋ → ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝐴 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝐴 ) ) )
53		fveq2	⊢ ( 𝑓 = 𝐶 → ( 𝑇 ‘ 𝑓 ) = ( 𝑇 ‘ 𝐶 ) )
54	53	oveq1d	⊢ ( 𝑓 = 𝐶 → ( ( 𝑇 ‘ 𝑓 ) ·ih 𝐴 ) = ( ( 𝑇 ‘ 𝐶 ) ·ih 𝐴 ) )
55		oveq1	⊢ ( 𝑓 = 𝐶 → ( 𝑓 ·ih ( 𝐹 ‘ 𝐴 ) ) = ( 𝐶 ·ih ( 𝐹 ‘ 𝐴 ) ) )
56	54 55	eqeq12d	⊢ ( 𝑓 = 𝐶 → ( ( ( 𝑇 ‘ 𝑓 ) ·ih 𝐴 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝐴 ) ) ↔ ( ( 𝑇 ‘ 𝐶 ) ·ih 𝐴 ) = ( 𝐶 ·ih ( 𝐹 ‘ 𝐴 ) ) ) )
57	56	rspccva	⊢ ( ( ∀ 𝑓 ∈ ℋ ( ( 𝑇 ‘ 𝑓 ) ·ih 𝐴 ) = ( 𝑓 ·ih ( 𝐹 ‘ 𝐴 ) ) ∧ 𝐶 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐶 ) ·ih 𝐴 ) = ( 𝐶 ·ih ( 𝐹 ‘ 𝐴 ) ) )
58	52 57	sylan	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝑇 ‘ 𝐶 ) ·ih 𝐴 ) = ( 𝐶 ·ih ( 𝐹 ‘ 𝐴 ) ) )