Step | Hyp | Ref
| Expression |
1 | | eqid 2770 |
. . . 4
⊢
(Base‘𝑊) =
(Base‘𝑊) |
2 | | eqid 2770 |
. . . 4
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
3 | | eqid 2770 |
. . . 4
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
4 | | lkrlss.f |
. . . 4
⊢ 𝐹 = (LFnl‘𝑊) |
5 | | lkrlss.k |
. . . 4
⊢ 𝐾 = (LKer‘𝑊) |
6 | 1, 2, 3, 4, 5 | lkrval2 34892 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = {𝑥 ∈ (Base‘𝑊) ∣ (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))}) |
7 | | ssrab2 3834 |
. . 3
⊢ {𝑥 ∈ (Base‘𝑊) ∣ (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))} ⊆ (Base‘𝑊) |
8 | 6, 7 | syl6eqss 3802 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ⊆ (Base‘𝑊)) |
9 | | eqid 2770 |
. . . . . 6
⊢
(0g‘𝑊) = (0g‘𝑊) |
10 | 1, 9 | lmod0vcl 19101 |
. . . . 5
⊢ (𝑊 ∈ LMod →
(0g‘𝑊)
∈ (Base‘𝑊)) |
11 | 10 | adantr 466 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (0g‘𝑊) ∈ (Base‘𝑊)) |
12 | 2, 3, 9, 4 | lfl0 34867 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘(0g‘𝑊)) =
(0g‘(Scalar‘𝑊))) |
13 | 1, 2, 3, 4, 5 | ellkr 34891 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((0g‘𝑊) ∈ (𝐾‘𝐺) ↔ ((0g‘𝑊) ∈ (Base‘𝑊) ∧ (𝐺‘(0g‘𝑊)) =
(0g‘(Scalar‘𝑊))))) |
14 | 11, 12, 13 | mpbir2and 684 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (0g‘𝑊) ∈ (𝐾‘𝐺)) |
15 | | ne0i 4067 |
. . 3
⊢
((0g‘𝑊) ∈ (𝐾‘𝐺) → (𝐾‘𝐺) ≠ ∅) |
16 | 14, 15 | syl 17 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ≠ ∅) |
17 | | simplll 750 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑊 ∈ LMod) |
18 | | simplr 744 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) |
19 | | simpllr 752 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝐺 ∈ 𝐹) |
20 | | simprl 746 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑥 ∈ (𝐾‘𝐺)) |
21 | 1, 4, 5 | lkrcl 34894 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ (𝐾‘𝐺)) → 𝑥 ∈ (Base‘𝑊)) |
22 | 17, 19, 20, 21 | syl3anc 1475 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑥 ∈ (Base‘𝑊)) |
23 | | eqid 2770 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
24 | | eqid 2770 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
25 | 1, 2, 23, 24 | lmodvscl 19089 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
26 | 17, 18, 22, 25 | syl3anc 1475 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
27 | | simprr 748 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑦 ∈ (𝐾‘𝐺)) |
28 | 1, 4, 5 | lkrcl 34894 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ (𝐾‘𝐺)) → 𝑦 ∈ (Base‘𝑊)) |
29 | 17, 19, 27, 28 | syl3anc 1475 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑦 ∈ (Base‘𝑊)) |
30 | | eqid 2770 |
. . . . . . 7
⊢
(+g‘𝑊) = (+g‘𝑊) |
31 | 1, 30 | lmodvacl 19086 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑟(
·𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊)) |
32 | 17, 26, 29, 31 | syl3anc 1475 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊)) |
33 | | eqid 2770 |
. . . . . . . 8
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) |
34 | | eqid 2770 |
. . . . . . . 8
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
35 | 1, 30, 2, 23, 24, 33, 34, 4 | lfli 34863 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦))) |
36 | 17, 19, 18, 22, 29, 35 | syl113anc 1487 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦))) |
37 | 2, 3, 4, 5 | lkrf0 34895 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ (𝐾‘𝐺)) → (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))) |
38 | 17, 19, 20, 37 | syl3anc 1475 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))) |
39 | 38 | oveq2d 6808 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥)) = (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) |
40 | 2 | lmodring 19080 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) |
41 | 17, 40 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (Scalar‘𝑊) ∈ Ring) |
42 | 24, 34, 3 | ringrz 18795 |
. . . . . . . . 9
⊢
(((Scalar‘𝑊)
∈ Ring ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
43 | 41, 18, 42 | syl2anc 565 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
44 | 39, 43 | eqtrd 2804 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥)) = (0g‘(Scalar‘𝑊))) |
45 | 2, 3, 4, 5 | lkrf0 34895 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ (𝐾‘𝐺)) → (𝐺‘𝑦) = (0g‘(Scalar‘𝑊))) |
46 | 17, 19, 27, 45 | syl3anc 1475 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘𝑦) = (0g‘(Scalar‘𝑊))) |
47 | 44, 46 | oveq12d 6810 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦)) =
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) |
48 | 2 | lmodfgrp 19081 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) |
49 | 17, 48 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (Scalar‘𝑊) ∈ Grp) |
50 | 24, 3 | grpidcl 17657 |
. . . . . . . 8
⊢
((Scalar‘𝑊)
∈ Grp → (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) →
(0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
52 | 24, 33, 3 | grplid 17659 |
. . . . . . 7
⊢
(((Scalar‘𝑊)
∈ Grp ∧ (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
53 | 49, 51, 52 | syl2anc 565 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
54 | 36, 47, 53 | 3eqtrd 2808 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (0g‘(Scalar‘𝑊))) |
55 | 1, 2, 3, 4, 5 | ellkr 34891 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺) ↔ (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊) ∧ (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (0g‘(Scalar‘𝑊))))) |
56 | 55 | ad2antrr 697 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺) ↔ (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊) ∧ (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (0g‘(Scalar‘𝑊))))) |
57 | 32, 54, 56 | mpbir2and 684 |
. . . 4
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) |
58 | 57 | ralrimivva 3119 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) → ∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) |
59 | 58 | ralrimiva 3114 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) |
60 | | lkrlss.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑊) |
61 | 2, 24, 1, 30, 23, 60 | islss 19144 |
. 2
⊢ ((𝐾‘𝐺) ∈ 𝑆 ↔ ((𝐾‘𝐺) ⊆ (Base‘𝑊) ∧ (𝐾‘𝐺) ≠ ∅ ∧ ∀𝑟 ∈
(Base‘(Scalar‘𝑊))∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺))) |
62 | 8, 16, 59, 61 | syl3anbrc 1427 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ∈ 𝑆) |