Metamath Proof Explorer

Theorem lss1d

Description: One-dimensional subspace (or zero-dimensional if X is the zero vector). (Contributed by NM, 14-Jan-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lss1d.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lss1d.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lss1d.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lss1d.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lss1d.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lss1d ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lss1d.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lss1d.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 lss1d.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 lss1d.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lss1d.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
6 2 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝐹 = ( Scalar ‘ 𝑊 ) )
7 4 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝐾 = ( Base ‘ 𝐹 ) )
8 1 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑉 = ( Base ‘ 𝑊 ) )
9 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) )
10 3 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → · = ( ·𝑠 ‘ 𝑊 ) )
11 5 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑆 = ( LSubSp ‘ 𝑊 ) )
12 1 2 3 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑘 · 𝑋 ) ∈ 𝑉 )
13 12 3expa ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ 𝐾 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑘 · 𝑋 ) ∈ 𝑉 )
14 13 an32s ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑘 ∈ 𝐾 ) → ( 𝑘 · 𝑋 ) ∈ 𝑉 )
15 eleq1a ⊢ ( ( 𝑘 · 𝑋 ) ∈ 𝑉 → ( 𝑣 = ( 𝑘 · 𝑋 ) → 𝑣 ∈ 𝑉 ) )
16 14 15 syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑘 ∈ 𝐾 ) → ( 𝑣 = ( 𝑘 · 𝑋 ) → 𝑣 ∈ 𝑉 ) )
17 16 rexlimdva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) → 𝑣 ∈ 𝑉 ) )
18 17 abssdv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ⊆ 𝑉 )
19 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
20 2 4 19 lmod0cl ⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝐹 ) ∈ 𝐾 )
21 20 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 0g ‘ 𝐹 ) ∈ 𝐾 )
22 nfcv ⊢ Ⅎ 𝑘 ( 0g ‘ 𝐹 )
23 nfre1 ⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 )
24 23 nfab ⊢ Ⅎ 𝑘 { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) }
25 nfcv ⊢ Ⅎ 𝑘 ∅
26 24 25 nfne ⊢ Ⅎ 𝑘 { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ≠ ∅
27 biidd ⊢ ( 𝑘 = ( 0g ‘ 𝐹 ) → ( { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ≠ ∅ ↔ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ≠ ∅ ) )
28 ovex ⊢ ( 𝑘 · 𝑋 ) ∈ V
29 28 elabrex ⊢ ( 𝑘 ∈ 𝐾 → ( 𝑘 · 𝑋 ) ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } )
30 29 ne0d ⊢ ( 𝑘 ∈ 𝐾 → { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ≠ ∅ )
31 22 26 27 30 vtoclgaf ⊢ ( ( 0g ‘ 𝐹 ) ∈ 𝐾 → { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ≠ ∅ )
32 21 31 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ≠ ∅ )
33 vex ⊢ 𝑎 ∈ V
34 eqeq1 ⊢ ( 𝑣 = 𝑎 → ( 𝑣 = ( 𝑘 · 𝑋 ) ↔ 𝑎 = ( 𝑘 · 𝑋 ) ) )
35 34 rexbidv ⊢ ( 𝑣 = 𝑎 → ( ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) ↔ ∃ 𝑘 ∈ 𝐾 𝑎 = ( 𝑘 · 𝑋 ) ) )
36 33 35 elab ⊢ ( 𝑎 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ↔ ∃ 𝑘 ∈ 𝐾 𝑎 = ( 𝑘 · 𝑋 ) )
37 oveq1 ⊢ ( 𝑘 = 𝑦 → ( 𝑘 · 𝑋 ) = ( 𝑦 · 𝑋 ) )
38 37 eqeq2d ⊢ ( 𝑘 = 𝑦 → ( 𝑎 = ( 𝑘 · 𝑋 ) ↔ 𝑎 = ( 𝑦 · 𝑋 ) ) )
39 38 cbvrexvw ⊢ ( ∃ 𝑘 ∈ 𝐾 𝑎 = ( 𝑘 · 𝑋 ) ↔ ∃ 𝑦 ∈ 𝐾 𝑎 = ( 𝑦 · 𝑋 ) )
40 36 39 bitri ⊢ ( 𝑎 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ↔ ∃ 𝑦 ∈ 𝐾 𝑎 = ( 𝑦 · 𝑋 ) )
41 vex ⊢ 𝑏 ∈ V
42 eqeq1 ⊢ ( 𝑣 = 𝑏 → ( 𝑣 = ( 𝑘 · 𝑋 ) ↔ 𝑏 = ( 𝑘 · 𝑋 ) ) )
43 42 rexbidv ⊢ ( 𝑣 = 𝑏 → ( ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) ↔ ∃ 𝑘 ∈ 𝐾 𝑏 = ( 𝑘 · 𝑋 ) ) )
44 41 43 elab ⊢ ( 𝑏 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ↔ ∃ 𝑘 ∈ 𝐾 𝑏 = ( 𝑘 · 𝑋 ) )
45 oveq1 ⊢ ( 𝑘 = 𝑧 → ( 𝑘 · 𝑋 ) = ( 𝑧 · 𝑋 ) )
46 45 eqeq2d ⊢ ( 𝑘 = 𝑧 → ( 𝑏 = ( 𝑘 · 𝑋 ) ↔ 𝑏 = ( 𝑧 · 𝑋 ) ) )
47 46 cbvrexvw ⊢ ( ∃ 𝑘 ∈ 𝐾 𝑏 = ( 𝑘 · 𝑋 ) ↔ ∃ 𝑧 ∈ 𝐾 𝑏 = ( 𝑧 · 𝑋 ) )
48 44 47 bitri ⊢ ( 𝑏 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ↔ ∃ 𝑧 ∈ 𝐾 𝑏 = ( 𝑧 · 𝑋 ) )
49 40 48 anbi12i ⊢ ( ( 𝑎 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ∧ 𝑏 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ) ↔ ( ∃ 𝑦 ∈ 𝐾 𝑎 = ( 𝑦 · 𝑋 ) ∧ ∃ 𝑧 ∈ 𝐾 𝑏 = ( 𝑧 · 𝑋 ) ) )
50 reeanv ⊢ ( ∃ 𝑦 ∈ 𝐾 ∃ 𝑧 ∈ 𝐾 ( 𝑎 = ( 𝑦 · 𝑋 ) ∧ 𝑏 = ( 𝑧 · 𝑋 ) ) ↔ ( ∃ 𝑦 ∈ 𝐾 𝑎 = ( 𝑦 · 𝑋 ) ∧ ∃ 𝑧 ∈ 𝐾 𝑏 = ( 𝑧 · 𝑋 ) ) )
51 49 50 bitr4i ⊢ ( ( 𝑎 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ∧ 𝑏 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ) ↔ ∃ 𝑦 ∈ 𝐾 ∃ 𝑧 ∈ 𝐾 ( 𝑎 = ( 𝑦 · 𝑋 ) ∧ 𝑏 = ( 𝑧 · 𝑋 ) ) )
52 simpll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → 𝑊 ∈ LMod )
53 simprr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → 𝑥 ∈ 𝐾 )
54 simprll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → 𝑦 ∈ 𝐾 )
55 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
56 2 4 55 lmodmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ∈ 𝐾 )
57 52 53 54 56 syl3anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ∈ 𝐾 )
58 simprlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → 𝑧 ∈ 𝐾 )
59 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
60 2 4 59 lmodacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) → ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ( +g ‘ 𝐹 ) 𝑧 ) ∈ 𝐾 )
61 52 57 58 60 syl3anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ( +g ‘ 𝐹 ) 𝑧 ) ∈ 𝐾 )
62 simplr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → 𝑋 ∈ 𝑉 )
63 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
64 1 63 2 3 4 59 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ( +g ‘ 𝐹 ) 𝑧 ) · 𝑋 ) = ( ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) )
65 52 57 58 62 64 syl13anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → ( ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ( +g ‘ 𝐹 ) 𝑧 ) · 𝑋 ) = ( ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) )
66 1 2 3 4 55 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) · 𝑋 ) = ( 𝑥 · ( 𝑦 · 𝑋 ) ) )
67 52 53 54 62 66 syl13anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) · 𝑋 ) = ( 𝑥 · ( 𝑦 · 𝑋 ) ) )
68 67 oveq1d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → ( ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) = ( ( 𝑥 · ( 𝑦 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) )
69 65 68 eqtr2d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → ( ( 𝑥 · ( 𝑦 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) = ( ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ( +g ‘ 𝐹 ) 𝑧 ) · 𝑋 ) )
70 oveq1 ⊢ ( 𝑘 = ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ( +g ‘ 𝐹 ) 𝑧 ) → ( 𝑘 · 𝑋 ) = ( ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ( +g ‘ 𝐹 ) 𝑧 ) · 𝑋 ) )
71 70 rspceeqv ⊢ ( ( ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ( +g ‘ 𝐹 ) 𝑧 ) ∈ 𝐾 ∧ ( ( 𝑥 · ( 𝑦 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) = ( ( ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ( +g ‘ 𝐹 ) 𝑧 ) · 𝑋 ) ) → ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · ( 𝑦 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) = ( 𝑘 · 𝑋 ) )
72 61 69 71 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · ( 𝑦 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) = ( 𝑘 · 𝑋 ) )
73 oveq2 ⊢ ( 𝑎 = ( 𝑦 · 𝑋 ) → ( 𝑥 · 𝑎 ) = ( 𝑥 · ( 𝑦 · 𝑋 ) ) )
74 oveq12 ⊢ ( ( ( 𝑥 · 𝑎 ) = ( 𝑥 · ( 𝑦 · 𝑋 ) ) ∧ 𝑏 = ( 𝑧 · 𝑋 ) ) → ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( ( 𝑥 · ( 𝑦 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) )
75 73 74 sylan ⊢ ( ( 𝑎 = ( 𝑦 · 𝑋 ) ∧ 𝑏 = ( 𝑧 · 𝑋 ) ) → ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( ( 𝑥 · ( 𝑦 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) )
76 75 eqeq1d ⊢ ( ( 𝑎 = ( 𝑦 · 𝑋 ) ∧ 𝑏 = ( 𝑧 · 𝑋 ) ) → ( ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ↔ ( ( 𝑥 · ( 𝑦 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) = ( 𝑘 · 𝑋 ) ) )
77 76 rexbidv ⊢ ( ( 𝑎 = ( 𝑦 · 𝑋 ) ∧ 𝑏 = ( 𝑧 · 𝑋 ) ) → ( ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ↔ ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · ( 𝑦 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑧 · 𝑋 ) ) = ( 𝑘 · 𝑋 ) ) )
78 72 77 syl5ibrcom ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) ) → ( ( 𝑎 = ( 𝑦 · 𝑋 ) ∧ 𝑏 = ( 𝑧 · 𝑋 ) ) → ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ) )
79 78 expr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑥 ∈ 𝐾 → ( ( 𝑎 = ( 𝑦 · 𝑋 ) ∧ 𝑏 = ( 𝑧 · 𝑋 ) ) → ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ) ) )
80 79 com23 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑎 = ( 𝑦 · 𝑋 ) ∧ 𝑏 = ( 𝑧 · 𝑋 ) ) → ( 𝑥 ∈ 𝐾 → ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ) ) )
81 80 rexlimdvva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ∃ 𝑦 ∈ 𝐾 ∃ 𝑧 ∈ 𝐾 ( 𝑎 = ( 𝑦 · 𝑋 ) ∧ 𝑏 = ( 𝑧 · 𝑋 ) ) → ( 𝑥 ∈ 𝐾 → ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ) ) )
82 51 81 syl5bi ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑎 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ∧ 𝑏 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ) → ( 𝑥 ∈ 𝐾 → ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ) ) )
83 82 expcomd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑏 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } → ( 𝑎 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } → ( 𝑥 ∈ 𝐾 → ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ) ) ) )
84 83 com24 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐾 → ( 𝑎 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } → ( 𝑏 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } → ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ) ) ) )
85 84 3imp2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑎 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ∧ 𝑏 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ) ) → ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) )
86 ovex ⊢ ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ V
87 eqeq1 ⊢ ( 𝑣 = ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) → ( 𝑣 = ( 𝑘 · 𝑋 ) ↔ ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ) )
88 87 rexbidv ⊢ ( 𝑣 = ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) → ( ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) ↔ ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) ) )
89 86 88 elab ⊢ ( ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ↔ ∃ 𝑘 ∈ 𝐾 ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) = ( 𝑘 · 𝑋 ) )
90 85 89 sylibr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑎 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ∧ 𝑏 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ) ) → ( ( 𝑥 · 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } )
91 6 7 8 9 10 11 18 32 90 islssd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ∈ 𝑆 )