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 ∧ 𝐺𝐹 ∧ ( 𝑅𝐾𝑋𝑉 ) ) → ( 𝐺 ‘ ( 𝑅 · 𝑋 ) ) = ( 𝑅 × ( 𝐺𝑋 ) ) )