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 ⊢ D = Scalar ⁡ W
lfl0.o ⊢ 0 ˙ = 0 D
lfl0.z ⊢ Z = 0 W
lfl0.f ⊢ F = LFnl ⁡ W
Assertion lfl0 ⊢ W ∈ LMod ∧ G ∈ F → G ⁡ Z = 0 ˙

Proof

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