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 } ) ∈ 𝐹 )