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 ellspsni ⊢ ( ( ( 𝑊 ∈ 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 ) → ( ( 𝐾 ‘ 𝐺 ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )