Metamath Proof Explorer


Theorem ldepspr

Description: If a vector is a scalar multiple of another vector, the (unordered pair containing the) two vectors are linearly dependent. (Contributed by AV, 16-Apr-2019) (Revised by AV, 27-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Hypotheses snlindsntor.b
|- B = ( Base ` M )
snlindsntor.r
|- R = ( Scalar ` M )
snlindsntor.s
|- S = ( Base ` R )
snlindsntor.0
|- .0. = ( 0g ` R )
snlindsntor.z
|- Z = ( 0g ` M )
snlindsntor.t
|- .x. = ( .s ` M )
Assertion ldepspr
|- ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> { X , Y } linDepS M ) )

Proof

Step Hyp Ref Expression
1 snlindsntor.b
 |-  B = ( Base ` M )
2 snlindsntor.r
 |-  R = ( Scalar ` M )
3 snlindsntor.s
 |-  S = ( Base ` R )
4 snlindsntor.0
 |-  .0. = ( 0g ` R )
5 snlindsntor.z
 |-  Z = ( 0g ` M )
6 snlindsntor.t
 |-  .x. = ( .s ` M )
7 3simpa
 |-  ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( X e. B /\ Y e. B ) )
8 7 ad2antlr
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( X e. B /\ Y e. B ) )
9 fvex
 |-  ( 1r ` R ) e. _V
10 fvex
 |-  ( ( invg ` R ) ` A ) e. _V
11 9 10 pm3.2i
 |-  ( ( 1r ` R ) e. _V /\ ( ( invg ` R ) ` A ) e. _V )
12 11 a1i
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( 1r ` R ) e. _V /\ ( ( invg ` R ) ` A ) e. _V ) )
13 simp3
 |-  ( ( X e. B /\ Y e. B /\ X =/= Y ) -> X =/= Y )
14 13 ad2antlr
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> X =/= Y )
15 fprg
 |-  ( ( ( X e. B /\ Y e. B ) /\ ( ( 1r ` R ) e. _V /\ ( ( invg ` R ) ` A ) e. _V ) /\ X =/= Y ) -> { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } : { X , Y } --> { ( 1r ` R ) , ( ( invg ` R ) ` A ) } )
16 8 12 14 15 syl3anc
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } : { X , Y } --> { ( 1r ` R ) , ( ( invg ` R ) ` A ) } )
17 prfi
 |-  { X , Y } e. Fin
18 17 a1i
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> { X , Y } e. Fin )
19 4 fvexi
 |-  .0. e. _V
20 19 a1i
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> .0. e. _V )
21 16 18 20 fdmfifsupp
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } finSupp .0. )
22 13 anim2i
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( M e. LMod /\ X =/= Y ) )
23 22 adantr
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( M e. LMod /\ X =/= Y ) )
24 eqid
 |-  ( 1r ` R ) = ( 1r ` R )
25 2 3 24 lmod1cl
 |-  ( M e. LMod -> ( 1r ` R ) e. S )
26 simp1
 |-  ( ( X e. B /\ Y e. B /\ X =/= Y ) -> X e. B )
27 25 26 anim12ci
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( X e. B /\ ( 1r ` R ) e. S ) )
28 27 adantr
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( X e. B /\ ( 1r ` R ) e. S ) )
29 simp2
 |-  ( ( X e. B /\ Y e. B /\ X =/= Y ) -> Y e. B )
30 29 ad2antlr
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> Y e. B )
31 2 lmodfgrp
 |-  ( M e. LMod -> R e. Grp )
32 31 adantr
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> R e. Grp )
33 simpl
 |-  ( ( A e. S /\ X = ( A .x. Y ) ) -> A e. S )
34 eqid
 |-  ( invg ` R ) = ( invg ` R )
35 3 34 grpinvcl
 |-  ( ( R e. Grp /\ A e. S ) -> ( ( invg ` R ) ` A ) e. S )
36 32 33 35 syl2an
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( invg ` R ) ` A ) e. S )
37 eqid
 |-  ( +g ` M ) = ( +g ` M )
38 eqid
 |-  { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } = { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. }
39 1 2 3 6 37 38 lincvalpr
 |-  ( ( ( M e. LMod /\ X =/= Y ) /\ ( X e. B /\ ( 1r ` R ) e. S ) /\ ( Y e. B /\ ( ( invg ` R ) ` A ) e. S ) ) -> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ( linC ` M ) { X , Y } ) = ( ( ( 1r ` R ) .x. X ) ( +g ` M ) ( ( ( invg ` R ) ` A ) .x. Y ) ) )
40 23 28 30 36 39 syl112anc
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ( linC ` M ) { X , Y } ) = ( ( ( 1r ` R ) .x. X ) ( +g ` M ) ( ( ( invg ` R ) ` A ) .x. Y ) ) )
41 simpll
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> M e. LMod )
42 26 ad2antlr
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> X e. B )
43 33 adantl
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> A e. S )
44 42 30 43 3jca
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( X e. B /\ Y e. B /\ A e. S ) )
45 41 44 jca
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) )
46 simprr
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> X = ( A .x. Y ) )
47 1 2 3 4 5 6 24 34 ldepsprlem
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ A e. S ) ) -> ( X = ( A .x. Y ) -> ( ( ( 1r ` R ) .x. X ) ( +g ` M ) ( ( ( invg ` R ) ` A ) .x. Y ) ) = Z ) )
48 45 46 47 sylc
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( ( 1r ` R ) .x. X ) ( +g ` M ) ( ( ( invg ` R ) ` A ) .x. Y ) ) = Z )
49 40 48 eqtrd
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ( linC ` M ) { X , Y } ) = Z )
50 2 lmodring
 |-  ( M e. LMod -> R e. Ring )
51 eqcom
 |-  ( ( 1r ` R ) = ( 0g ` R ) <-> ( 0g ` R ) = ( 1r ` R ) )
52 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
53 3 52 24 01eq0ring
 |-  ( ( R e. Ring /\ ( 0g ` R ) = ( 1r ` R ) ) -> S = { ( 0g ` R ) } )
54 sneq
 |-  ( ( 0g ` R ) = ( 1r ` R ) -> { ( 0g ` R ) } = { ( 1r ` R ) } )
55 54 eqeq2d
 |-  ( ( 0g ` R ) = ( 1r ` R ) -> ( S = { ( 0g ` R ) } <-> S = { ( 1r ` R ) } ) )
56 eleq2
 |-  ( S = { ( 1r ` R ) } -> ( A e. S <-> A e. { ( 1r ` R ) } ) )
57 elsni
 |-  ( A e. { ( 1r ` R ) } -> A = ( 1r ` R ) )
58 oveq1
 |-  ( A = ( 1r ` R ) -> ( A .x. Y ) = ( ( 1r ` R ) .x. Y ) )
59 58 eqeq2d
 |-  ( A = ( 1r ` R ) -> ( X = ( A .x. Y ) <-> X = ( ( 1r ` R ) .x. Y ) ) )
60 29 anim1i
 |-  ( ( ( X e. B /\ Y e. B /\ X =/= Y ) /\ M e. LMod ) -> ( Y e. B /\ M e. LMod ) )
61 60 ancomd
 |-  ( ( ( X e. B /\ Y e. B /\ X =/= Y ) /\ M e. LMod ) -> ( M e. LMod /\ Y e. B ) )
62 1 2 6 24 lmodvs1
 |-  ( ( M e. LMod /\ Y e. B ) -> ( ( 1r ` R ) .x. Y ) = Y )
63 61 62 syl
 |-  ( ( ( X e. B /\ Y e. B /\ X =/= Y ) /\ M e. LMod ) -> ( ( 1r ` R ) .x. Y ) = Y )
64 63 eqeq2d
 |-  ( ( ( X e. B /\ Y e. B /\ X =/= Y ) /\ M e. LMod ) -> ( X = ( ( 1r ` R ) .x. Y ) <-> X = Y ) )
65 eqneqall
 |-  ( X = Y -> ( X =/= Y -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) )
66 65 com12
 |-  ( X =/= Y -> ( X = Y -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) )
67 66 3ad2ant3
 |-  ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( X = Y -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) )
68 67 adantr
 |-  ( ( ( X e. B /\ Y e. B /\ X =/= Y ) /\ M e. LMod ) -> ( X = Y -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) )
69 64 68 sylbid
 |-  ( ( ( X e. B /\ Y e. B /\ X =/= Y ) /\ M e. LMod ) -> ( X = ( ( 1r ` R ) .x. Y ) -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) )
70 69 ex
 |-  ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( M e. LMod -> ( X = ( ( 1r ` R ) .x. Y ) -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) )
71 70 com3r
 |-  ( X = ( ( 1r ` R ) .x. Y ) -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) )
72 59 71 syl6bi
 |-  ( A = ( 1r ` R ) -> ( X = ( A .x. Y ) -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) )
73 57 72 syl
 |-  ( A e. { ( 1r ` R ) } -> ( X = ( A .x. Y ) -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) )
74 56 73 syl6bi
 |-  ( S = { ( 1r ` R ) } -> ( A e. S -> ( X = ( A .x. Y ) -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) ) )
75 74 impd
 |-  ( S = { ( 1r ` R ) } -> ( ( A e. S /\ X = ( A .x. Y ) ) -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) )
76 75 com23
 |-  ( S = { ( 1r ` R ) } -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) )
77 55 76 syl6bi
 |-  ( ( 0g ` R ) = ( 1r ` R ) -> ( S = { ( 0g ` R ) } -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) ) )
78 77 adantl
 |-  ( ( R e. Ring /\ ( 0g ` R ) = ( 1r ` R ) ) -> ( S = { ( 0g ` R ) } -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) ) )
79 53 78 mpd
 |-  ( ( R e. Ring /\ ( 0g ` R ) = ( 1r ` R ) ) -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) )
80 79 ex
 |-  ( R e. Ring -> ( ( 0g ` R ) = ( 1r ` R ) -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) ) )
81 51 80 syl5bi
 |-  ( R e. Ring -> ( ( 1r ` R ) = ( 0g ` R ) -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> ( M e. LMod -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) ) )
82 81 com25
 |-  ( R e. Ring -> ( M e. LMod -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> ( ( 1r ` R ) = ( 0g ` R ) -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) ) )
83 50 82 mpcom
 |-  ( M e. LMod -> ( ( X e. B /\ Y e. B /\ X =/= Y ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> ( ( 1r ` R ) = ( 0g ` R ) -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) ) ) )
84 83 imp31
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( 1r ` R ) = ( 0g ` R ) -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) ) )
85 orc
 |-  ( -. ( 1r ` R ) = ( 0g ` R ) -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) )
86 84 85 pm2.61d1
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) )
87 4 eqeq2i
 |-  ( ( 1r ` R ) = .0. <-> ( 1r ` R ) = ( 0g ` R ) )
88 87 necon3abii
 |-  ( ( 1r ` R ) =/= .0. <-> -. ( 1r ` R ) = ( 0g ` R ) )
89 88 orbi1i
 |-  ( ( ( 1r ` R ) =/= .0. \/ ( ( invg ` R ) ` A ) =/= .0. ) <-> ( -. ( 1r ` R ) = ( 0g ` R ) \/ ( ( invg ` R ) ` A ) =/= .0. ) )
90 86 89 sylibr
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( 1r ` R ) =/= .0. \/ ( ( invg ` R ) ` A ) =/= .0. ) )
91 fvexd
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( 1r ` R ) e. _V )
92 fvpr1g
 |-  ( ( X e. B /\ ( 1r ` R ) e. _V /\ X =/= Y ) -> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` X ) = ( 1r ` R ) )
93 42 91 14 92 syl3anc
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` X ) = ( 1r ` R ) )
94 93 neeq1d
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` X ) =/= .0. <-> ( 1r ` R ) =/= .0. ) )
95 fvexd
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( invg ` R ) ` A ) e. _V )
96 fvpr2g
 |-  ( ( Y e. B /\ ( ( invg ` R ) ` A ) e. _V /\ X =/= Y ) -> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` Y ) = ( ( invg ` R ) ` A ) )
97 30 95 14 96 syl3anc
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` Y ) = ( ( invg ` R ) ` A ) )
98 97 neeq1d
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` Y ) =/= .0. <-> ( ( invg ` R ) ` A ) =/= .0. ) )
99 94 98 orbi12d
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` X ) =/= .0. \/ ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` Y ) =/= .0. ) <-> ( ( 1r ` R ) =/= .0. \/ ( ( invg ` R ) ` A ) =/= .0. ) ) )
100 90 99 mpbird
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` X ) =/= .0. \/ ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` Y ) =/= .0. ) )
101 fveq2
 |-  ( v = X -> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) = ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` X ) )
102 101 neeq1d
 |-  ( v = X -> ( ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) =/= .0. <-> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` X ) =/= .0. ) )
103 fveq2
 |-  ( v = Y -> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) = ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` Y ) )
