Metamath Proof Explorer


Theorem lfl0f

Description: The zero function is a functional. (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lfl0f.d 𝐷 = ( Scalar ‘ 𝑊 )
lfl0f.o 0 = ( 0g𝐷 )
lfl0f.v 𝑉 = ( Base ‘ 𝑊 )
lfl0f.f 𝐹 = ( LFnl ‘ 𝑊 )
Assertion lfl0f ( 𝑊 ∈ LMod → ( 𝑉 × { 0 } ) ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 lfl0f.d 𝐷 = ( Scalar ‘ 𝑊 )
2 lfl0f.o 0 = ( 0g𝐷 )
3 lfl0f.v 𝑉 = ( Base ‘ 𝑊 )
4 lfl0f.f 𝐹 = ( LFnl ‘ 𝑊 )
5 2 fvexi 0 ∈ V
6 5 fconst ( 𝑉 × { 0 } ) : 𝑉 ⟶ { 0 }
7 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8 1 7 2 lmod0cl ( 𝑊 ∈ LMod → 0 ∈ ( Base ‘ 𝐷 ) )
9 8 snssd ( 𝑊 ∈ LMod → { 0 } ⊆ ( Base ‘ 𝐷 ) )
10 fss ( ( ( 𝑉 × { 0 } ) : 𝑉 ⟶ { 0 } ∧ { 0 } ⊆ ( Base ‘ 𝐷 ) ) → ( 𝑉 × { 0 } ) : 𝑉 ⟶ ( Base ‘ 𝐷 ) )
11 6 9 10 sylancr ( 𝑊 ∈ LMod → ( 𝑉 × { 0 } ) : 𝑉 ⟶ ( Base ‘ 𝐷 ) )
12 1 lmodring ( 𝑊 ∈ LMod → 𝐷 ∈ Ring )
13 12 ad2antrr ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → 𝐷 ∈ Ring )
14 simplrl ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → 𝑟 ∈ ( Base ‘ 𝐷 ) )
15 eqid ( .r𝐷 ) = ( .r𝐷 )
16 7 15 2 ringrz ( ( 𝐷 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑟 ( .r𝐷 ) 0 ) = 0 )
17 13 14 16 syl2anc ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( 𝑟 ( .r𝐷 ) 0 ) = 0 )
18 17 oveq1d ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( ( 𝑟 ( .r𝐷 ) 0 ) ( +g𝐷 ) 0 ) = ( 0 ( +g𝐷 ) 0 ) )
19 ringgrp ( 𝐷 ∈ Ring → 𝐷 ∈ Grp )
20 13 19 syl ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → 𝐷 ∈ Grp )
21 7 2 grpidcl ( 𝐷 ∈ Grp → 0 ∈ ( Base ‘ 𝐷 ) )
22 eqid ( +g𝐷 ) = ( +g𝐷 )
23 7 22 2 grplid ( ( 𝐷 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝐷 ) ) → ( 0 ( +g𝐷 ) 0 ) = 0 )
24 20 21 23 syl2anc2 ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( 0 ( +g𝐷 ) 0 ) = 0 )
25 18 24 eqtrd ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( ( 𝑟 ( .r𝐷 ) 0 ) ( +g𝐷 ) 0 ) = 0 )
26 simplrr ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → 𝑥𝑉 )
27 5 fvconst2 ( 𝑥𝑉 → ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) = 0 )
28 26 27 syl ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) = 0 )
29 28 oveq2d ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( 𝑟 ( .r𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) ) = ( 𝑟 ( .r𝐷 ) 0 ) )
30 5 fvconst2 ( 𝑦𝑉 → ( ( 𝑉 × { 0 } ) ‘ 𝑦 ) = 0 )
31 30 adantl ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( ( 𝑉 × { 0 } ) ‘ 𝑦 ) = 0 )
32 29 31 oveq12d ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( ( 𝑟 ( .r𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) ) ( +g𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑦 ) ) = ( ( 𝑟 ( .r𝐷 ) 0 ) ( +g𝐷 ) 0 ) )
33 simpll ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → 𝑊 ∈ LMod )
34 eqid ( ·𝑠𝑊 ) = ( ·𝑠𝑊 )
35 3 1 34 7 lmodvscl ( ( 𝑊 ∈ LMod ∧ 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) → ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ∈ 𝑉 )
36 33 14 26 35 syl3anc ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ∈ 𝑉 )
37 simpr ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → 𝑦𝑉 )
38 eqid ( +g𝑊 ) = ( +g𝑊 )
39 3 38 lmodvacl ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ∈ 𝑉𝑦𝑉 ) → ( ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ( +g𝑊 ) 𝑦 ) ∈ 𝑉 )
40 33 36 37 39 syl3anc ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ( +g𝑊 ) 𝑦 ) ∈ 𝑉 )
41 5 fvconst2 ( ( ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ( +g𝑊 ) 𝑦 ) ∈ 𝑉 → ( ( 𝑉 × { 0 } ) ‘ ( ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ( +g𝑊 ) 𝑦 ) ) = 0 )
42 40 41 syl ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( ( 𝑉 × { 0 } ) ‘ ( ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ( +g𝑊 ) 𝑦 ) ) = 0 )
43 25 32 42 3eqtr4rd ( ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) ∧ 𝑦𝑉 ) → ( ( 𝑉 × { 0 } ) ‘ ( ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ( +g𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) ) ( +g𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑦 ) ) )
44 43 ralrimiva ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ∈ ( Base ‘ 𝐷 ) ∧ 𝑥𝑉 ) ) → ∀ 𝑦𝑉 ( ( 𝑉 × { 0 } ) ‘ ( ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ( +g𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) ) ( +g𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑦 ) ) )
45 44 ralrimivva ( 𝑊 ∈ LMod → ∀ 𝑟 ∈ ( Base ‘ 𝐷 ) ∀ 𝑥𝑉𝑦𝑉 ( ( 𝑉 × { 0 } ) ‘ ( ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ( +g𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) ) ( +g𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑦 ) ) )
46 3 38 1 34 7 22 15 4 islfl ( 𝑊 ∈ LMod → ( ( 𝑉 × { 0 } ) ∈ 𝐹 ↔ ( ( 𝑉 × { 0 } ) : 𝑉 ⟶ ( Base ‘ 𝐷 ) ∧ ∀ 𝑟 ∈ ( Base ‘ 𝐷 ) ∀ 𝑥𝑉𝑦𝑉 ( ( 𝑉 × { 0 } ) ‘ ( ( 𝑟 ( ·𝑠𝑊 ) 𝑥 ) ( +g𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑥 ) ) ( +g𝐷 ) ( ( 𝑉 × { 0 } ) ‘ 𝑦 ) ) ) ) )
47 11 45 46 mpbir2and ( 𝑊 ∈ LMod → ( 𝑉 × { 0 } ) ∈ 𝐹 )