# 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 𝑋 = ( BaseSet ‘ 𝑈 )
lnoval.2 𝑌 = ( BaseSet ‘ 𝑊 )
lnoval.3 𝐺 = ( +𝑣𝑈 )
lnoval.4 𝐻 = ( +𝑣𝑊 )
lnoval.5 𝑅 = ( ·𝑠OLD𝑈 )
lnoval.6 𝑆 = ( ·𝑠OLD𝑊 )
lnoval.7 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion lnolin ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵𝑋𝐶𝑋 ) ) → ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝐶 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝐵 ) ) 𝐻 ( 𝑇𝐶 ) ) )

### 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 1 2 3 4 5 6 7 islno ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇𝐿 ↔ ( 𝑇 : 𝑋𝑌 ∧ ∀ 𝑢 ∈ ℂ ∀ 𝑤𝑋𝑡𝑋 ( 𝑇 ‘ ( ( 𝑢 𝑅 𝑤 ) 𝐺 𝑡 ) ) = ( ( 𝑢 𝑆 ( 𝑇𝑤 ) ) 𝐻 ( 𝑇𝑡 ) ) ) ) )
9 8 biimp3a ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿 ) → ( 𝑇 : 𝑋𝑌 ∧ ∀ 𝑢 ∈ ℂ ∀ 𝑤𝑋𝑡𝑋 ( 𝑇 ‘ ( ( 𝑢 𝑅 𝑤 ) 𝐺 𝑡 ) ) = ( ( 𝑢 𝑆 ( 𝑇𝑤 ) ) 𝐻 ( 𝑇𝑡 ) ) ) )
10 9 simprd ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿 ) → ∀ 𝑢 ∈ ℂ ∀ 𝑤𝑋𝑡𝑋 ( 𝑇 ‘ ( ( 𝑢 𝑅 𝑤 ) 𝐺 𝑡 ) ) = ( ( 𝑢 𝑆 ( 𝑇𝑤 ) ) 𝐻 ( 𝑇𝑡 ) ) )
11 oveq1 ( 𝑢 = 𝐴 → ( 𝑢 𝑅 𝑤 ) = ( 𝐴 𝑅 𝑤 ) )
12 11 fvoveq1d ( 𝑢 = 𝐴 → ( 𝑇 ‘ ( ( 𝑢 𝑅 𝑤 ) 𝐺 𝑡 ) ) = ( 𝑇 ‘ ( ( 𝐴 𝑅 𝑤 ) 𝐺 𝑡 ) ) )
13 oveq1 ( 𝑢 = 𝐴 → ( 𝑢 𝑆 ( 𝑇𝑤 ) ) = ( 𝐴 𝑆 ( 𝑇𝑤 ) ) )
14 13 oveq1d ( 𝑢 = 𝐴 → ( ( 𝑢 𝑆 ( 𝑇𝑤 ) ) 𝐻 ( 𝑇𝑡 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝑤 ) ) 𝐻 ( 𝑇𝑡 ) ) )
15 12 14 eqeq12d ( 𝑢 = 𝐴 → ( ( 𝑇 ‘ ( ( 𝑢 𝑅 𝑤 ) 𝐺 𝑡 ) ) = ( ( 𝑢 𝑆 ( 𝑇𝑤 ) ) 𝐻 ( 𝑇𝑡 ) ) ↔ ( 𝑇 ‘ ( ( 𝐴 𝑅 𝑤 ) 𝐺 𝑡 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝑤 ) ) 𝐻 ( 𝑇𝑡 ) ) ) )
16 oveq2 ( 𝑤 = 𝐵 → ( 𝐴 𝑅 𝑤 ) = ( 𝐴 𝑅 𝐵 ) )
17 16 fvoveq1d ( 𝑤 = 𝐵 → ( 𝑇 ‘ ( ( 𝐴 𝑅 𝑤 ) 𝐺 𝑡 ) ) = ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝑡 ) ) )
18 fveq2 ( 𝑤 = 𝐵 → ( 𝑇𝑤 ) = ( 𝑇𝐵 ) )
19 18 oveq2d ( 𝑤 = 𝐵 → ( 𝐴 𝑆 ( 𝑇𝑤 ) ) = ( 𝐴 𝑆 ( 𝑇𝐵 ) ) )
20 19 oveq1d ( 𝑤 = 𝐵 → ( ( 𝐴 𝑆 ( 𝑇𝑤 ) ) 𝐻 ( 𝑇𝑡 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝐵 ) ) 𝐻 ( 𝑇𝑡 ) ) )
21 17 20 eqeq12d ( 𝑤 = 𝐵 → ( ( 𝑇 ‘ ( ( 𝐴 𝑅 𝑤 ) 𝐺 𝑡 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝑤 ) ) 𝐻 ( 𝑇𝑡 ) ) ↔ ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝑡 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝐵 ) ) 𝐻 ( 𝑇𝑡 ) ) ) )
22 oveq2 ( 𝑡 = 𝐶 → ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝑡 ) = ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝐶 ) )
23 22 fveq2d ( 𝑡 = 𝐶 → ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝑡 ) ) = ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝐶 ) ) )
24 fveq2 ( 𝑡 = 𝐶 → ( 𝑇𝑡 ) = ( 𝑇𝐶 ) )
25 24 oveq2d ( 𝑡 = 𝐶 → ( ( 𝐴 𝑆 ( 𝑇𝐵 ) ) 𝐻 ( 𝑇𝑡 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝐵 ) ) 𝐻 ( 𝑇𝐶 ) ) )
26 23 25 eqeq12d ( 𝑡 = 𝐶 → ( ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝑡 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝐵 ) ) 𝐻 ( 𝑇𝑡 ) ) ↔ ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝐶 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝐵 ) ) 𝐻 ( 𝑇𝐶 ) ) ) )
27 15 21 26 rspc3v ( ( 𝐴 ∈ ℂ ∧ 𝐵𝑋𝐶𝑋 ) → ( ∀ 𝑢 ∈ ℂ ∀ 𝑤𝑋𝑡𝑋 ( 𝑇 ‘ ( ( 𝑢 𝑅 𝑤 ) 𝐺 𝑡 ) ) = ( ( 𝑢 𝑆 ( 𝑇𝑤 ) ) 𝐻 ( 𝑇𝑡 ) ) → ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝐶 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝐵 ) ) 𝐻 ( 𝑇𝐶 ) ) ) )
28 10 27 mpan9 ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵𝑋𝐶𝑋 ) ) → ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝐶 ) ) = ( ( 𝐴 𝑆 ( 𝑇𝐵 ) ) 𝐻 ( 𝑇𝐶 ) ) )