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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
lnoval.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
lnoval.3 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
lnoval.4 ⊢ 𝐻 = ( +𝑣 ‘ 𝑊 )
lnoval.5 ⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑈 )
lnoval.6 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑊 )
lnoval.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion islno ( ( 𝑈 ∈ 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 lnoval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐿 = { 𝑤 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑤 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑤 ‘ 𝑦 ) ) 𝐻 ( 𝑤 ‘ 𝑧 ) ) } )
9 8 eleq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐿 ↔ 𝑇 ∈ { 𝑤 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑤 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑤 ‘ 𝑦 ) ) 𝐻 ( 𝑤 ‘ 𝑧 ) ) } ) )
10 fveq1 ⊢ ( 𝑤 = 𝑇 → ( 𝑤 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( 𝑇 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) )
11 fveq1 ⊢ ( 𝑤 = 𝑇 → ( 𝑤 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) )
12 11 oveq2d ⊢ ( 𝑤 = 𝑇 → ( 𝑥 𝑆 ( 𝑤 ‘ 𝑦 ) ) = ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) )
13 fveq1 ⊢ ( 𝑤 = 𝑇 → ( 𝑤 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑧 ) )
14 12 13 oveq12d ⊢ ( 𝑤 = 𝑇 → ( ( 𝑥 𝑆 ( 𝑤 ‘ 𝑦 ) ) 𝐻 ( 𝑤 ‘ 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) 𝐻 ( 𝑇 ‘ 𝑧 ) ) )
15 10 14 eqeq12d ⊢ ( 𝑤 = 𝑇 → ( ( 𝑤 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑤 ‘ 𝑦 ) ) 𝐻 ( 𝑤 ‘ 𝑧 ) ) ↔ ( 𝑇 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) 𝐻 ( 𝑇 ‘ 𝑧 ) ) ) )
16 15 2ralbidv ⊢ ( 𝑤 = 𝑇 → ( ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑤 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑤 ‘ 𝑦 ) ) 𝐻 ( 𝑤 ‘ 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑇 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) 𝐻 ( 𝑇 ‘ 𝑧 ) ) ) )
17 16 ralbidv ⊢ ( 𝑤 = 𝑇 → ( ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑤 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑤 ‘ 𝑦 ) ) 𝐻 ( 𝑤 ‘ 𝑧 ) ) ↔ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑇 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) 𝐻 ( 𝑇 ‘ 𝑧 ) ) ) )
18 17 elrab ⊢ ( 𝑇 ∈ { 𝑤 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑤 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑤 ‘ 𝑦 ) ) 𝐻 ( 𝑤 ‘ 𝑧 ) ) } ↔ ( 𝑇 ∈ ( 𝑌 ↑m 𝑋 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑇 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) 𝐻 ( 𝑇 ‘ 𝑧 ) ) ) )
19 2 fvexi ⊢ 𝑌 ∈ V
20 1 fvexi ⊢ 𝑋 ∈ V
21 19 20 elmap ⊢ ( 𝑇 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝑇 : 𝑋 ⟶ 𝑌 )
22 21 anbi1i ⊢ ( ( 𝑇 ∈ ( 𝑌 ↑m 𝑋 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑇 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) 𝐻 ( 𝑇 ‘ 𝑧 ) ) ) ↔ ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑇 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) 𝐻 ( 𝑇 ‘ 𝑧 ) ) ) )
23 18 22 bitri ⊢ ( 𝑇 ∈ { 𝑤 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑤 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑤 ‘ 𝑦 ) ) 𝐻 ( 𝑤 ‘ 𝑧 ) ) } ↔ ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑇 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) 𝐻 ( 𝑇 ‘ 𝑧 ) ) ) )
24 9 23 bitrdi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐿 ↔ ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑇 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) 𝐻 ( 𝑇 ‘ 𝑧 ) ) ) ) )