Metamath Proof Explorer

Theorem islno

Description: The predicate "is a linear operator." (Contributed by NM, 4-Dec-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=ULnOpW
Assertion islno ⊢U∈NrmCVec∧W∈NrmCVec→T∈L↔T:X⟶Y∧∀x∈ℂ∀y∈X∀z∈XT⁡xRyGz=xST⁡yHT⁡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=ULnOpW
8 1 2 3 4 5 6 7 lnoval ⊢U∈NrmCVec∧W∈NrmCVec→L=w∈YX|∀x∈ℂ∀y∈X∀z∈Xw⁡xRyGz=xSw⁡yHw⁡z
9 8 eleq2d ⊢U∈NrmCVec∧W∈NrmCVec→T∈L↔T∈w∈YX|∀x∈ℂ∀y∈X∀z∈Xw⁡xRyGz=xSw⁡yHw⁡z
10 fveq1 ⊢w=T→w⁡xRyGz=T⁡xRyGz
11 fveq1 ⊢w=T→w⁡y=T⁡y
12 11 oveq2d ⊢w=T→xSw⁡y=xST⁡y
13 fveq1 ⊢w=T→w⁡z=T⁡z
14 12 13 oveq12d ⊢w=T→xSw⁡yHw⁡z=xST⁡yHT⁡z
15 10 14 eqeq12d ⊢w=T→w⁡xRyGz=xSw⁡yHw⁡z↔T⁡xRyGz=xST⁡yHT⁡z
16 15 2ralbidv ⊢w=T→∀y∈X∀z∈Xw⁡xRyGz=xSw⁡yHw⁡z↔∀y∈X∀z∈XT⁡xRyGz=xST⁡yHT⁡z
17 16 ralbidv ⊢w=T→∀x∈ℂ∀y∈X∀z∈Xw⁡xRyGz=xSw⁡yHw⁡z↔∀x∈ℂ∀y∈X∀z∈XT⁡xRyGz=xST⁡yHT⁡z
18 17 elrab ⊢T∈w∈YX|∀x∈ℂ∀y∈X∀z∈Xw⁡xRyGz=xSw⁡yHw⁡z↔T∈YX∧∀x∈ℂ∀y∈X∀z∈XT⁡xRyGz=xST⁡yHT⁡z
19 2 fvexi ⊢Y∈V
20 1 fvexi ⊢X∈V
21 19 20 elmap ⊢T∈YX↔T:X⟶Y
22 21 anbi1i ⊢T∈YX∧∀x∈ℂ∀y∈X∀z∈XT⁡xRyGz=xST⁡yHT⁡z↔T:X⟶Y∧∀x∈ℂ∀y∈X∀z∈XT⁡xRyGz=xST⁡yHT⁡z
23 18 22 bitri ⊢T∈w∈YX|∀x∈ℂ∀y∈X∀z∈Xw⁡xRyGz=xSw⁡yHw⁡z↔T:X⟶Y∧∀x∈ℂ∀y∈X∀z∈XT⁡xRyGz=xST⁡yHT⁡z
24 9 23 bitrdi ⊢U∈NrmCVec∧W∈NrmCVec→T∈L↔T:X⟶Y∧∀x∈ℂ∀y∈X∀z∈XT⁡xRyGz=xST⁡yHT⁡z