Metamath Proof Explorer

Theorem lflmul

Description: Property of a linear functional. ( lnfnmuli analog.) (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lflmul.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lflmul.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lflmul.t ⊢ × = ( .r ‘ 𝐷 )
lflmul.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lflmul.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lflmul.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
Assertion lflmul ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑅 · 𝑋 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 lflmul.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2 lflmul.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
3 lflmul.t ⊢ × = ( .r ‘ 𝐷 )
4 lflmul.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
5 lflmul.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 lflmul.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
7 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
8 simp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → 𝐺 ∈ 𝐹 )
9 simp3l ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → 𝑅 ∈ 𝐾 )
10 simp3r ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → 𝑋 ∈ 𝑉 )
11 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
12 4 11 lmod0vcl ⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
13 12 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
14 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
15 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
16 4 14 1 5 2 15 3 6 lfli ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) ) )
17 7 8 9 10 13 16 syl113anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) ) )
18 4 1 5 2 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑅 · 𝑋 ) ∈ 𝑉 )
19 7 9 10 18 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑅 · 𝑋 ) ∈ 𝑉 )
20 4 14 11 lmod0vrid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 · 𝑋 ) ∈ 𝑉 ) → ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 𝑅 · 𝑋 ) )
21 7 19 20 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 𝑅 · 𝑋 ) )
22 21 fveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ) = ( 𝐺 ‘ ( 𝑅 · 𝑋 ) ) )
23 eqid ⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
24 1 23 11 6 lfl0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝐷 ) )
25 24 3adant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝐷 ) )
26 25 oveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) ) = ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 0g ‘ 𝐷 ) ) )
27 1 lmodfgrp ⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Grp )
28 27 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → 𝐷 ∈ Grp )
29 1 2 4 6 lflcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ 𝐾 )
30 29 3adant3l ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ 𝑋 ) ∈ 𝐾 )
31 1 2 3 lmodmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑋 ) ∈ 𝐾 ) → ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐾 )
32 7 9 30 31 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐾 )
33 2 15 23 grprid ⊢ ( ( 𝐷 ∈ Grp ∧ ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐾 ) → ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 0g ‘ 𝐷 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) )
34 28 32 33 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 0g ‘ 𝐷 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) )
35 26 34 eqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) )
36 17 22 35 3eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑅 · 𝑋 ) ) = ( 𝑅 × ( 𝐺 ‘ 𝑋 ) ) )