# Metamath Proof Explorer

## 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 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦𝑋𝑧𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡𝑦 ) ) 𝐻 ( 𝑡𝑧 ) ) } )