Theorem lflset

Description: The set of linear functionals in a left module or left vector space. (Contributed by NM, 15-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	lflset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lflset.a	⊢ + = ( +g ‘ 𝑊 )
	lflset.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	lflset.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lflset.k	⊢ 𝐾 = ( Base ‘ 𝐷 )
	lflset.p	⊢ ⨣ = ( +g ‘ 𝐷 )
	lflset.t	⊢ × = ( .r ‘ 𝐷 )
	lflset.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
Assertion	lflset	⊢ ( 𝑊 ∈ 𝑋 → 𝐹 = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		lflset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lflset.a	⊢ + = ( +g ‘ 𝑊 )
3		lflset.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
4		lflset.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		lflset.k	⊢ 𝐾 = ( Base ‘ 𝐷 )
6		lflset.p	⊢ ⨣ = ( +g ‘ 𝐷 )
7		lflset.t	⊢ × = ( .r ‘ 𝐷 )
8		lflset.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
9		elex	⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
10		fveq2	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
11	10 3	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐷 )
12	11	fveq2d	⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = ( Base ‘ 𝐷 ) )
13	12 5	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = 𝐾 )
14		fveq2	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
15	14 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
16	13 15	oveq12d	⊢ ( 𝑤 = 𝑊 → ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↑m ( Base ‘ 𝑤 ) ) = ( 𝐾 ↑m 𝑉 ) )
17		fveq2	⊢ ( 𝑤 = 𝑊 → ( +g ‘ 𝑤 ) = ( +g ‘ 𝑊 ) )
18	17 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( +g ‘ 𝑤 ) = + )
19		fveq2	⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
20	19 4	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = · )
21	20	oveqd	⊢ ( 𝑤 = 𝑊 → ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) = ( 𝑟 · 𝑥 ) )
22		eqidd	⊢ ( 𝑤 = 𝑊 → 𝑦 = 𝑦 )
23	18 21 22	oveq123d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) = ( ( 𝑟 · 𝑥 ) + 𝑦 ) )
24	23	fveq2d	⊢ ( 𝑤 = 𝑊 → ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) )
25	11	fveq2d	⊢ ( 𝑤 = 𝑊 → ( +g ‘ ( Scalar ‘ 𝑤 ) ) = ( +g ‘ 𝐷 ) )
26	25 6	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( +g ‘ ( Scalar ‘ 𝑤 ) ) = ⨣ )
27	11	fveq2d	⊢ ( 𝑤 = 𝑊 → ( .r ‘ ( Scalar ‘ 𝑤 ) ) = ( .r ‘ 𝐷 ) )
28	27 7	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( .r ‘ ( Scalar ‘ 𝑤 ) ) = × )
29	28	oveqd	⊢ ( 𝑤 = 𝑊 → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) = ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) )
30		eqidd	⊢ ( 𝑤 = 𝑊 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
31	26 29 30	oveq123d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) )
32	24 31	eqeq12d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
33	15 32	raleqbidv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
34	15 33	raleqbidv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
35	13 34	raleqbidv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
36	16 35	rabeqbidv	⊢ ( 𝑤 = 𝑊 → { 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↑m ( Base ‘ 𝑤 ) ) ∣ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) } = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } )
37		df-lfl	⊢ LFnl = ( 𝑤 ∈ V ↦ { 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ↑m ( Base ‘ 𝑤 ) ) ∣ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( 𝑓 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ( +g ‘ 𝑤 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑤 ) ) ( 𝑓 ‘ 𝑦 ) ) } )
38		ovex	⊢ ( 𝐾 ↑m 𝑉 ) ∈ V
39	38	rabex	⊢ { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } ∈ V
40	36 37 39	fvmpt	⊢ ( 𝑊 ∈ V → ( LFnl ‘ 𝑊 ) = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } )
41	8 40	eqtrid	⊢ ( 𝑊 ∈ V → 𝐹 = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } )
42	9 41	syl	⊢ ( 𝑊 ∈ 𝑋 → 𝐹 = { 𝑓 ∈ ( 𝐾 ↑m 𝑉 ) ∣ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓 ‘ 𝑥 ) ) ⨣ ( 𝑓 ‘ 𝑦 ) ) } )