Metamath Proof Explorer

Theorem lnolin

Description: Basic linearity property of 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 lnolin ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈ℂ∧B∈X∧C∈X→T⁡ARBGC=AST⁡BHT⁡C

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 islno ⊢U∈NrmCVec∧W∈NrmCVec→T∈L↔T:X⟶Y∧∀u∈ℂ∀w∈X∀t∈XT⁡uRwGt=uST⁡wHT⁡t
9 8 biimp3a ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→T:X⟶Y∧∀u∈ℂ∀w∈X∀t∈XT⁡uRwGt=uST⁡wHT⁡t
10 9 simprd ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→∀u∈ℂ∀w∈X∀t∈XT⁡uRwGt=uST⁡wHT⁡t
11 oveq1 ⊢u=A→uRw=ARw
12 11 fvoveq1d ⊢u=A→T⁡uRwGt=T⁡ARwGt
13 oveq1 ⊢u=A→uST⁡w=AST⁡w
14 13 oveq1d ⊢u=A→uST⁡wHT⁡t=AST⁡wHT⁡t
15 12 14 eqeq12d ⊢u=A→T⁡uRwGt=uST⁡wHT⁡t↔T⁡ARwGt=AST⁡wHT⁡t
16 oveq2 ⊢w=B→ARw=ARB
17 16 fvoveq1d ⊢w=B→T⁡ARwGt=T⁡ARBGt
18 fveq2 ⊢w=B→T⁡w=T⁡B
19 18 oveq2d ⊢w=B→AST⁡w=AST⁡B
20 19 oveq1d ⊢w=B→AST⁡wHT⁡t=AST⁡BHT⁡t
21 17 20 eqeq12d ⊢w=B→T⁡ARwGt=AST⁡wHT⁡t↔T⁡ARBGt=AST⁡BHT⁡t
22 oveq2 ⊢t=C→ARBGt=ARBGC
23 22 fveq2d ⊢t=C→T⁡ARBGt=T⁡ARBGC
24 fveq2 ⊢t=C→T⁡t=T⁡C
25 24 oveq2d ⊢t=C→AST⁡BHT⁡t=AST⁡BHT⁡C
26 23 25 eqeq12d ⊢t=C→T⁡ARBGt=AST⁡BHT⁡t↔T⁡ARBGC=AST⁡BHT⁡C
27 15 21 26 rspc3v ⊢A∈ℂ∧B∈X∧C∈X→∀u∈ℂ∀w∈X∀t∈XT⁡uRwGt=uST⁡wHT⁡t→T⁡ARBGC=AST⁡BHT⁡C
28 10 27 mpan9 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈ℂ∧B∈X∧C∈X→T⁡ARBGC=AST⁡BHT⁡C