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