Metamath Proof Explorer

Theorem lspexch

Description: Exchange property for span of a pair. TODO: see if a version with Y,Z and X,Z reversed will shorten proofs (analogous to lspexchn1 versus lspexchn2 ); look for lspexch and prcom in same proof. TODO: would a hypothesis of -. X e. ( N{ Z } ) instead of ( N{ X } ) =/= ( N{ Z } ) be better overall? This would be shorter and also satisfy the X =/= .0. condition. Here and also lspindp* and all proofs affected by them (all in NM's mathbox); there are 58 hypotheses with the =/= pattern as of 24-May-2015. (Contributed by NM, 11-Apr-2015)

Ref Expression
Hypotheses lspexch.v 
|- V = ( Base ` W )
lspexch.o 
|- .0. = ( 0g ` W )
lspexch.n 
|- N = ( LSpan ` W )
lspexch.w 
|- ( ph -> W e. LVec )
lspexch.x 
|- ( ph -> X e. ( V \ { .0. } ) )
lspexch.y 
|- ( ph -> Y e. V )
lspexch.z 
|- ( ph -> Z e. V )
lspexch.q 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )
lspexch.e 
|- ( ph -> X e. ( N ` { Y , Z } ) )
Assertion lspexch 
|- ( ph -> Y e. ( N ` { X , Z } ) )

Proof

Step Hyp Ref Expression
1 lspexch.v 
 |-  V = ( Base ` W )
2 lspexch.o 
 |-  .0. = ( 0g ` W )
3 lspexch.n 
 |-  N = ( LSpan ` W )
4 lspexch.w 
 |-  ( ph -> W e. LVec )
5 lspexch.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
6 lspexch.y 
 |-  ( ph -> Y e. V )
7 lspexch.z 
 |-  ( ph -> Z e. V )
8 lspexch.q 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )
9 lspexch.e 
 |-  ( ph -> X e. ( N ` { Y , Z } ) )
10 eqid 
 |-  ( +g ` W ) = ( +g ` W )
11 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
12 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
13 eqid 
 |-  ( .s ` W ) = ( .s ` W )
14 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
15 4 14 syl 
 |-  ( ph -> W e. LMod )
16 1 10 11 12 13 3 15 6 7 lspprel 
 |-  ( ph -> ( X e. ( N ` { Y , Z } ) <-> E. j e. ( Base ` ( Scalar ` W ) ) E. k e. ( Base ` ( Scalar ` W ) ) X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) )
17 9 16 mpbid 
 |-  ( ph -> E. j e. ( Base ` ( Scalar ` W ) ) E. k e. ( Base ` ( Scalar ` W ) ) X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) )
18 eqid 
 |-  ( -g ` W ) = ( -g ` W )
19 eqid 
 |-  ( invg ` ( Scalar ` W ) ) = ( invg ` ( Scalar ` W ) )
20 4 3ad2ant1 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> W e. LVec )
21 20 14 syl 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> W e. LMod )
22 simp2r 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> k e. ( Base ` ( Scalar ` W ) ) )
23 5 3ad2ant1 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> X e. ( V \ { .0. } ) )
24 23 eldifad 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> X e. V )
25 7 3ad2ant1 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> Z e. V )
26 1 10 18 13 11 12 19 21 22 24 25 lmodsubvs 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( X ( -g ` W ) ( k ( .s ` W ) Z ) ) = ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) )
27 simp3 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) )
28 27 eqcomd 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) = X )
29 15 3ad2ant1 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> W e. LMod )
30 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
31 29 30 syl 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> W e. Grp )
32 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) /\ Z e. V ) -> ( k ( .s ` W ) Z ) e. V )
33 21 22 25 32 syl3anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( k ( .s ` W ) Z ) e. V )
34 simp2l 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> j e. ( Base ` ( Scalar ` W ) ) )
35 6 3ad2ant1 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> Y e. V )
36 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ j e. ( Base ` ( Scalar ` W ) ) /\ Y e. V ) -> ( j ( .s ` W ) Y ) e. V )
37 21 34 35 36 syl3anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( j ( .s ` W ) Y ) e. V )
38 1 10 18 grpsubadd 
 |-  ( ( W e. Grp /\ ( X e. V /\ ( k ( .s ` W ) Z ) e. V /\ ( j ( .s ` W ) Y ) e. V ) ) -> ( ( X ( -g ` W ) ( k ( .s ` W ) Z ) ) = ( j ( .s ` W ) Y ) <-> ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) = X ) )
39 31 24 33 37 38 syl13anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( X ( -g ` W ) ( k ( .s ` W ) Z ) ) = ( j ( .s ` W ) Y ) <-> ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) = X ) )
40 28 39 mpbird 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( X ( -g ` W ) ( k ( .s ` W ) Z ) ) = ( j ( .s ` W ) Y ) )
41 26 40 eqtr3d 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) = ( j ( .s ` W ) Y ) )
42 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
43 eqid 
 |-  ( invr ` ( Scalar ` W ) ) = ( invr ` ( Scalar ` W ) )
44 8 3ad2ant1 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( N ` { X } ) =/= ( N ` { Z } ) )
45 20 adantr 
 |-  ( ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) /\ j = ( 0g ` ( Scalar ` W ) ) ) -> W e. LVec )
46 25 adantr 
 |-  ( ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) /\ j = ( 0g ` ( Scalar ` W ) ) ) -> Z e. V )
47 27 adantr 
 |-  ( ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) /\ j = ( 0g ` ( Scalar ` W ) ) ) -> X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) )
48 oveq1 
 |-  ( j = ( 0g ` ( Scalar ` W ) ) -> ( j ( .s ` W ) Y ) = ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) )
49 48 oveq1d 
 |-  ( j = ( 0g ` ( Scalar ` W ) ) -> ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) = ( ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) )
50 1 11 13 42 2 lmod0vs 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) = .0. )
51 21 35 50 syl2anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) = .0. )
52 51 oveq1d 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) = ( .0. ( +g ` W ) ( k ( .s ` W ) Z ) ) )
53 1 10 2 lmod0vlid 
 |-  ( ( W e. LMod /\ ( k ( .s ` W ) Z ) e. V ) -> ( .0. ( +g ` W ) ( k ( .s ` W ) Z ) ) = ( k ( .s ` W ) Z ) )
54 21 33 53 syl2anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( .0. ( +g ` W ) ( k ( .s ` W ) Z ) ) = ( k ( .s ` W ) Z ) )
55 52 54 eqtrd 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) = ( k ( .s ` W ) Z ) )
56 49 55 sylan9eqr 
 |-  ( ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) /\ j = ( 0g ` ( Scalar ` W ) ) ) -> ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) = ( k ( .s ` W ) Z ) )
57 47 56 eqtrd 
 |-  ( ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) /\ j = ( 0g ` ( Scalar ` W ) ) ) -> X = ( k ( .s ` W ) Z ) )
58 1 13 11 12 3 21 22 25 ellspsni 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( k ( .s ` W ) Z ) e. ( N ` { Z } ) )
59 58 adantr 
 |-  ( ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) /\ j = ( 0g ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) Z ) e. ( N ` { Z } ) )
60 57 59 eqeltrd 
 |-  ( ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) /\ j = ( 0g ` ( Scalar ` W ) ) ) -> X e. ( N ` { Z } ) )
61 eldifsni 
 |-  ( X e. ( V \ { .0. } ) -> X =/= .0. )
62 23 61 syl 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> X =/= .0. )
63 62 adantr 
 |-  ( ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) /\ j = ( 0g ` ( Scalar ` W ) ) ) -> X =/= .0. )
64 1 2 3 45 46 60 63 lspsneleq 
 |-  ( ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) /\ j = ( 0g ` ( Scalar ` W ) ) ) -> ( N ` { X } ) = ( N ` { Z } ) )
65 64 ex 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( j = ( 0g ` ( Scalar ` W ) ) -> ( N ` { X } ) = ( N ` { Z } ) ) )
66 65 necon3d 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( N ` { X } ) =/= ( N ` { Z } ) -> j =/= ( 0g ` ( Scalar ` W ) ) ) )
67 44 66 mpd 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> j =/= ( 0g ` ( Scalar ` W ) ) )
68 eldifsn 
 |-  ( j e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) <-> ( j e. ( Base ` ( Scalar ` W ) ) /\ j =/= ( 0g ` ( Scalar ` W ) ) ) )
69 34 67 68 sylanbrc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> j e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) )
70 11 lmodfgrp 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Grp )
71 29 70 syl 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( Scalar ` W ) e. Grp )
72 12 19 grpinvcl 
 |-  ( ( ( Scalar ` W ) e. Grp /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( ( invg ` ( Scalar ` W ) ) ` k ) e. ( Base ` ( Scalar ` W ) ) )
73 71 22 72 syl2anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( invg ` ( Scalar ` W ) ) ` k ) e. ( Base ` ( Scalar ` W ) ) )
74 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ ( ( invg ` ( Scalar ` W ) ) ` k ) e. ( Base ` ( Scalar ` W ) ) /\ Z e. V ) -> ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) e. V )
75 21 73 25 74 syl3anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) e. V )
76 1 10 lmodvacl 
 |-  ( ( W e. LMod /\ X e. V /\ ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) e. V ) -> ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) e. V )
77 21 24 75 76 syl3anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) e. V )
78 1 13 11 12 42 43 20 69 77 35 lvecinv 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) = ( j ( .s ` W ) Y ) <-> Y = ( ( ( invr ` ( Scalar ` W ) ) ` j ) ( .s ` W ) ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) ) ) )
79 41 78 mpbid 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> Y = ( ( ( invr ` ( Scalar ` W ) ) ` j ) ( .s ` W ) ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) ) )
80 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
81 1 80 3 21 24 25 lspprcl 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( N ` { X , Z } ) e. ( LSubSp ` W ) )
82 11 lvecdrng 
 |-  ( W e. LVec -> ( Scalar ` W ) e. DivRing )
83 20 82 syl 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( Scalar ` W ) e. DivRing )
84 12 42 43 drnginvrcl 
 |-  ( ( ( Scalar ` W ) e. DivRing /\ j e. ( Base ` ( Scalar ` W ) ) /\ j =/= ( 0g ` ( Scalar ` W ) ) ) -> ( ( invr ` ( Scalar ` W ) ) ` j ) e. ( Base ` ( Scalar ` W ) ) )
85 83 34 67 84 syl3anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( invr ` ( Scalar ` W ) ) ` j ) e. ( Base ` ( Scalar ` W ) ) )
86 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
87 1 11 13 86 lmodvs1 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) X ) = X )
88 21 24 87 syl2anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) X ) = X )
89 88 oveq1d 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) X ) ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) = ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) )
90 11 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
91 12 86 ringidcl 
 |-  ( ( Scalar ` W ) e. Ring -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
92 21 90 91 3syl 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
93 1 10 13 11 12 3 21 92 73 24 25 lsppreli 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) X ) ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) e. ( N ` { X , Z } ) )
94 89 93 eqeltrrd 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) e. ( N ` { X , Z } ) )
95 11 13 12 80 lssvscl 
 |-  ( ( ( W e. LMod /\ ( N ` { X , Z } ) e. ( LSubSp ` W ) ) /\ ( ( ( invr ` ( Scalar ` W ) ) ` j ) e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) e. ( N ` { X , Z } ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` j ) ( .s ` W ) ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) ) e. ( N ` { X , Z } ) )
96 21 81 85 94 95 syl22anc 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` j ) ( .s ` W ) ( X ( +g ` W ) ( ( ( invg ` ( Scalar ` W ) ) ` k ) ( .s ` W ) Z ) ) ) e. ( N ` { X , Z } ) )
97 79 96 eqeltrd 
 |-  ( ( ph /\ ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) ) -> Y e. ( N ` { X , Z } ) )
98 97 3exp 
 |-  ( ph -> ( ( j e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) ) -> ( X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) -> Y e. ( N ` { X , Z } ) ) ) )
99 98 rexlimdvv 
 |-  ( ph -> ( E. j e. ( Base ` ( Scalar ` W ) ) E. k e. ( Base ` ( Scalar ` W ) ) X = ( ( j ( .s ` W ) Y ) ( +g ` W ) ( k ( .s ` W ) Z ) ) -> Y e. ( N ` { X , Z } ) ) )
100 17 99 mpd 
 |-  ( ph -> Y e. ( N ` { X , Z } ) )