Proof of Theorem lfl0
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → 𝑊 ∈ LMod) |
2 | | simpr 488 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → 𝐺 ∈ 𝐹) |
3 | | lfl0.d |
. . . . . . 7
⊢ 𝐷 = (Scalar‘𝑊) |
4 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝐷) =
(Base‘𝐷) |
5 | | eqid 2737 |
. . . . . . 7
⊢
(1r‘𝐷) = (1r‘𝐷) |
6 | 3, 4, 5 | lmod1cl 19926 |
. . . . . 6
⊢ (𝑊 ∈ LMod →
(1r‘𝐷)
∈ (Base‘𝐷)) |
7 | 6 | adantr 484 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (1r‘𝐷) ∈ (Base‘𝐷)) |
8 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑊) =
(Base‘𝑊) |
9 | | lfl0.z |
. . . . . . 7
⊢ 𝑍 = (0g‘𝑊) |
10 | 8, 9 | lmod0vcl 19928 |
. . . . . 6
⊢ (𝑊 ∈ LMod → 𝑍 ∈ (Base‘𝑊)) |
11 | 10 | adantr 484 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → 𝑍 ∈ (Base‘𝑊)) |
12 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑊) = (+g‘𝑊) |
13 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
14 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝐷) = (+g‘𝐷) |
15 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝐷) = (.r‘𝐷) |
16 | | lfl0.f |
. . . . . 6
⊢ 𝐹 = (LFnl‘𝑊) |
17 | 8, 12, 3, 13, 4, 14, 15, 16 | lfli 36812 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ((1r‘𝐷) ∈ (Base‘𝐷) ∧ 𝑍 ∈ (Base‘𝑊) ∧ 𝑍 ∈ (Base‘𝑊))) → (𝐺‘(((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍)(+g‘𝑊)𝑍)) = (((1r‘𝐷)(.r‘𝐷)(𝐺‘𝑍))(+g‘𝐷)(𝐺‘𝑍))) |
18 | 1, 2, 7, 11, 11, 17 | syl113anc 1384 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘(((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍)(+g‘𝑊)𝑍)) = (((1r‘𝐷)(.r‘𝐷)(𝐺‘𝑍))(+g‘𝐷)(𝐺‘𝑍))) |
19 | 8, 3, 13, 4 | lmodvscl 19916 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧
(1r‘𝐷)
∈ (Base‘𝐷) ∧
𝑍 ∈ (Base‘𝑊)) →
((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍) ∈ (Base‘𝑊)) |
20 | 1, 7, 11, 19 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍) ∈ (Base‘𝑊)) |
21 | 8, 12, 9 | lmod0vrid 19930 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧
((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍) ∈ (Base‘𝑊)) → (((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍)(+g‘𝑊)𝑍) = ((1r‘𝐷)( ·𝑠
‘𝑊)𝑍)) |
22 | 20, 21 | syldan 594 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍)(+g‘𝑊)𝑍) = ((1r‘𝐷)( ·𝑠
‘𝑊)𝑍)) |
23 | 8, 3, 13, 5 | lmodvs1 19927 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ (Base‘𝑊)) →
((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍) = 𝑍) |
24 | 11, 23 | syldan 594 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍) = 𝑍) |
25 | 22, 24 | eqtrd 2777 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍)(+g‘𝑊)𝑍) = 𝑍) |
26 | 25 | fveq2d 6721 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘(((1r‘𝐷)(
·𝑠 ‘𝑊)𝑍)(+g‘𝑊)𝑍)) = (𝐺‘𝑍)) |
27 | 3 | lmodring 19907 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → 𝐷 ∈ Ring) |
28 | 27 | adantr 484 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → 𝐷 ∈ Ring) |
29 | 3, 4, 8, 16 | lflcl 36815 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑍 ∈ (Base‘𝑊)) → (𝐺‘𝑍) ∈ (Base‘𝐷)) |
30 | 11, 29 | mpd3an3 1464 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘𝑍) ∈ (Base‘𝐷)) |
31 | 4, 15, 5 | ringlidm 19589 |
. . . . . 6
⊢ ((𝐷 ∈ Ring ∧ (𝐺‘𝑍) ∈ (Base‘𝐷)) → ((1r‘𝐷)(.r‘𝐷)(𝐺‘𝑍)) = (𝐺‘𝑍)) |
32 | 28, 30, 31 | syl2anc 587 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((1r‘𝐷)(.r‘𝐷)(𝐺‘𝑍)) = (𝐺‘𝑍)) |
33 | 32 | oveq1d 7228 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (((1r‘𝐷)(.r‘𝐷)(𝐺‘𝑍))(+g‘𝐷)(𝐺‘𝑍)) = ((𝐺‘𝑍)(+g‘𝐷)(𝐺‘𝑍))) |
34 | 18, 26, 33 | 3eqtr3d 2785 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘𝑍) = ((𝐺‘𝑍)(+g‘𝐷)(𝐺‘𝑍))) |
35 | 34 | oveq1d 7228 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐺‘𝑍)(-g‘𝐷)(𝐺‘𝑍)) = (((𝐺‘𝑍)(+g‘𝐷)(𝐺‘𝑍))(-g‘𝐷)(𝐺‘𝑍))) |
36 | | ringgrp 19567 |
. . . 4
⊢ (𝐷 ∈ Ring → 𝐷 ∈ Grp) |
37 | 28, 36 | syl 17 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → 𝐷 ∈ Grp) |
38 | | lfl0.o |
. . . 4
⊢ 0 =
(0g‘𝐷) |
39 | | eqid 2737 |
. . . 4
⊢
(-g‘𝐷) = (-g‘𝐷) |
40 | 4, 38, 39 | grpsubid 18447 |
. . 3
⊢ ((𝐷 ∈ Grp ∧ (𝐺‘𝑍) ∈ (Base‘𝐷)) → ((𝐺‘𝑍)(-g‘𝐷)(𝐺‘𝑍)) = 0 ) |
41 | 37, 30, 40 | syl2anc 587 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐺‘𝑍)(-g‘𝐷)(𝐺‘𝑍)) = 0 ) |
42 | 4, 14, 39 | grppncan 18454 |
. . 3
⊢ ((𝐷 ∈ Grp ∧ (𝐺‘𝑍) ∈ (Base‘𝐷) ∧ (𝐺‘𝑍) ∈ (Base‘𝐷)) → (((𝐺‘𝑍)(+g‘𝐷)(𝐺‘𝑍))(-g‘𝐷)(𝐺‘𝑍)) = (𝐺‘𝑍)) |
43 | 37, 30, 30, 42 | syl3anc 1373 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (((𝐺‘𝑍)(+g‘𝐷)(𝐺‘𝑍))(-g‘𝐷)(𝐺‘𝑍)) = (𝐺‘𝑍)) |
44 | 35, 41, 43 | 3eqtr3rd 2786 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘𝑍) = 0 ) |