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 )