| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . 4
⊢
(Base‘𝑊) =
(Base‘𝑊) | 
| 2 |  | eqid 2736 | . . . 4
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 3 |  | eqid 2736 | . . . 4
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) | 
| 4 |  | lkrlss.f | . . . 4
⊢ 𝐹 = (LFnl‘𝑊) | 
| 5 |  | lkrlss.k | . . . 4
⊢ 𝐾 = (LKer‘𝑊) | 
| 6 | 1, 2, 3, 4, 5 | lkrval2 39092 | . . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = {𝑥 ∈ (Base‘𝑊) ∣ (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))}) | 
| 7 |  | ssrab2 4079 | . . 3
⊢ {𝑥 ∈ (Base‘𝑊) ∣ (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))} ⊆ (Base‘𝑊) | 
| 8 | 6, 7 | eqsstrdi 4027 | . 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ⊆ (Base‘𝑊)) | 
| 9 |  | eqid 2736 | . . . . . 6
⊢
(0g‘𝑊) = (0g‘𝑊) | 
| 10 | 1, 9 | lmod0vcl 20890 | . . . . 5
⊢ (𝑊 ∈ LMod →
(0g‘𝑊)
∈ (Base‘𝑊)) | 
| 11 | 10 | adantr 480 | . . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (0g‘𝑊) ∈ (Base‘𝑊)) | 
| 12 | 2, 3, 9, 4 | lfl0 39067 | . . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐺‘(0g‘𝑊)) =
(0g‘(Scalar‘𝑊))) | 
| 13 | 1, 2, 3, 4, 5 | ellkr 39091 | . . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((0g‘𝑊) ∈ (𝐾‘𝐺) ↔ ((0g‘𝑊) ∈ (Base‘𝑊) ∧ (𝐺‘(0g‘𝑊)) =
(0g‘(Scalar‘𝑊))))) | 
| 14 | 11, 12, 13 | mpbir2and 713 | . . 3
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (0g‘𝑊) ∈ (𝐾‘𝐺)) | 
| 15 | 14 | ne0d 4341 | . 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ≠ ∅) | 
| 16 |  | simplll 774 | . . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑊 ∈ LMod) | 
| 17 |  | simplr 768 | . . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑟 ∈ (Base‘(Scalar‘𝑊))) | 
| 18 |  | simpllr 775 | . . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝐺 ∈ 𝐹) | 
| 19 |  | simprl 770 | . . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑥 ∈ (𝐾‘𝐺)) | 
| 20 | 1, 4, 5 | lkrcl 39094 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ (𝐾‘𝐺)) → 𝑥 ∈ (Base‘𝑊)) | 
| 21 | 16, 18, 19, 20 | syl3anc 1372 | . . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑥 ∈ (Base‘𝑊)) | 
| 22 |  | eqid 2736 | . . . . . . . 8
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) | 
| 23 |  | eqid 2736 | . . . . . . . 8
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 24 | 1, 2, 22, 23 | lmodvscl 20877 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) | 
| 25 | 16, 17, 21, 24 | syl3anc 1372 | . . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟( ·𝑠
‘𝑊)𝑥) ∈ (Base‘𝑊)) | 
| 26 |  | simprr 772 | . . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑦 ∈ (𝐾‘𝐺)) | 
| 27 | 1, 4, 5 | lkrcl 39094 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ (𝐾‘𝐺)) → 𝑦 ∈ (Base‘𝑊)) | 
| 28 | 16, 18, 26, 27 | syl3anc 1372 | . . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → 𝑦 ∈ (Base‘𝑊)) | 
| 29 |  | eqid 2736 | . . . . . . 7
⊢
(+g‘𝑊) = (+g‘𝑊) | 
| 30 | 1, 29 | lmodvacl 20874 | . . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑟(
·𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊)) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊)) | 
| 31 | 16, 25, 28, 30 | syl3anc 1372 | . . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (Base‘𝑊)) | 
| 32 |  | eqid 2736 | . . . . . . . 8
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) | 
| 33 |  | eqid 2736 | . . . . . . . 8
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) | 
| 34 | 1, 29, 2, 22, 23, 32, 33, 4 | lfli 39063 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (𝑟 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊) ∧ 𝑦 ∈ (Base‘𝑊))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦))) | 
| 35 | 16, 18, 17, 21, 28, 34 | syl113anc 1383 | . . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦))) | 
| 36 | 2, 3, 4, 5 | lkrf0 39095 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ (𝐾‘𝐺)) → (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))) | 
| 37 | 16, 18, 19, 36 | syl3anc 1372 | . . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘𝑥) = (0g‘(Scalar‘𝑊))) | 
| 38 | 37 | oveq2d 7448 | . . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥)) = (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) | 
| 39 | 2 | lmodring 20867 | . . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) | 
| 40 | 16, 39 | syl 17 | . . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (Scalar‘𝑊) ∈ Ring) | 
| 41 | 23, 33, 3 | ringrz 20292 | . . . . . . . . 9
⊢
(((Scalar‘𝑊)
∈ Ring ∧ 𝑟 ∈
(Base‘(Scalar‘𝑊))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) | 
| 42 | 40, 17, 41 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) | 
| 43 | 38, 42 | eqtrd 2776 | . . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥)) = (0g‘(Scalar‘𝑊))) | 
| 44 | 2, 3, 4, 5 | lkrf0 39095 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ (𝐾‘𝐺)) → (𝐺‘𝑦) = (0g‘(Scalar‘𝑊))) | 
| 45 | 16, 18, 26, 44 | syl3anc 1372 | . . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘𝑦) = (0g‘(Scalar‘𝑊))) | 
| 46 | 43, 45 | oveq12d 7450 | . . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → ((𝑟(.r‘(Scalar‘𝑊))(𝐺‘𝑥))(+g‘(Scalar‘𝑊))(𝐺‘𝑦)) =
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊)))) | 
| 47 | 2 | lmodfgrp 20868 | . . . . . . . 8
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) | 
| 48 | 16, 47 | syl 17 | . . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (Scalar‘𝑊) ∈ Grp) | 
| 49 | 23, 3 | grpidcl 18984 | . . . . . . 7
⊢
((Scalar‘𝑊)
∈ Grp → (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) | 
| 50 | 23, 32, 3 | grplid 18986 | . . . . . . 7
⊢
(((Scalar‘𝑊)
∈ Grp ∧ (0g‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) | 
| 51 | 48, 49, 50 | syl2anc2 585 | . . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) | 
| 52 | 35, 46, 51 | 3eqtrd 2780 | . . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝑥 ∈ (𝐾‘𝐺) ∧ 𝑦 ∈ (𝐾‘𝐺))) → (𝐺‘((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦)) = (0g‘(Scalar‘𝑊))) | 
| 53 | 1, 2, 3, 4, 5 | ellkr 39091 | . . . . . 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 3201 | . . 3
⊢ (((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) → ∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) | 
| 57 | 56 | ralrimiva 3145 | . 2
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺)) | 
| 58 |  | lkrlss.s | . . 3
⊢ 𝑆 = (LSubSp‘𝑊) | 
| 59 | 2, 23, 1, 29, 22, 58 | islss 20933 | . 2
⊢ ((𝐾‘𝐺) ∈ 𝑆 ↔ ((𝐾‘𝐺) ⊆ (Base‘𝑊) ∧ (𝐾‘𝐺) ≠ ∅ ∧ ∀𝑟 ∈
(Base‘(Scalar‘𝑊))∀𝑥 ∈ (𝐾‘𝐺)∀𝑦 ∈ (𝐾‘𝐺)((𝑟( ·𝑠
‘𝑊)𝑥)(+g‘𝑊)𝑦) ∈ (𝐾‘𝐺))) | 
| 60 | 8, 15, 57, 59 | syl3anbrc 1343 | 1
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ∈ 𝑆) |