Metamath Proof Explorer

Theorem lnoadd

Description: Addition property of a linear operator. (Contributed by NM, 7-Dec-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lnoadd.1 ⊢X=BaseSet⁡U
lnoadd.5 ⊢G=+v⁡U
lnoadd.6 ⊢H=+v⁡W
lnoadd.7 ⊢L=ULnOpW
Assertion lnoadd ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡AGB=T⁡AHT⁡B

Proof

Step Hyp Ref Expression
1 lnoadd.1 ⊢X=BaseSet⁡U
2 lnoadd.5 ⊢G=+v⁡U
3 lnoadd.6 ⊢H=+v⁡W
4 lnoadd.7 ⊢L=ULnOpW
5 ax-1cn ⊢1∈ℂ
6 eqid ⊢BaseSet⁡W=BaseSet⁡W
7 eqid ⊢⋅𝑠OLD⁡U=⋅𝑠OLD⁡U
8 eqid ⊢⋅𝑠OLD⁡W=⋅𝑠OLD⁡W
9 1 6 2 3 7 8 4 lnolin ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧1∈ℂ∧A∈X∧B∈X→T⁡1⋅𝑠OLD⁡UAGB=1⋅𝑠OLD⁡WT⁡AHT⁡B
10 5 9 mp3anr1 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡1⋅𝑠OLD⁡UAGB=1⋅𝑠OLD⁡WT⁡AHT⁡B
11 simp1 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→U∈NrmCVec
12 simpl ⊢A∈X∧B∈X→A∈X
13 1 7 nvsid ⊢U∈NrmCVec∧A∈X→1⋅𝑠OLD⁡UA=A
14 11 12 13 syl2an ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→1⋅𝑠OLD⁡UA=A
15 14 fvoveq1d ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡1⋅𝑠OLD⁡UAGB=T⁡AGB
16 simpl2 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→W∈NrmCVec
17 1 6 4 lnof ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→T:X⟶BaseSet⁡W
18 ffvelcdm ⊢T:X⟶BaseSet⁡W∧A∈X→T⁡A∈BaseSet⁡W
19 17 12 18 syl2an ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡A∈BaseSet⁡W
20 6 8 nvsid ⊢W∈NrmCVec∧T⁡A∈BaseSet⁡W→1⋅𝑠OLD⁡WT⁡A=T⁡A
21 16 19 20 syl2anc ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→1⋅𝑠OLD⁡WT⁡A=T⁡A
22 21 oveq1d ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→1⋅𝑠OLD⁡WT⁡AHT⁡B=T⁡AHT⁡B
23 10 15 22 3eqtr3d ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧A∈X∧B∈X→T⁡AGB=T⁡AHT⁡B