Metamath Proof Explorer


Theorem lfl0

Description: A linear functional is zero at the zero vector. ( lnfn0i analog.) (Contributed by NM, 16-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses lfl0.d 𝐷 = ( Scalar ‘ 𝑊 )
lfl0.o 0 = ( 0g𝐷 )
lfl0.z 𝑍 = ( 0g𝑊 )
lfl0.f 𝐹 = ( LFnl ‘ 𝑊 )
Assertion lfl0 ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 𝐺𝑍 ) = 0 )

Proof

Step Hyp Ref Expression
1 lfl0.d 𝐷 = ( Scalar ‘ 𝑊 )
2 lfl0.o 0 = ( 0g𝐷 )
3 lfl0.z 𝑍 = ( 0g𝑊 )
4 lfl0.f 𝐹 = ( LFnl ‘ 𝑊 )
5 simpl ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → 𝑊 ∈ LMod )
6 simpr ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → 𝐺𝐹 )
7 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8 eqid ( 1r𝐷 ) = ( 1r𝐷 )
9 1 7 8 lmod1cl ( 𝑊 ∈ LMod → ( 1r𝐷 ) ∈ ( Base ‘ 𝐷 ) )
10 9 adantr ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 1r𝐷 ) ∈ ( Base ‘ 𝐷 ) )
11 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12 11 3 lmod0vcl ( 𝑊 ∈ LMod → 𝑍 ∈ ( Base ‘ 𝑊 ) )
13 12 adantr ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → 𝑍 ∈ ( Base ‘ 𝑊 ) )
14 eqid ( +g𝑊 ) = ( +g𝑊 )
15 eqid ( ·𝑠𝑊 ) = ( ·𝑠𝑊 )
16 eqid ( +g𝐷 ) = ( +g𝐷 )
17 eqid ( .r𝐷 ) = ( .r𝐷 )
18 11 14 1 15 7 16 17 4 lfli ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ∧ ( ( 1r𝐷 ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑍 ∈ ( Base ‘ 𝑊 ) ∧ 𝑍 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝐺 ‘ ( ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) ( +g𝑊 ) 𝑍 ) ) = ( ( ( 1r𝐷 ) ( .r𝐷 ) ( 𝐺𝑍 ) ) ( +g𝐷 ) ( 𝐺𝑍 ) ) )
19 5 6 10 13 13 18 syl113anc ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 𝐺 ‘ ( ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) ( +g𝑊 ) 𝑍 ) ) = ( ( ( 1r𝐷 ) ( .r𝐷 ) ( 𝐺𝑍 ) ) ( +g𝐷 ) ( 𝐺𝑍 ) ) )
20 11 1 15 7 lmodvscl ( ( 𝑊 ∈ LMod ∧ ( 1r𝐷 ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑍 ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) ∈ ( Base ‘ 𝑊 ) )
21 5 10 13 20 syl3anc ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) ∈ ( Base ‘ 𝑊 ) )
22 11 14 3 lmod0vrid ( ( 𝑊 ∈ LMod ∧ ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) ( +g𝑊 ) 𝑍 ) = ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) )
23 21 22 syldan ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) ( +g𝑊 ) 𝑍 ) = ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) )
24 11 1 15 8 lmodvs1 ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) = 𝑍 )
25 13 24 syldan ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) = 𝑍 )
26 23 25 eqtrd ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) ( +g𝑊 ) 𝑍 ) = 𝑍 )
27 26 fveq2d ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 𝐺 ‘ ( ( ( 1r𝐷 ) ( ·𝑠𝑊 ) 𝑍 ) ( +g𝑊 ) 𝑍 ) ) = ( 𝐺𝑍 ) )
28 1 lmodring ( 𝑊 ∈ LMod → 𝐷 ∈ Ring )
29 28 adantr ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → 𝐷 ∈ Ring )
30 1 7 11 4 lflcl ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹𝑍 ∈ ( Base ‘ 𝑊 ) ) → ( 𝐺𝑍 ) ∈ ( Base ‘ 𝐷 ) )
31 13 30 mpd3an3 ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 𝐺𝑍 ) ∈ ( Base ‘ 𝐷 ) )
32 7 17 8 ringlidm ( ( 𝐷 ∈ Ring ∧ ( 𝐺𝑍 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 1r𝐷 ) ( .r𝐷 ) ( 𝐺𝑍 ) ) = ( 𝐺𝑍 ) )
33 29 31 32 syl2anc ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( 1r𝐷 ) ( .r𝐷 ) ( 𝐺𝑍 ) ) = ( 𝐺𝑍 ) )
34 33 oveq1d ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( ( 1r𝐷 ) ( .r𝐷 ) ( 𝐺𝑍 ) ) ( +g𝐷 ) ( 𝐺𝑍 ) ) = ( ( 𝐺𝑍 ) ( +g𝐷 ) ( 𝐺𝑍 ) ) )
35 19 27 34 3eqtr3d ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 𝐺𝑍 ) = ( ( 𝐺𝑍 ) ( +g𝐷 ) ( 𝐺𝑍 ) ) )
36 35 oveq1d ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( 𝐺𝑍 ) ( -g𝐷 ) ( 𝐺𝑍 ) ) = ( ( ( 𝐺𝑍 ) ( +g𝐷 ) ( 𝐺𝑍 ) ) ( -g𝐷 ) ( 𝐺𝑍 ) ) )
37 ringgrp ( 𝐷 ∈ Ring → 𝐷 ∈ Grp )
38 29 37 syl ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → 𝐷 ∈ Grp )
39 eqid ( -g𝐷 ) = ( -g𝐷 )
40 7 2 39 grpsubid ( ( 𝐷 ∈ Grp ∧ ( 𝐺𝑍 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝐺𝑍 ) ( -g𝐷 ) ( 𝐺𝑍 ) ) = 0 )
41 38 31 40 syl2anc ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( 𝐺𝑍 ) ( -g𝐷 ) ( 𝐺𝑍 ) ) = 0 )
42 7 16 39 grppncan ( ( 𝐷 ∈ Grp ∧ ( 𝐺𝑍 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺𝑍 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( ( 𝐺𝑍 ) ( +g𝐷 ) ( 𝐺𝑍 ) ) ( -g𝐷 ) ( 𝐺𝑍 ) ) = ( 𝐺𝑍 ) )
43 38 31 31 42 syl3anc ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( ( 𝐺𝑍 ) ( +g𝐷 ) ( 𝐺𝑍 ) ) ( -g𝐷 ) ( 𝐺𝑍 ) ) = ( 𝐺𝑍 ) )
44 36 41 43 3eqtr3rd ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 𝐺𝑍 ) = 0 )