Metamath Proof Explorer


Theorem lkrlsp

Description: The subspace sum of a kernel and the span of a vector not in the kernel (by ellkr ) is the whole vector space. (Contributed by NM, 19-Apr-2014)

Ref Expression
Hypotheses lkrlsp.d 𝐷 = ( Scalar ‘ 𝑊 )
lkrlsp.o 0 = ( 0g𝐷 )
lkrlsp.v 𝑉 = ( Base ‘ 𝑊 )
lkrlsp.n 𝑁 = ( LSpan ‘ 𝑊 )
lkrlsp.p = ( LSSum ‘ 𝑊 )
lkrlsp.f 𝐹 = ( LFnl ‘ 𝑊 )
lkrlsp.k 𝐾 = ( LKer ‘ 𝑊 )
Assertion lkrlsp ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → ( ( 𝐾𝐺 ) ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )

Proof

Step Hyp Ref Expression
1 lkrlsp.d 𝐷 = ( Scalar ‘ 𝑊 )
2 lkrlsp.o 0 = ( 0g𝐷 )
3 lkrlsp.v 𝑉 = ( Base ‘ 𝑊 )
4 lkrlsp.n 𝑁 = ( LSpan ‘ 𝑊 )
5 lkrlsp.p = ( LSSum ‘ 𝑊 )
6 lkrlsp.f 𝐹 = ( LFnl ‘ 𝑊 )
7 lkrlsp.k 𝐾 = ( LKer ‘ 𝑊 )
8 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9 8 3ad2ant1 ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → 𝑊 ∈ LMod )
10 simp2r ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → 𝐺𝐹 )
11 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
12 6 7 11 lkrlss ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 𝐾𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) )
13 9 10 12 syl2anc ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → ( 𝐾𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) )
14 simp2l ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → 𝑋𝑉 )
15 3 11 4 lspsncl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
16 9 14 15 syl2anc ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
17 11 5 lsmcl ( ( 𝑊 ∈ LMod ∧ ( 𝐾𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( 𝐾𝐺 ) ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
18 9 13 16 17 syl3anc ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → ( ( 𝐾𝐺 ) ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
19 3 11 lssss ( ( ( 𝐾𝐺 ) ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( LSubSp ‘ 𝑊 ) → ( ( 𝐾𝐺 ) ( 𝑁 ‘ { 𝑋 } ) ) ⊆ 𝑉 )
20 18 19 syl ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → ( ( 𝐾𝐺 ) ( 𝑁 ‘ { 𝑋 } ) ) ⊆ 𝑉 )
21 simpl1 ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → 𝑊 ∈ LVec )
22 21 8 syl ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → 𝑊 ∈ LMod )
23 simpr ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → 𝑢𝑉 )
24 1 lmodring ( 𝑊 ∈ LMod → 𝐷 ∈ Ring )
25 22 24 syl ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → 𝐷 ∈ Ring )
26 simpl2r ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → 𝐺𝐹 )
27 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
28 1 27 3 6 lflcl ( ( 𝑊 ∈ LVec ∧ 𝐺𝐹𝑢𝑉 ) → ( 𝐺𝑢 ) ∈ ( Base ‘ 𝐷 ) )
29 21 26 23 28 syl3anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝐺𝑢 ) ∈ ( Base ‘ 𝐷 ) )
30 1 lvecdrng ( 𝑊 ∈ LVec → 𝐷 ∈ DivRing )
31 21 30 syl ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → 𝐷 ∈ DivRing )
32 simpl2l ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → 𝑋𝑉 )
33 1 27 3 6 lflcl ( ( 𝑊 ∈ LVec ∧ 𝐺𝐹𝑋𝑉 ) → ( 𝐺𝑋 ) ∈ ( Base ‘ 𝐷 ) )
34 21 26 32 33 syl3anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝐺𝑋 ) ∈ ( Base ‘ 𝐷 ) )
35 simpl3 ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝐺𝑋 ) ≠ 0 )
36 eqid ( invr𝐷 ) = ( invr𝐷 )
37 27 2 36 drnginvrcl ( ( 𝐷 ∈ DivRing ∧ ( 𝐺𝑋 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ∈ ( Base ‘ 𝐷 ) )
38 31 34 35 37 syl3anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ∈ ( Base ‘ 𝐷 ) )
39 eqid ( .r𝐷 ) = ( .r𝐷 )
40 27 39 ringcl ( ( 𝐷 ∈ Ring ∧ ( 𝐺𝑢 ) ∈ ( Base ‘ 𝐷 ) ∧ ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ∈ ( Base ‘ 𝐷 ) )
41 25 29 38 40 syl3anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ∈ ( Base ‘ 𝐷 ) )
42 eqid ( ·𝑠𝑊 ) = ( ·𝑠𝑊 )
43 3 1 42 27 lmodvscl ( ( 𝑊 ∈ LMod ∧ ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑋𝑉 ) → ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ∈ 𝑉 )
44 22 41 32 43 syl3anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ∈ 𝑉 )
45 eqid ( +g𝑊 ) = ( +g𝑊 )
46 eqid ( -g𝑊 ) = ( -g𝑊 )
47 3 45 46 lmodvnpcan ( ( 𝑊 ∈ LMod ∧ 𝑢𝑉 ∧ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ∈ 𝑉 ) → ( ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) = 𝑢 )
48 22 23 44 47 syl3anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) = 𝑢 )
49 11 lsssssubg ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
50 22 49 syl ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
51 13 adantr ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝐾𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) )
52 50 51 sseldd ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝐾𝐺 ) ∈ ( SubGrp ‘ 𝑊 ) )
53 16 adantr ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
54 50 53 sseldd ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
55 3 46 lmodvsubcl ( ( 𝑊 ∈ LMod ∧ 𝑢𝑉 ∧ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ∈ 𝑉 ) → ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ∈ 𝑉 )
56 22 23 44 55 syl3anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ∈ 𝑉 )
57 eqid ( -g𝐷 ) = ( -g𝐷 )
58 1 57 3 46 6 lflsub ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ∧ ( 𝑢𝑉 ∧ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ∈ 𝑉 ) ) → ( 𝐺 ‘ ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ) = ( ( 𝐺𝑢 ) ( -g𝐷 ) ( 𝐺 ‘ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ) )
59 22 26 23 44 58 syl112anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝐺 ‘ ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ) = ( ( 𝐺𝑢 ) ( -g𝐷 ) ( 𝐺 ‘ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ) )
60 1 27 39 3 42 6 lflmul ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ∧ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑋𝑉 ) ) → ( 𝐺 ‘ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) = ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( .r𝐷 ) ( 𝐺𝑋 ) ) )
61 22 26 41 32 60 syl112anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝐺 ‘ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) = ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( .r𝐷 ) ( 𝐺𝑋 ) ) )
62 27 39 ringass ( ( 𝐷 ∈ Ring ∧ ( ( 𝐺𝑢 ) ∈ ( Base ‘ 𝐷 ) ∧ ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺𝑋 ) ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( .r𝐷 ) ( 𝐺𝑋 ) ) = ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ( .r𝐷 ) ( 𝐺𝑋 ) ) ) )
63 25 29 38 34 62 syl13anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( .r𝐷 ) ( 𝐺𝑋 ) ) = ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ( .r𝐷 ) ( 𝐺𝑋 ) ) ) )
64 eqid ( 1r𝐷 ) = ( 1r𝐷 )
65 27 2 39 64 36 drnginvrl ( ( 𝐷 ∈ DivRing ∧ ( 𝐺𝑋 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → ( ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ( .r𝐷 ) ( 𝐺𝑋 ) ) = ( 1r𝐷 ) )
66 31 34 35 65 syl3anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ( .r𝐷 ) ( 𝐺𝑋 ) ) = ( 1r𝐷 ) )
67 66 oveq2d ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ( .r𝐷 ) ( 𝐺𝑋 ) ) ) = ( ( 𝐺𝑢 ) ( .r𝐷 ) ( 1r𝐷 ) ) )
68 27 39 64 ringridm ( ( 𝐷 ∈ Ring ∧ ( 𝐺𝑢 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝐺𝑢 ) ( .r𝐷 ) ( 1r𝐷 ) ) = ( 𝐺𝑢 ) )
69 25 29 68 syl2anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( 𝐺𝑢 ) ( .r𝐷 ) ( 1r𝐷 ) ) = ( 𝐺𝑢 ) )
70 67 69 eqtrd ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ( .r𝐷 ) ( 𝐺𝑋 ) ) ) = ( 𝐺𝑢 ) )
71 61 63 70 3eqtrd ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝐺 ‘ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) = ( 𝐺𝑢 ) )
72 71 oveq2d ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( 𝐺𝑢 ) ( -g𝐷 ) ( 𝐺 ‘ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ) = ( ( 𝐺𝑢 ) ( -g𝐷 ) ( 𝐺𝑢 ) ) )
73 1 lmodfgrp ( 𝑊 ∈ LMod → 𝐷 ∈ Grp )
74 22 73 syl ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → 𝐷 ∈ Grp )
75 27 2 57 grpsubid ( ( 𝐷 ∈ Grp ∧ ( 𝐺𝑢 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝐺𝑢 ) ( -g𝐷 ) ( 𝐺𝑢 ) ) = 0 )
76 74 29 75 syl2anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( 𝐺𝑢 ) ( -g𝐷 ) ( 𝐺𝑢 ) ) = 0 )
77 59 72 76 3eqtrd ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝐺 ‘ ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ) = 0 )
78 3 1 2 6 7 ellkr ( ( 𝑊 ∈ LVec ∧ 𝐺𝐹 ) → ( ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ∈ ( 𝐾𝐺 ) ↔ ( ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ∈ 𝑉 ∧ ( 𝐺 ‘ ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ) = 0 ) ) )
79 21 26 78 syl2anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ∈ ( 𝐾𝐺 ) ↔ ( ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ∈ 𝑉 ∧ ( 𝐺 ‘ ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ) = 0 ) ) )
80 56 77 79 mpbir2and ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ∈ ( 𝐾𝐺 ) )
81 3 42 1 27 4 22 41 32 lspsneli ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )
82 45 5 lsmelvali ( ( ( ( 𝐾𝐺 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ) ∧ ( ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ∈ ( 𝐾𝐺 ) ∧ ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) ) ) → ( ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ∈ ( ( 𝐾𝐺 ) ( 𝑁 ‘ { 𝑋 } ) ) )
83 52 54 80 81 82 syl22anc ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → ( ( 𝑢 ( -g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ( +g𝑊 ) ( ( ( 𝐺𝑢 ) ( .r𝐷 ) ( ( invr𝐷 ) ‘ ( 𝐺𝑋 ) ) ) ( ·𝑠𝑊 ) 𝑋 ) ) ∈ ( ( 𝐾𝐺 ) ( 𝑁 ‘ { 𝑋 } ) ) )
84 48 83 eqeltrrd ( ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) ∧ 𝑢𝑉 ) → 𝑢 ∈ ( ( 𝐾𝐺 ) ( 𝑁 ‘ { 𝑋 } ) ) )
85 20 84 eqelssd ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ( 𝐺𝑋 ) ≠ 0 ) → ( ( 𝐾𝐺 ) ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )