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 ) โ†’ ( ( ๐พ โ€˜ ๐บ ) โŠ• ( ๐‘ โ€˜ { ๐‘‹ } ) ) = ๐‘‰ )