Metamath Proof Explorer

Theorem lkrlss

Description: The kernel of a linear functional is a subspace. ( nlelshi analog.) (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lkrlss.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lkrlss.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
lkrlss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lkrlss ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lkrlss.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 lkrlss.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
3 lkrlss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
4 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
6 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
7 4 5 6 1 2 lkrval2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝐺 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
8 ssrab2 ⊢ { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝐺 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ⊆ ( Base ‘ 𝑊 )
9 7 8 eqsstrdi ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑊 ) )
10 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
11 4 10 lmod0vcl ⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
12 11 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 0g ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
13 5 6 10 1 lfl0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
14 4 5 6 1 2 ellkr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 0g ‘ 𝑊 ) ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( ( 0g ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐺 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
15 12 13 14 mpbir2and ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 0g ‘ 𝑊 ) ∈ ( 𝐾 ‘ 𝐺 ) )
16 15 ne0d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) ≠ ∅ )
17 simplll ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → 𝑊 ∈ LMod )
18 simplr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
19 simpllr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → 𝐺 ∈ 𝐹 )
20 simprl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) )
21 4 1 2 lkrcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
22 17 19 20 21 syl3anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
23 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
24 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
25 4 5 23 24 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( Base ‘ 𝑊 ) )
26 17 18 22 25 syl3anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( Base ‘ 𝑊 ) )
27 simprr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) )
28 4 1 2 lkrcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
29 17 19 27 28 syl3anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
30 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
31 4 30 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( Base ‘ 𝑊 ) )
32 17 26 29 31 syl3anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( Base ‘ 𝑊 ) )
33 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
34 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
35 4 30 5 23 24 33 34 1 lfli ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) )
36 17 19 18 22 29 35 syl113anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) )
37 5 6 1 2 lkrf0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( 𝐺 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
38 17 19 20 37 syl3anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
39 38 oveq2d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
40 5 lmodring ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring )
41 17 40 syl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( Scalar ‘ 𝑊 ) ∈ Ring )
42 24 34 6 ringrz ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Ring ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
43 41 18 42 syl2anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
44 39 43 eqtrd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
45 5 6 1 2 lkrf0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( 𝐺 ‘ 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
46 17 19 27 45 syl3anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( 𝐺 ‘ 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
47 44 46 oveq12d ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
48 5 lmodfgrp ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Grp )
49 17 48 syl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( Scalar ‘ 𝑊 ) ∈ Grp )
50 24 6 grpidcl ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Grp → ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
51 24 33 6 grplid ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
52 49 50 51 syl2anc2 ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
53 36 47 52 3eqtrd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
54 4 5 6 1 2 ellkr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
55 54 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
56 32 53 55 mpbir2and ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐾 ‘ 𝐺 ) )
57 56 ralrimivva ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ∀ 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∀ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐾 ‘ 𝐺 ) )
58 57 ralrimiva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∀ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐾 ‘ 𝐺 ) )
59 5 24 4 30 23 3 islss ⊢ ( ( 𝐾 ‘ 𝐺 ) ∈ 𝑆 ↔ ( ( 𝐾 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ ∅ ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( 𝐾 ‘ 𝐺 ) ∀ 𝑦 ∈ ( 𝐾 ‘ 𝐺 ) ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ∈ ( 𝐾 ‘ 𝐺 ) ) )
60 9 16 58 59 syl3anbrc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝑆 )