Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑊) =
(Base‘𝑊) |
2 | | eqid 2610 |
. . . 4
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
3 | | eqid 2610 |
. . . 4
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
4 | | lkrlss.f |
. . . 4
⊢ 𝐹 = (LFnl‘𝑊) |
5 | | lkrlss.k |
. . . 4
⊢ 𝐾 = (LKer‘𝑊) |
6 | 1, 2, 3, 4, 5 | lkrval2 33395 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = {𝑥 ∈ (Base‘𝑊) ∣ (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))}) |
7 | | ssrab2 3650 |
. . 3
⊢ {𝑥 ∈ (Base‘𝑊) ∣ (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))} ⊆ (Base‘𝑊) |
8 | 6, 7 | syl6eqss 3618 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ⊆ (Base‘𝑊)) |
9 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝑊) = (0g‘𝑊) |
10 | 1, 9 | lmod0vcl 18715 |
. . . . 5
⊢ (𝑊 ∈ LMod →
(0g‘𝑊)
∈ (Base‘𝑊)) |
11 | 10 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (0g‘𝑊) ∈ (Base‘𝑊)) |
12 | 2, 3, 9, 4 | lfl0 33370 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘(0g‘𝑊)) =
(0g‘(Scalar‘𝑊))) |
13 | 1, 2, 3, 4, 5 | ellkr 33394 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((0g‘𝑊) ∈ (𝐾‘𝐺) ↔ ((0g‘𝑊) ∈ (Base‘𝑊) ∧ (𝐺‘(0g‘𝑊)) =
(0g‘(Scalar‘𝑊))))) |
14 | 11, 12, 13 | mpbir2and 959 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (0g‘𝑊) ∈ (𝐾‘𝐺)) |
15 | | ne0i 3880 |
. . 3
⊢
((0g‘𝑊) ∈ (𝐾‘𝐺) → (𝐾‘𝐺) ≠ ∅) |
16 | 14, 15 | syl 17 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ≠ ∅) |
17 | | simplll 794 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑊 ∈ LMod) |
18 | | simplr 788 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) |
19 | | simpllr 795 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝐺 ∈ 𝐹) |
20 | | simprl 790 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑥 ∈ (𝐾‘𝐺)) |
21 | 1, 4, 5 | lkrcl 33397 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ (𝐾‘𝐺)) → 𝑥 ∈ (Base‘𝑊)) |
22 | 17, 19, 20, 21 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑥 ∈ (Base‘𝑊)) |
23 | | eqid 2610 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
24 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
25 | 1, 2, 23, 24 | lmodvscl 18703 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
26 | 17, 18, 22, 25 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) |
27 | | simprr 792 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑦 ∈ (𝐾‘𝐺)) |
28 | 1, 4, 5 | lkrcl 33397 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ (𝐾‘𝐺)) → 𝑦 ∈ (Base‘𝑊)) |
29 | 17, 19, 27, 28 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑦 ∈ (Base‘𝑊)) |
30 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑊) = (+g‘𝑊) |
31 | 1, 30 | lmodvacl 18700 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑟(
·𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊)) |
32 | 17, 26, 29, 31 | syl3anc 1318 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊)) |
33 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) |
34 | | eqid 2610 |
. . . . . . . 8
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
35 | 1, 30, 2, 23, 24, 33, 34, 4 | lfli 33366 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦))) |
36 | 17, 19, 18, 22, 29, 35 | syl113anc 1330 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦))) |
37 | 2, 3, 4, 5 | lkrf0 33398 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ (𝐾‘𝐺)) → (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))) |
38 | 17, 19, 20, 37 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))) |
39 | 38 | oveq2d 6565 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥)) = (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) |
40 | 2 | lmodring 18694 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) |
41 | 17, 40 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (Scalar‘𝑊) ∈ Ring) |
42 | 24, 34, 3 | ringrz 18411 |
. . . . . . . . 9
⊢
(((Scalar‘𝑊)
∈ Ring ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
43 | 41, 18, 42 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
44 | 39, 43 | eqtrd 2644 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥)) = (0g‘(Scalar‘𝑊))) |
45 | 2, 3, 4, 5 | lkrf0 33398 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ (𝐾‘𝐺)) → (𝐺‘𝑦) = (0g‘(Scalar‘𝑊))) |
46 | 17, 19, 27, 45 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘𝑦) = (0g‘(Scalar‘𝑊))) |
47 | 44, 46 | oveq12d 6567 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦)) =
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) |
48 | 2 | lmodfgrp 18695 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) |
49 | 17, 48 | syl 17 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (Scalar‘𝑊) ∈ Grp) |
50 | 24, 3 | grpidcl 17273 |
. . . . . . . 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 17275 |
. . . . . . 7
⊢
(((Scalar‘𝑊)
∈ Grp ∧ (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
53 | 49, 51, 52 | syl2anc 691 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
54 | 36, 47, 53 | 3eqtrd 2648 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (0g‘(Scalar‘𝑊))) |
55 | 1, 2, 3, 4, 5 | ellkr 33394 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺) ↔ (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊) ∧ (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (0g‘(Scalar‘𝑊))))) |
56 | 55 | ad2antrr 758 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺) ↔ (((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊) ∧ (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (0g‘(Scalar‘𝑊))))) |
57 | 32, 54, 56 | mpbir2and 959 |
. . . 4
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) |
58 | 57 | ralrimivva 2954 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) → ∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) |
59 | 58 | ralrimiva 2949 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) |
60 | | lkrlss.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑊) |
61 | 2, 24, 1, 30, 23, 60 | islss 18756 |
. 2
⊢ ((𝐾‘𝐺) ∈ 𝑆 ↔ ((𝐾‘𝐺) ⊆ (Base‘𝑊) ∧ (𝐾‘𝐺) ≠ ∅ ∧ ∀𝑟 ∈
(Base‘(Scalar‘𝑊))∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺))) |
62 | 8, 16, 59, 61 | syl3anbrc 1239 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ∈ 𝑆) |