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 ⊢ X = BaseSet ⁡ U
lnoval.2 ⊢ Y = BaseSet ⁡ W
lnoval.3 ⊢ G = + v ⁡ U
lnoval.4 ⊢ H = + v ⁡ W
lnoval.5 ⊢ R = ⋅ 𝑠OLD ⁡ U
lnoval.6 ⊢ S = ⋅ 𝑠OLD ⁡ W
lnoval.7 ⊢ L = U LnOp W
Assertion lnoval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → L = t ∈ Y X | ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x S t ⁡ y H t ⁡ z

Proof

Step Hyp Ref Expression
1 lnoval.1 ⊢ X = BaseSet ⁡ U
2 lnoval.2 ⊢ Y = BaseSet ⁡ W
3 lnoval.3 ⊢ G = + v ⁡ U
4 lnoval.4 ⊢ H = + v ⁡ W
5 lnoval.5 ⊢ R = ⋅ 𝑠OLD ⁡ U
6 lnoval.6 ⊢ S = ⋅ 𝑠OLD ⁡ W
7 lnoval.7 ⊢ L = U LnOp W
8 fveq2 ⊢ u = U → BaseSet ⁡ u = BaseSet ⁡ U
9 8 1 eqtr4di ⊢ u = U → BaseSet ⁡ u = X
10 9 oveq2d ⊢ u = U → BaseSet ⁡ w BaseSet ⁡ u = BaseSet ⁡ w X
11 fveq2 ⊢ u = U → + v ⁡ u = + v ⁡ U
12 11 3 eqtr4di ⊢ u = U → + v ⁡ u = G
13 fveq2 ⊢ u = U → ⋅ 𝑠OLD ⁡ u = ⋅ 𝑠OLD ⁡ U
14 13 5 eqtr4di ⊢ u = U → ⋅ 𝑠OLD ⁡ u = R
15 14 oveqd ⊢ u = U → x ⋅ 𝑠OLD ⁡ u y = x R y
16 eqidd ⊢ u = U → z = z
17 12 15 16 oveq123d ⊢ u = U → x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x R y G z
18 17 fveqeq2d ⊢ u = U → t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z ↔ t ⁡ x R y G z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
19 9 18 raleqbidv ⊢ u = U → ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z ↔ ∀ z ∈ X t ⁡ x R y G z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
20 9 19 raleqbidv ⊢ u = U → ∀ y ∈ BaseSet ⁡ u ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z ↔ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
21 20 ralbidv ⊢ u = U → ∀ x ∈ ℂ ∀ y ∈ BaseSet ⁡ u ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z ↔ ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
22 10 21 rabeqbidv ⊢ u = U → t ∈ BaseSet ⁡ w BaseSet ⁡ u | ∀ x ∈ ℂ ∀ y ∈ BaseSet ⁡ u ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z = t ∈ BaseSet ⁡ w X | ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
23 fveq2 ⊢ w = W → BaseSet ⁡ w = BaseSet ⁡ W
24 23 2 eqtr4di ⊢ w = W → BaseSet ⁡ w = Y
25 24 oveq1d ⊢ w = W → BaseSet ⁡ w X = Y X
26 fveq2 ⊢ w = W → + v ⁡ w = + v ⁡ W
27 26 4 eqtr4di ⊢ w = W → + v ⁡ w = H
28 fveq2 ⊢ w = W → ⋅ 𝑠OLD ⁡ w = ⋅ 𝑠OLD ⁡ W
29 28 6 eqtr4di ⊢ w = W → ⋅ 𝑠OLD ⁡ w = S
30 29 oveqd ⊢ w = W → x ⋅ 𝑠OLD ⁡ w t ⁡ y = x S t ⁡ y
31 eqidd ⊢ w = W → t ⁡ z = t ⁡ z
32 27 30 31 oveq123d ⊢ w = W → x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z = x S t ⁡ y H t ⁡ z
33 32 eqeq2d ⊢ w = W → t ⁡ x R y G z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z ↔ t ⁡ x R y G z = x S t ⁡ y H t ⁡ z
34 33 2ralbidv ⊢ w = W → ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z ↔ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x S t ⁡ y H t ⁡ z
35 34 ralbidv ⊢ w = W → ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z ↔ ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x S t ⁡ y H t ⁡ z
36 25 35 rabeqbidv ⊢ w = W → t ∈ BaseSet ⁡ w X | ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z = t ∈ Y X | ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x S t ⁡ y H t ⁡ z
37 df-lno ⊢ LnOp = u ∈ NrmCVec , w ∈ NrmCVec ⟼ t ∈ BaseSet ⁡ w BaseSet ⁡ u | ∀ x ∈ ℂ ∀ y ∈ BaseSet ⁡ u ∀ z ∈ BaseSet ⁡ u t ⁡ x ⋅ 𝑠OLD ⁡ u y + v ⁡ u z = x ⋅ 𝑠OLD ⁡ w t ⁡ y + v ⁡ w t ⁡ z
38 ovex ⊢ Y X ∈ V
39 38 rabex ⊢ t ∈ Y X | ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x S t ⁡ y H t ⁡ z ∈ V
40 22 36 37 39 ovmpo ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → U LnOp W = t ∈ Y X | ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x S t ⁡ y H t ⁡ z
41 7 40 syl5eq ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → L = t ∈ Y X | ∀ x ∈ ℂ ∀ y ∈ X ∀ z ∈ X t ⁡ x R y G z = x S t ⁡ y H t ⁡ z