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 ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 𝐴 𝑅 𝐵 ) 𝐺 𝐶 ) ) = ( ( 𝐴 𝑆 ( 𝑇 ‘ 𝐵 ) ) 𝐻 ( 𝑇 ‘ 𝐶 ) ) )