islfld

Description: Properties that determine a linear functional. TODO: use this in place of islfl when it shortens the proof. (Contributed by NM, 19-Oct-2014)

	Ref	Expression
Hypotheses	islfld.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
	islfld.a	⊢ ( 𝜑 → + = ( +_g ‘ 𝑊 ) )
	islfld.d	⊢ ( 𝜑 → 𝐷 = ( Scalar ‘ 𝑊 ) )
	islfld.s	⊢ ( 𝜑 → · = ( ·_𝑠 ‘ 𝑊 ) )
	islfld.k	⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝐷 ) )
	islfld.p	⊢ ( 𝜑 → ⨣ = ( +_g ‘ 𝐷 ) )
	islfld.t	⊢ ( 𝜑 → × = ( ._r ‘ 𝐷 ) )
	islfld.f	⊢ ( 𝜑 → 𝐹 = ( LFnl ‘ 𝑊 ) )
	islfld.u	⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
	islfld.l	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) )
	islfld.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
Assertion	islfld	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		islfld.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
2		islfld.a	⊢ ( 𝜑 → + = ( +_g ‘ 𝑊 ) )
3		islfld.d	⊢ ( 𝜑 → 𝐷 = ( Scalar ‘ 𝑊 ) )
4		islfld.s	⊢ ( 𝜑 → · = ( ·_𝑠 ‘ 𝑊 ) )
5		islfld.k	⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝐷 ) )
6		islfld.p	⊢ ( 𝜑 → ⨣ = ( +_g ‘ 𝐷 ) )
7		islfld.t	⊢ ( 𝜑 → × = ( ._r ‘ 𝐷 ) )
8		islfld.f	⊢ ( 𝜑 → 𝐹 = ( LFnl ‘ 𝑊 ) )
9		islfld.u	⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
10		islfld.l	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) )
11		islfld.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
12	3	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
13	5 12	eqtrd	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
14	1 13	feq23d	⊢ ( 𝜑 → ( 𝐺 : 𝑉 ⟶ 𝐾 ↔ 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
15	9 14	mpbid	⊢ ( 𝜑 → 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
16	10	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) )
17	4	oveqd	⊢ ( 𝜑 → ( 𝑟 · 𝑥 ) = ( 𝑟 ( ·_𝑠 ‘ 𝑊 ) 𝑥 ) )
18		eqidd	⊢ ( 𝜑 → 𝑦 = 𝑦 )
19	2 17 18	oveq123d	⊢ ( 𝜑 → ( ( 𝑟 · 𝑥 ) + 𝑦 ) = ( ( 𝑟 ( ·_𝑠 ‘ 𝑊 ) 𝑥 ) ( +_g ‘ 𝑊 ) 𝑦 ) )
20	19	fveq2d	⊢ ( 𝜑 → ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑟 ( ·_𝑠 ‘ 𝑊 ) 𝑥 ) ( +_g ‘ 𝑊 ) 𝑦 ) ) )
21	3	fveq2d	⊢ ( 𝜑 → ( +_g ‘ 𝐷 ) = ( +_g ‘ ( Scalar ‘ 𝑊 ) ) )
22	6 21	eqtrd	⊢ ( 𝜑 → ⨣ = ( +_g ‘ ( Scalar ‘ 𝑊 ) ) )
23	3	fveq2d	⊢ ( 𝜑 → ( ._r ‘ 𝐷 ) = ( ._r ‘ ( Scalar ‘ 𝑊 ) ) )
24	7 23	eqtrd	⊢ ( 𝜑 → × = ( ._r ‘ ( Scalar ‘ 𝑊 ) ) )
25	24	oveqd	⊢ ( 𝜑 → ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) = ( 𝑟 ( ._r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) )
26		eqidd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
27	22 25 26	oveq123d	⊢ ( 𝜑 → ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝑟 ( ._r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +_g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) )
28	20 27	eqeq12d	⊢ ( 𝜑 → ( ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ ( ( 𝑟 ( ·_𝑠 ‘ 𝑊 ) 𝑥 ) ( +_g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( ._r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +_g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) )
29	1 28	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·_𝑠 ‘ 𝑊 ) 𝑥 ) ( +_g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( ._r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +_g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) )
30	1 29	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·_𝑠 ‘ 𝑊 ) 𝑥 ) ( +_g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( ._r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +_g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) )
31	13 30	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·_𝑠 ‘ 𝑊 ) 𝑥 ) ( +_g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( ._r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +_g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) )
32	16 31	mpbid	⊢ ( 𝜑 → ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·_𝑠 ‘ 𝑊 ) 𝑥 ) ( +_g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( ._r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +_g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) )
33		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
34		eqid	⊢ ( +_g ‘ 𝑊 ) = ( +_g ‘ 𝑊 )
35		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
36		eqid	⊢ ( ·_𝑠 ‘ 𝑊 ) = ( ·_𝑠 ‘ 𝑊 )
37		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
38		eqid	⊢ ( +_g ‘ ( Scalar ‘ 𝑊 ) ) = ( +_g ‘ ( Scalar ‘ 𝑊 ) )
39		eqid	⊢ ( ._r ‘ ( Scalar ‘ 𝑊 ) ) = ( ._r ‘ ( Scalar ‘ 𝑊 ) )
40		eqid	⊢ ( LFnl ‘ 𝑊 ) = ( LFnl ‘ 𝑊 )
41	33 34 35 36 37 38 39 40	islfl	⊢ ( 𝑊 ∈ 𝑋 → ( 𝐺 ∈ ( LFnl ‘ 𝑊 ) ↔ ( 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·_𝑠 ‘ 𝑊 ) 𝑥 ) ( +_g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( ._r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +_g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) ) )
42	41	biimpar	⊢ ( ( 𝑊 ∈ 𝑋 ∧ ( 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·_𝑠 ‘ 𝑊 ) 𝑥 ) ( +_g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( ._r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +_g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) ) → 𝐺 ∈ ( LFnl ‘ 𝑊 ) )
43	11 15 32 42	syl12anc	⊢ ( 𝜑 → 𝐺 ∈ ( LFnl ‘ 𝑊 ) )
44	43 8	eleqtrrd	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )

Metamath Proof Explorer

Theorem islfld

Proof