104 103 neeq1d
 |-  ( v = Y -> ( ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) =/= .0. <-> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` Y ) =/= .0. ) )
105 102 104 rexprg
 |-  ( ( X e. B /\ Y e. B ) -> ( E. v e. { X , Y } ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) =/= .0. <-> ( ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` X ) =/= .0. \/ ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` Y ) =/= .0. ) ) )
106 8 105 syl
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( E. v e. { X , Y } ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) =/= .0. <-> ( ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` X ) =/= .0. \/ ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` Y ) =/= .0. ) ) )
107 100 106 mpbird
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> E. v e. { X , Y } ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) =/= .0. )
108 25 adantr
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( 1r ` R ) e. S )
109 108 adantr
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( 1r ` R ) e. S )
110 3 fvexi
 |-  S e. _V
111 14 110 jctir
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( X =/= Y /\ S e. _V ) )
112 38 mapprop
 |-  ( ( ( X e. B /\ ( 1r ` R ) e. S ) /\ ( Y e. B /\ ( ( invg ` R ) ` A ) e. S ) /\ ( X =/= Y /\ S e. _V ) ) -> { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } e. ( S ^m { X , Y } ) )
113 42 109 30 36 111 112 syl221anc
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } e. ( S ^m { X , Y } ) )
114 breq1
 |-  ( f = { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } -> ( f finSupp .0. <-> { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } finSupp .0. ) )
115 oveq1
 |-  ( f = { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } -> ( f ( linC ` M ) { X , Y } ) = ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ( linC ` M ) { X , Y } ) )
116 115 eqeq1d
 |-  ( f = { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } -> ( ( f ( linC ` M ) { X , Y } ) = Z <-> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ( linC ` M ) { X , Y } ) = Z ) )
117 fveq1
 |-  ( f = { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } -> ( f ` v ) = ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) )
118 117 neeq1d
 |-  ( f = { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } -> ( ( f ` v ) =/= .0. <-> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) =/= .0. ) )
119 118 rexbidv
 |-  ( f = { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } -> ( E. v e. { X , Y } ( f ` v ) =/= .0. <-> E. v e. { X , Y } ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) =/= .0. ) )
120 114 116 119 3anbi123d
 |-  ( f = { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } -> ( ( f finSupp .0. /\ ( f ( linC ` M ) { X , Y } ) = Z /\ E. v e. { X , Y } ( f ` v ) =/= .0. ) <-> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } finSupp .0. /\ ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ( linC ` M ) { X , Y } ) = Z /\ E. v e. { X , Y } ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) =/= .0. ) ) )
121 120 adantl
 |-  ( ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) /\ f = { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ) -> ( ( f finSupp .0. /\ ( f ( linC ` M ) { X , Y } ) = Z /\ E. v e. { X , Y } ( f ` v ) =/= .0. ) <-> ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } finSupp .0. /\ ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ( linC ` M ) { X , Y } ) = Z /\ E. v e. { X , Y } ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) =/= .0. ) ) )
122 113 121 rspcedv
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } finSupp .0. /\ ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ( linC ` M ) { X , Y } ) = Z /\ E. v e. { X , Y } ( { <. X , ( 1r ` R ) >. , <. Y , ( ( invg ` R ) ` A ) >. } ` v ) =/= .0. ) -> E. f e. ( S ^m { X , Y } ) ( f finSupp .0. /\ ( f ( linC ` M ) { X , Y } ) = Z /\ E. v e. { X , Y } ( f ` v ) =/= .0. ) ) )
123 21 49 107 122 mp3and
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> E. f e. ( S ^m { X , Y } ) ( f finSupp .0. /\ ( f ( linC ` M ) { X , Y } ) = Z /\ E. v e. { X , Y } ( f ` v ) =/= .0. ) )
124 prelpwi
 |-  ( ( X e. B /\ Y e. B ) -> { X , Y } e. ~P B )
125 124 3adant3
 |-  ( ( X e. B /\ Y e. B /\ X =/= Y ) -> { X , Y } e. ~P B )
126 125 ad2antlr
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> { X , Y } e. ~P B )
127 1 5 2 3 4 islindeps
 |-  ( ( M e. LMod /\ { X , Y } e. ~P B ) -> ( { X , Y } linDepS M <-> E. f e. ( S ^m { X , Y } ) ( f finSupp .0. /\ ( f ( linC ` M ) { X , Y } ) = Z /\ E. v e. { X , Y } ( f ` v ) =/= .0. ) ) )
128 41 126 127 syl2anc
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> ( { X , Y } linDepS M <-> E. f e. ( S ^m { X , Y } ) ( f finSupp .0. /\ ( f ( linC ` M ) { X , Y } ) = Z /\ E. v e. { X , Y } ( f ` v ) =/= .0. ) ) )
129 123 128 mpbird
 |-  ( ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) /\ ( A e. S /\ X = ( A .x. Y ) ) ) -> { X , Y } linDepS M )
130 129 ex
 |-  ( ( M e. LMod /\ ( X e. B /\ Y e. B /\ X =/= Y ) ) -> ( ( A e. S /\ X = ( A .x. Y ) ) -> { X , Y } linDepS M ) )