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 ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝑆 )