This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐿 = { 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑡 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑡 ‘ 𝑦 ) ) 𝐻 ( 𝑡 ‘ 𝑧 ) ) } )