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 ) → ( 𝑇 ∈ 𝐿 ↔ ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( 𝑇 ‘ ( ( 𝑥 𝑅 𝑦 ) 𝐺 𝑧 ) ) = ( ( 𝑥 𝑆 ( 𝑇 ‘ 𝑦 ) ) 𝐻 ( 𝑇 ‘ 𝑧 ) ) ) ) )