Metamath Proof Explorer

Theorem lfli

Description: Property of a linear functional. ( lnfnli analog.) (Contributed by NM, 16-Apr-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 lfli ( ( 𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) )

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 1 2 3 4 5 6 7 8 islfl ⊢ ( 𝑊 ∈ 𝑍 → ( 𝐺 ∈ 𝐹 ↔ ( 𝐺 : 𝑉 ⟶ 𝐾 ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) )
10 9 simplbda ⊢ ( ( 𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ) → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) )
11 10 3adant3 ⊢ ( ( 𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) )
12 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 · 𝑥 ) = ( 𝑅 · 𝑥 ) )
13 12 fvoveq1d ⊢ ( 𝑟 = 𝑅 → ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑅 · 𝑥 ) + 𝑦 ) ) )
14 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) )
15 14 oveq1d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) )
16 13 15 eqeq12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ ( ( 𝑅 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) )
17 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑅 · 𝑥 ) = ( 𝑅 · 𝑋 ) )
18 17 fvoveq1d ⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ ( ( 𝑅 · 𝑥 ) + 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑦 ) ) )
19 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑋 ) )
20 19 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) )
21 20 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) )
22 18 21 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐺 ‘ ( ( 𝑅 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) )
23 oveq2 ⊢ ( 𝑦 = 𝑌 → ( ( 𝑅 · 𝑋 ) + 𝑦 ) = ( ( 𝑅 · 𝑋 ) + 𝑌 ) )
24 23 fveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) )
25 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑌 ) )
26 25 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) )
27 24 26 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑦 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) ) )
28 16 22 27 rspc3v ⊢ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) ) )
29 28 3ad2ant3 ⊢ ( ( 𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) ) )
30 11 29 mpd ⊢ ( ( 𝑊 ∈ 𝑍 ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) + 𝑌 ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ⨣ ( 𝐺 ‘ 𝑌 ) ) )