Step | Hyp | Ref
| Expression |
1 | | lfl0f.o |
. . . . 5
⊢ 0 =
(0g‘𝐷) |
2 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝐷) ∈ V |
3 | 1, 2 | eqeltri 2684 |
. . . 4
⊢ 0 ∈
V |
4 | 3 | fconst 6004 |
. . 3
⊢ (𝑉 × { 0 }):𝑉⟶{ 0 } |
5 | | lfl0f.d |
. . . . 5
⊢ 𝐷 = (Scalar‘𝑊) |
6 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) |
7 | 5, 6, 1 | lmod0cl 18712 |
. . . 4
⊢ (𝑊 ∈ LMod → 0 ∈
(Base‘𝐷)) |
8 | 7 | snssd 4281 |
. . 3
⊢ (𝑊 ∈ LMod → { 0 } ⊆
(Base‘𝐷)) |
9 | | fss 5969 |
. . 3
⊢ (((𝑉 × { 0 }):𝑉⟶{ 0 } ∧ { 0 } ⊆
(Base‘𝐷)) →
(𝑉 × { 0 }):𝑉⟶(Base‘𝐷)) |
10 | 4, 8, 9 | sylancr 694 |
. 2
⊢ (𝑊 ∈ LMod → (𝑉 × { 0 }):𝑉⟶(Base‘𝐷)) |
11 | 5 | lmodring 18694 |
. . . . . . . . 9
⊢ (𝑊 ∈ LMod → 𝐷 ∈ Ring) |
12 | 11 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → 𝐷 ∈ Ring) |
13 | | simplrl 796 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → 𝑟 ∈ (Base‘𝐷)) |
14 | | eqid 2610 |
. . . . . . . . 9
⊢
(.r‘𝐷) = (.r‘𝐷) |
15 | 6, 14, 1 | ringrz 18411 |
. . . . . . . 8
⊢ ((𝐷 ∈ Ring ∧ 𝑟 ∈ (Base‘𝐷)) → (𝑟(.r‘𝐷) 0 ) = 0 ) |
16 | 12, 13, 15 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → (𝑟(.r‘𝐷) 0 ) = 0 ) |
17 | 16 | oveq1d 6564 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → ((𝑟(.r‘𝐷) 0
)(+g‘𝐷)
0 ) = (
0
(+g‘𝐷)
0
)) |
18 | | ringgrp 18375 |
. . . . . . . 8
⊢ (𝐷 ∈ Ring → 𝐷 ∈ Grp) |
19 | 12, 18 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → 𝐷 ∈ Grp) |
20 | 6, 1 | grpidcl 17273 |
. . . . . . . 8
⊢ (𝐷 ∈ Grp → 0 ∈
(Base‘𝐷)) |
21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → 0 ∈ (Base‘𝐷)) |
22 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝐷) = (+g‘𝐷) |
23 | 6, 22, 1 | grplid 17275 |
. . . . . . 7
⊢ ((𝐷 ∈ Grp ∧ 0 ∈
(Base‘𝐷)) → (
0
(+g‘𝐷)
0 ) =
0
) |
24 | 19, 21, 23 | syl2anc 691 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → ( 0 (+g‘𝐷) 0 ) = 0 ) |
25 | 17, 24 | eqtrd 2644 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → ((𝑟(.r‘𝐷) 0
)(+g‘𝐷)
0 ) =
0
) |
26 | | simplrr 797 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
27 | 3 | fvconst2 6374 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑉 → ((𝑉 × { 0 })‘𝑥) = 0 ) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → ((𝑉 × { 0 })‘𝑥) = 0 ) |
29 | 28 | oveq2d 6565 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → (𝑟(.r‘𝐷)((𝑉 × { 0 })‘𝑥)) = (𝑟(.r‘𝐷) 0 )) |
30 | 3 | fvconst2 6374 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑉 → ((𝑉 × { 0 })‘𝑦) = 0 ) |
31 | 30 | adantl 481 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → ((𝑉 × { 0 })‘𝑦) = 0 ) |
32 | 29, 31 | oveq12d 6567 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → ((𝑟(.r‘𝐷)((𝑉 × { 0 })‘𝑥))(+g‘𝐷)((𝑉 × { 0 })‘𝑦)) = ((𝑟(.r‘𝐷) 0
)(+g‘𝐷)
0
)) |
33 | | simpll 786 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → 𝑊 ∈ LMod) |
34 | | lfl0f.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
35 | | eqid 2610 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
36 | 34, 5, 35, 6 | lmodvscl 18703 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ 𝑉) |
37 | 33, 13, 26, 36 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ 𝑉) |
38 | | simpr 476 |
. . . . . . 7
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
39 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝑊) = (+g‘𝑊) |
40 | 34, 39 | lmodvacl 18700 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ (𝑟(
·𝑠 ‘𝑊)𝑥) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ 𝑉) |
41 | 33, 37, 38, 40 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ 𝑉) |
42 | 3 | fvconst2 6374 |
. . . . . 6
⊢ (((𝑟(
·𝑠 ‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ 𝑉 → ((𝑉 × { 0 })‘((𝑟(
·𝑠 ‘𝑊)𝑥)(+g‘𝑊)𝑦)) = 0 ) |
43 | 41, 42 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → ((𝑉 × { 0 })‘((𝑟(
·𝑠 ‘𝑊)𝑥)(+g‘𝑊)𝑦)) = 0 ) |
44 | 25, 32, 43 | 3eqtr4rd 2655 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) ∧ 𝑦 ∈ 𝑉) → ((𝑉 × { 0 })‘((𝑟(
·𝑠 ‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘𝐷)((𝑉 × { 0 })‘𝑥))(+g‘𝐷)((𝑉 × { 0 })‘𝑦))) |
45 | 44 | ralrimiva 2949 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ (𝑟 ∈ (Base‘𝐷) ∧ 𝑥 ∈ 𝑉)) → ∀𝑦 ∈ 𝑉 ((𝑉 × { 0 })‘((𝑟(
·𝑠 ‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘𝐷)((𝑉 × { 0 })‘𝑥))(+g‘𝐷)((𝑉 × { 0 })‘𝑦))) |
46 | 45 | ralrimivva 2954 |
. 2
⊢ (𝑊 ∈ LMod →
∀𝑟 ∈
(Base‘𝐷)∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((𝑉 × { 0 })‘((𝑟(
·𝑠 ‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘𝐷)((𝑉 × { 0 })‘𝑥))(+g‘𝐷)((𝑉 × { 0 })‘𝑦))) |
47 | | lfl0f.f |
. . 3
⊢ 𝐹 = (LFnl‘𝑊) |
48 | 34, 39, 5, 35, 6, 22, 14, 47 | islfl 33365 |
. 2
⊢ (𝑊 ∈ LMod → ((𝑉 × { 0 }) ∈ 𝐹 ↔ ((𝑉 × { 0 }):𝑉⟶(Base‘𝐷) ∧ ∀𝑟 ∈ (Base‘𝐷)∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ((𝑉 × { 0 })‘((𝑟(
·𝑠 ‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘𝐷)((𝑉 × { 0 })‘𝑥))(+g‘𝐷)((𝑉 × { 0 })‘𝑦))))) |
49 | 10, 46, 48 | mpbir2and 959 |
1
⊢ (𝑊 ∈ LMod → (𝑉 × { 0 }) ∈ 𝐹) |