Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑊) =
(Base‘𝑊) |
2 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
3 | | eqid 2737 |
. . . 4
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
4 | | lkrlss.f |
. . . 4
⊢ 𝐹 = (LFnl‘𝑊) |
5 | | lkrlss.k |
. . . 4
⊢ 𝐾 = (LKer‘𝑊) |
6 | 1, 2, 3, 4, 5 | lkrval2 36841 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = {𝑥 ∈ (Base‘𝑊) ∣ (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))}) |
7 | | ssrab2 3993 |
. . 3
⊢ {𝑥 ∈ (Base‘𝑊) ∣ (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))} ⊆ (Base‘𝑊) |
8 | 6, 7 | eqsstrdi 3955 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ⊆ (Base‘𝑊)) |
9 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑊) = (0g‘𝑊) |
10 | 1, 9 | lmod0vcl 19928 |
. . . . 5
⊢ (𝑊 ∈ LMod →
(0g‘𝑊)
∈ (Base‘𝑊)) |
11 | 10 | adantr 484 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (0g‘𝑊) ∈ (Base‘𝑊)) |
12 | 2, 3, 9, 4 | lfl0 36816 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘(0g‘𝑊)) =
(0g‘(Scalar‘𝑊))) |
13 | 1, 2, 3, 4, 5 | ellkr 36840 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((0g‘𝑊) ∈ (𝐾‘𝐺) ↔ ((0g‘𝑊) ∈ (Base‘𝑊) ∧ (𝐺‘(0g‘𝑊)) =
(0g‘(Scalar‘𝑊))))) |
14 | 11, 12, 13 | mpbir2and 713 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (0g‘𝑊) ∈ (𝐾‘𝐺)) |
15 | 14 | ne0d 4250 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ≠ ∅) |
16 | | simplll 775 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑊 ∈ LMod) |
17 | | simplr 769 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) |
18 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝐺 ∈ 𝐹) |
19 | | simprl 771 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑥 ∈ (𝐾‘𝐺)) |
20 | 1, 4, 5 | lkrcl 36843 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ (𝐾‘𝐺)) → 𝑥 ∈ (Base‘𝑊)) |
21 | 16, 18, 19, 20 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑥 ∈ (Base‘𝑊)) |
22 | | eqid 2737 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
23 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
24 | 1, 2, 22, 23 | lmodvscl 19916 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
25 | 16, 17, 21, 24 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
26 | | simprr 773 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑦 ∈ (𝐾‘𝐺)) |
27 | 1, 4, 5 | lkrcl 36843 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ (𝐾‘𝐺)) → 𝑦 ∈ (Base‘𝑊)) |
28 | 16, 18, 26, 27 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑦 ∈ (Base‘𝑊)) |
29 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑊) = (+g‘𝑊) |
30 | 1, 29 | lmodvacl 19913 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑟(
·𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊)) |
31 | 16, 25, 28, 30 | syl3anc 1373 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊)) |
32 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) |
33 | | eqid 2737 |
. . . . . . . 8
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
34 | 1, 29, 2, 22, 23, 32, 33, 4 | lfli 36812 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦))) |
35 | 16, 18, 17, 21, 28, 34 | syl113anc 1384 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦))) |
36 | 2, 3, 4, 5 | lkrf0 36844 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ (𝐾‘𝐺)) → (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))) |
37 | 16, 18, 19, 36 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))) |
38 | 37 | oveq2d 7229 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥)) = (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) |
39 | 2 | lmodring 19907 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) |
40 | 16, 39 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (Scalar‘𝑊) ∈ Ring) |
41 | 23, 33, 3 | ringrz 19606 |
. . . . . . . . 9
⊢
(((Scalar‘𝑊)
∈ Ring ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
42 | 40, 17, 41 | syl2anc 587 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
43 | 38, 42 | eqtrd 2777 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥)) = (0g‘(Scalar‘𝑊))) |
44 | 2, 3, 4, 5 | lkrf0 36844 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ (𝐾‘𝐺)) → (𝐺‘𝑦) = (0g‘(Scalar‘𝑊))) |
45 | 16, 18, 26, 44 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘𝑦) = (0g‘(Scalar‘𝑊))) |
46 | 43, 45 | oveq12d 7231 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦)) =
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) |
47 | 2 | lmodfgrp 19908 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) |
48 | 16, 47 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (Scalar‘𝑊) ∈ Grp) |
49 | 23, 3 | grpidcl 18395 |
. . . . . . 7
⊢
((Scalar‘𝑊)
∈ Grp → (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
50 | 23, 32, 3 | grplid 18397 |
. . . . . . 7
⊢
(((Scalar‘𝑊)
∈ Grp ∧ (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
51 | 48, 49, 50 | syl2anc2 588 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
52 | 35, 46, 51 | 3eqtrd 2781 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (0g‘(Scalar‘𝑊))) |
53 | 1, 2, 3, 4, 5 | ellkr 36840 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺) ↔ (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊) ∧ (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (0g‘(Scalar‘𝑊))))) |
54 | 53 | ad2antrr 726 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺) ↔ (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊) ∧ (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (0g‘(Scalar‘𝑊))))) |
55 | 31, 52, 54 | mpbir2and 713 |
. . . 4
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) |
56 | 55 | ralrimivva 3112 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) → ∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) |
57 | 56 | ralrimiva 3105 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) |
58 | | lkrlss.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑊) |
59 | 2, 23, 1, 29, 22, 58 | islss 19971 |
. 2
⊢ ((𝐾‘𝐺) ∈ 𝑆 ↔ ((𝐾‘𝐺) ⊆ (Base‘𝑊) ∧ (𝐾‘𝐺) ≠ ∅ ∧ ∀𝑟 ∈
(Base‘(Scalar‘𝑊))∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺))) |
60 | 8, 15, 57, 59 | syl3anbrc 1345 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ∈ 𝑆) |