Theorem lnoval

Description: The set of linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnoval.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	lnoval.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	lnoval.3	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	lnoval.4	⊢ 𝐻 = ( +𝑣 ‘ 𝑊 )
	lnoval.5	⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑈 )
	lnoval.6	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑊 )
	lnoval.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion	lnoval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐿 = { 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) 𝐻 ( 𝑡 ‘ 𝑧 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		lnoval.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		lnoval.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		lnoval.3	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
4		lnoval.4	⊢ 𝐻 = ( +𝑣 ‘ 𝑊 )
5		lnoval.5	⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑈 )
6		lnoval.6	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑊 )
7		lnoval.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
8		fveq2	⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = ( BaseSet ‘ 𝑈 ) )
9	8 1	eqtr4di	⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = 𝑋 )
10	9	oveq2d	⊢ ( 𝑢 = 𝑈 → ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) = ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) )
11		fveq2	⊢ ( 𝑢 = 𝑈 → ( +𝑣 ‘ 𝑢 ) = ( +𝑣 ‘ 𝑈 ) )
12	11 3	eqtr4di	⊢ ( 𝑢 = 𝑈 → ( +𝑣 ‘ 𝑢 ) = 𝐺 )
13		fveq2	⊢ ( 𝑢 = 𝑈 → ( ·𝑠OLD ‘ 𝑢 ) = ( ·𝑠OLD ‘ 𝑈 ) )
14	13 5	eqtr4di	⊢ ( 𝑢 = 𝑈 → ( ·𝑠OLD ‘ 𝑢 ) = 𝑅 )
15	14	oveqd	⊢ ( 𝑢 = 𝑈 → ( 𝑥 ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) = ( 𝑥 𝑅 𝑦 ) )
16		eqidd	⊢ ( 𝑢 = 𝑈 → 𝑧 = 𝑧 )
17	12 15 16	oveq123d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ( +𝑣 ‘ 𝑢 ) 𝑧 ) = ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) )
18	17	fveqeq2d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑡 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ( +𝑣 ‘ 𝑢 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ↔ ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ) )
19	9 18	raleqbidv	⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( 𝑡 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ( +𝑣 ‘ 𝑢 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ) )
20	9 19	raleqbidv	⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑦 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( 𝑡 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ( +𝑣 ‘ 𝑢 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ) )
21	20	ralbidv	⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( 𝑡 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ( +𝑣 ‘ 𝑢 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ↔ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ) )
22	10 21	rabeqbidv	⊢ ( 𝑢 = 𝑈 → { 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( 𝑡 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ( +𝑣 ‘ 𝑢 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) } = { 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) } )
23		fveq2	⊢ ( 𝑤 = 𝑊 → ( BaseSet ‘ 𝑤 ) = ( BaseSet ‘ 𝑊 ) )
24	23 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( BaseSet ‘ 𝑤 ) = 𝑌 )
25	24	oveq1d	⊢ ( 𝑤 = 𝑊 → ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) = ( 𝑌 ↑m 𝑋 ) )
26		fveq2	⊢ ( 𝑤 = 𝑊 → ( +𝑣 ‘ 𝑤 ) = ( +𝑣 ‘ 𝑊 ) )
27	26 4	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( +𝑣 ‘ 𝑤 ) = 𝐻 )
28		fveq2	⊢ ( 𝑤 = 𝑊 → ( ·𝑠OLD ‘ 𝑤 ) = ( ·𝑠OLD ‘ 𝑊 ) )
29	28 6	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( ·𝑠OLD ‘ 𝑤 ) = 𝑆 )
30	29	oveqd	⊢ ( 𝑤 = 𝑊 → ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) = ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) )
31		eqidd	⊢ ( 𝑤 = 𝑊 → ( 𝑡 ‘ 𝑧 ) = ( 𝑡 ‘ 𝑧 ) )
32	27 30 31	oveq123d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) 𝐻 ( 𝑡 ‘ 𝑧 ) ) )
33	32	eqeq2d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ↔ ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) 𝐻 ( 𝑡 ‘ 𝑧 ) ) ) )
34	33	2ralbidv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) 𝐻 ( 𝑡 ‘ 𝑧 ) ) ) )
35	34	ralbidv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) ↔ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) 𝐻 ( 𝑡 ‘ 𝑧 ) ) ) )
36	25 35	rabeqbidv	⊢ ( 𝑤 = 𝑊 → { 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) } = { 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) 𝐻 ( 𝑡 ‘ 𝑧 ) ) } )
37		df-lno	⊢ LnOp = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ { 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( 𝑡 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑢 ) 𝑦 ) ( +𝑣 ‘ 𝑢 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑤 ) ( 𝑡 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑤 ) ( 𝑡 ‘ 𝑧 ) ) } )
38		ovex	⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
39	38	rabex	⊢ { 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) 𝐻 ( 𝑡 ‘ 𝑧 ) ) } ∈ V
40	22 36 37 39	ovmpo	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑈 LnOp 𝑊 ) = { 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) 𝐻 ( 𝑡 ‘ 𝑧 ) ) } )
41	7 40	syl5eq	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐿 = { 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) 𝐻 ( 𝑡 ‘ 𝑧 ) ) } )