Metamath Proof Explorer

Theorem linds2eq

Description: Deduce equality of elements in an independent set. (Contributed by Thierry Arnoux, 18-Jul-2023)

Ref Expression
Hypotheses linds2eq.1 
|- F = ( Base ` ( Scalar ` W ) )
linds2eq.2 
|- .x. = ( .s ` W )
linds2eq.3 
|- .+ = ( +g ` W )
linds2eq.4 
|- .0. = ( 0g ` ( Scalar ` W ) )
linds2eq.5 
|- ( ph -> W e. LVec )
linds2eq.6 
|- ( ph -> B e. ( LIndS ` W ) )
linds2eq.7 
|- ( ph -> X e. B )
linds2eq.8 
|- ( ph -> Y e. B )
linds2eq.9 
|- ( ph -> K e. F )
linds2eq.10 
|- ( ph -> L e. F )
linds2eq.11 
|- ( ph -> K =/= .0. )
linds2eq.12 
|- ( ph -> ( K .x. X ) = ( L .x. Y ) )
Assertion linds2eq 
|- ( ph -> ( X = Y /\ K = L ) )

Proof

Step Hyp Ref Expression
1 linds2eq.1 
 |-  F = ( Base ` ( Scalar ` W ) )
2 linds2eq.2 
 |-  .x. = ( .s ` W )
3 linds2eq.3 
 |-  .+ = ( +g ` W )
4 linds2eq.4 
 |-  .0. = ( 0g ` ( Scalar ` W ) )
5 linds2eq.5 
 |-  ( ph -> W e. LVec )
6 linds2eq.6 
 |-  ( ph -> B e. ( LIndS ` W ) )
7 linds2eq.7 
 |-  ( ph -> X e. B )
8 linds2eq.8 
 |-  ( ph -> Y e. B )
9 linds2eq.9 
 |-  ( ph -> K e. F )
10 linds2eq.10 
 |-  ( ph -> L e. F )
11 linds2eq.11 
 |-  ( ph -> K =/= .0. )
12 linds2eq.12 
 |-  ( ph -> ( K .x. X ) = ( L .x. Y ) )
13 simpr 
 |-  ( ( ph /\ X = Y ) -> X = Y )
14 12 adantr 
 |-  ( ( ph /\ X = Y ) -> ( K .x. X ) = ( L .x. Y ) )
15 13 oveq2d 
 |-  ( ( ph /\ X = Y ) -> ( L .x. X ) = ( L .x. Y ) )
16 14 15 eqtr4d 
 |-  ( ( ph /\ X = Y ) -> ( K .x. X ) = ( L .x. X ) )
17 eqid 
 |-  ( Base ` W ) = ( Base ` W )
18 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
19 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
20 5 adantr 
 |-  ( ( ph /\ X = Y ) -> W e. LVec )
21 9 adantr 
 |-  ( ( ph /\ X = Y ) -> K e. F )
22 10 adantr 
 |-  ( ( ph /\ X = Y ) -> L e. F )
23 17 linds1 
 |-  ( B e. ( LIndS ` W ) -> B C_ ( Base ` W ) )
24 6 23 syl 
 |-  ( ph -> B C_ ( Base ` W ) )
25 24 7 sseldd 
 |-  ( ph -> X e. ( Base ` W ) )
26 25 adantr 
 |-  ( ( ph /\ X = Y ) -> X e. ( Base ` W ) )
27 19 0nellinds 
 |-  ( ( W e. LVec /\ B e. ( LIndS ` W ) ) -> -. ( 0g ` W ) e. B )
28 5 6 27 syl2anc 
 |-  ( ph -> -. ( 0g ` W ) e. B )
29 nelne2 
 |-  ( ( X e. B /\ -. ( 0g ` W ) e. B ) -> X =/= ( 0g ` W ) )
30 7 28 29 syl2anc 
 |-  ( ph -> X =/= ( 0g ` W ) )
31 30 adantr 
 |-  ( ( ph /\ X = Y ) -> X =/= ( 0g ` W ) )
32 17 2 18 1 19 20 21 22 26 31 lvecvscan2 
 |-  ( ( ph /\ X = Y ) -> ( ( K .x. X ) = ( L .x. X ) <-> K = L ) )
33 16 32 mpbid 
 |-  ( ( ph /\ X = Y ) -> K = L )
34 13 33 jca 
 |-  ( ( ph /\ X = Y ) -> ( X = Y /\ K = L ) )
35 7 adantr 
 |-  ( ( ph /\ X =/= Y ) -> X e. B )
36 9 adantr 
 |-  ( ( ph /\ X =/= Y ) -> K e. F )
37 opex 
 |-  <. X , K >. e. _V
38 37 a1i 
 |-  ( ( ph /\ X =/= Y ) -> <. X , K >. e. _V )
39 opex 
 |-  <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. e. _V
40 39 a1i 
 |-  ( ( ph /\ X =/= Y ) -> <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. e. _V )
41 animorrl 
 |-  ( ( ph /\ X =/= Y ) -> ( X =/= Y \/ K =/= ( ( invg ` ( Scalar ` W ) ) ` L ) ) )
42 opthneg 
 |-  ( ( X e. B /\ K e. F ) -> ( <. X , K >. =/= <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. <-> ( X =/= Y \/ K =/= ( ( invg ` ( Scalar ` W ) ) ` L ) ) ) )
43 42 biimpar 
 |-  ( ( ( X e. B /\ K e. F ) /\ ( X =/= Y \/ K =/= ( ( invg ` ( Scalar ` W ) ) ` L ) ) ) -> <. X , K >. =/= <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. )
44 35 36 41 43 syl21anc 
 |-  ( ( ph /\ X =/= Y ) -> <. X , K >. =/= <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. )
45 animorrl 
 |-  ( ( ph /\ X =/= Y ) -> ( X =/= Y \/ K =/= .0. ) )
46 opthneg 
 |-  ( ( X e. B /\ K e. F ) -> ( <. X , K >. =/= <. Y , .0. >. <-> ( X =/= Y \/ K =/= .0. ) ) )
47 46 biimpar 
 |-  ( ( ( X e. B /\ K e. F ) /\ ( X =/= Y \/ K =/= .0. ) ) -> <. X , K >. =/= <. Y , .0. >. )
48 35 36 45 47 syl21anc 
 |-  ( ( ph /\ X =/= Y ) -> <. X , K >. =/= <. Y , .0. >. )
49 44 48 jca 
 |-  ( ( ph /\ X =/= Y ) -> ( <. X , K >. =/= <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. /\ <. X , K >. =/= <. Y , .0. >. ) )
50 8 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Y e. B )
51 fvexd 
 |-  ( ( ph /\ X =/= Y ) -> ( ( invg ` ( Scalar ` W ) ) ` L ) e. _V )
52 simpr 
 |-  ( ( ph /\ X =/= Y ) -> X =/= Y )
53 fprg 
 |-  ( ( ( X e. B /\ Y e. B ) /\ ( K e. F /\ ( ( invg ` ( Scalar ` W ) ) ` L ) e. _V ) /\ X =/= Y ) -> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } : { X , Y } --> { K , ( ( invg ` ( Scalar ` W ) ) ` L ) } )
54 35 50 36 51 52 53 syl221anc 
 |-  ( ( ph /\ X =/= Y ) -> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } : { X , Y } --> { K , ( ( invg ` ( Scalar ` W ) ) ` L ) } )
55 prfi 
 |-  { X , Y } e. Fin
56 55 a1i 
 |-  ( ( ph /\ X =/= Y ) -> { X , Y } e. Fin )
57 4 fvexi 
 |-  .0. e. _V
58 57 a1i 
 |-  ( ( ph /\ X =/= Y ) -> .0. e. _V )
59 54 56 58 fdmfifsupp 
 |-  ( ( ph /\ X =/= Y ) -> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } finSupp .0. )
60 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
61 5 60 syl 
 |-  ( ph -> W e. LMod )
62 lmodcmn 
 |-  ( W e. LMod -> W e. CMnd )
63 61 62 syl 
 |-  ( ph -> W e. CMnd )
64 63 adantr 
 |-  ( ( ph /\ X =/= Y ) -> W e. CMnd )
65 61 adantr 
 |-  ( ( ph /\ X =/= Y ) -> W e. LMod )
66 18 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
67 ringgrp 
 |-  ( ( Scalar ` W ) e. Ring -> ( Scalar ` W ) e. Grp )
68 61 66 67 3syl 
 |-  ( ph -> ( Scalar ` W ) e. Grp )
69 eqid 
 |-  ( invg ` ( Scalar ` W ) ) = ( invg ` ( Scalar ` W ) )
70 1 69 grpinvcl 
 |-  ( ( ( Scalar ` W ) e. Grp /\ L e. F ) -> ( ( invg ` ( Scalar ` W ) ) ` L ) e. F )
71 68 10 70 syl2anc 
 |-  ( ph -> ( ( invg ` ( Scalar ` W ) ) ` L ) e. F )
72 9 71 prssd 
 |-  ( ph -> { K , ( ( invg ` ( Scalar ` W ) ) ` L ) } C_ F )
73 72 adantr 
 |-  ( ( ph /\ X =/= Y ) -> { K , ( ( invg ` ( Scalar ` W ) ) ` L ) } C_ F )
74 54 73 fssd 
 |-  ( ( ph /\ X =/= Y ) -> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } : { X , Y } --> F )
75 eqidd 
 |-  ( ( ph /\ X =/= Y ) -> X = X )
76 75 orcd 
 |-  ( ( ph /\ X =/= Y ) -> ( X = X \/ X = Y ) )
77 elprg 
 |-  ( X e. B -> ( X e. { X , Y } <-> ( X = X \/ X = Y ) ) )
78 77 biimpar 
 |-  ( ( X e. B /\ ( X = X \/ X = Y ) ) -> X e. { X , Y } )
79 35 76 78 syl2anc 
 |-  ( ( ph /\ X =/= Y ) -> X e. { X , Y } )
80 74 79 ffvelcdmd 
 |-  ( ( ph /\ X =/= Y ) -> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) e. F )
81 25 adantr 
 |-  ( ( ph /\ X =/= Y ) -> X e. ( Base ` W ) )
82 17 18 2 1 lmodvscl 
 |-  ( ( W e. LMod /\ ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) e. F /\ X e. ( Base ` W ) ) -> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) .x. X ) e. ( Base ` W ) )
83 65 80 81 82 syl3anc 
 |-  ( ( ph /\ X =/= Y ) -> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) .x. X ) e. ( Base ` W ) )
84 eqidd 
 |-  ( ( ph /\ X =/= Y ) -> Y = Y )
85 84 olcd 
 |-  ( ( ph /\ X =/= Y ) -> ( Y = X \/ Y = Y ) )
86 elprg 
 |-  ( Y e. B -> ( Y e. { X , Y } <-> ( Y = X \/ Y = Y ) ) )
87 86 biimpar 
 |-  ( ( Y e. B /\ ( Y = X \/ Y = Y ) ) -> Y e. { X , Y } )
88 50 85 87 syl2anc 
 |-  ( ( ph /\ X =/= Y ) -> Y e. { X , Y } )
89 74 88 ffvelcdmd 
 |-  ( ( ph /\ X =/= Y ) -> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) e. F )
90 24 8 sseldd 
 |-  ( ph -> Y e. ( Base ` W ) )
91 90 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Y e. ( Base ` W ) )
92 17 18 2 1 lmodvscl 
 |-  ( ( W e. LMod /\ ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) e. F /\ Y e. ( Base ` W ) ) -> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) .x. Y ) e. ( Base ` W ) )
93 65 89 91 92 syl3anc 
 |-  ( ( ph /\ X =/= Y ) -> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) .x. Y ) e. ( Base ` W ) )
94 fveq2 
 |-  ( b = X -> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) = ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) )
95 id 
 |-  ( b = X -> b = X )
96 94 95 oveq12d 
 |-  ( b = X -> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) = ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) .x. X ) )
97 fveq2 
 |-  ( b = Y -> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) = ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) )
98 id 
 |-  ( b = Y -> b = Y )
99 97 98 oveq12d 
 |-  ( b = Y -> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) = ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) .x. Y ) )
100 17 3 96 99 gsumpr 
 |-  ( ( W e. CMnd /\ ( X e. B /\ Y e. B /\ X =/= Y ) /\ ( ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) .x. X ) e. ( Base ` W ) /\ ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) .x. Y ) e. ( Base ` W ) ) ) -> ( W gsum ( b e. { X , Y } |-> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) ) ) = ( ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) .x. X ) .+ ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) .x. Y ) ) )
101 64 35 50 52 83 93 100 syl132anc 
 |-  ( ( ph /\ X =/= Y ) -> ( W gsum ( b e. { X , Y } |-> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) ) ) = ( ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) .x. X ) .+ ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) .x. Y ) ) )
102 fvpr1g 
 |-  ( ( X e. B /\ K e. F /\ X =/= Y ) -> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) = K )
103 35 36 52 102 syl3anc 
 |-  ( ( ph /\ X =/= Y ) -> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) = K )
104 103 oveq1d 
 |-  ( ( ph /\ X =/= Y ) -> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) .x. X ) = ( K .x. X ) )
105 71 adantr 
 |-  ( ( ph /\ X =/= Y ) -> ( ( invg ` ( Scalar ` W ) ) ` L ) e. F )
106 fvpr2g 
 |-  ( ( Y e. B /\ ( ( invg ` ( Scalar ` W ) ) ` L ) e. F /\ X =/= Y ) -> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) = ( ( invg ` ( Scalar ` W ) ) ` L ) )
107 50 105 52 106 syl3anc 
 |-  ( ( ph /\ X =/= Y ) -> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) = ( ( invg ` ( Scalar ` W ) ) ` L ) )
108 107 oveq1d 
 |-  ( ( ph /\ X =/= Y ) -> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) .x. Y ) = ( ( ( invg ` ( Scalar ` W ) ) ` L ) .x. Y ) )
109 104 108 oveq12d 
 |-  ( ( ph /\ X =/= Y ) -> ( ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` X ) .x. X ) .+ ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` Y ) .x. Y ) ) = ( ( K .x. X ) .+ ( ( ( invg ` ( Scalar ` W ) ) ` L ) .x. Y ) ) )
110 17 18 2 1 lmodvscl 
 |-  ( ( W e. LMod /\ K e. F /\ X e. ( Base ` W ) ) -> ( K .x. X ) e. ( Base ` W ) )
111 61 9 25 110 syl3anc 
 |-  ( ph -> ( K .x. X ) e. ( Base ` W ) )
112 12 111 eqeltrrd 
 |-  ( ph -> ( L .x. Y ) e. ( Base ` W ) )
113 eqid 
 |-  ( invg ` W ) = ( invg ` W )
114 eqid 
 |-  ( -g ` W ) = ( -g ` W )
115 17 3 113 114 grpsubval 
 |-  ( ( ( K .x. X ) e. ( Base ` W ) /\ ( L .x. Y ) e. ( Base ` W ) ) -> ( ( K .x. X ) ( -g ` W ) ( L .x. Y ) ) = ( ( K .x. X ) .+ ( ( invg ` W ) ` ( L .x. Y ) ) ) )
116 111 112 115 syl2anc 
 |-  ( ph -> ( ( K .x. X ) ( -g ` W ) ( L .x. Y ) ) = ( ( K .x. X ) .+ ( ( invg ` W ) ` ( L .x. Y ) ) ) )
117 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
118 61 117 syl 
 |-  ( ph -> W e. Grp )
119 17 19 114 grpsubeq0 
 |-  ( ( W e. Grp /\ ( K .x. X ) e. ( Base ` W ) /\ ( L .x. Y ) e. ( Base ` W ) ) -> ( ( ( K .x. X ) ( -g ` W ) ( L .x. Y ) ) = ( 0g ` W ) <-> ( K .x. X ) = ( L .x. Y ) ) )
120 118 111 112 119 syl3anc 
 |-  ( ph -> ( ( ( K .x. X ) ( -g ` W ) ( L .x. Y ) ) = ( 0g ` W ) <-> ( K .x. X ) = ( L .x. Y ) ) )
121 12 120 mpbird 
 |-  ( ph -> ( ( K .x. X ) ( -g ` W ) ( L .x. Y ) ) = ( 0g ` W ) )
122 17 18 2 113 1 69 61 90 10 lmodvsneg 
 |-  ( ph -> ( ( invg ` W ) ` ( L .x. Y ) ) = ( ( ( invg ` ( Scalar ` W ) ) ` L ) .x. Y ) )
123 122 oveq2d 
 |-  ( ph -> ( ( K .x. X ) .+ ( ( invg ` W ) ` ( L .x. Y ) ) ) = ( ( K .x. X ) .+ ( ( ( invg ` ( Scalar ` W ) ) ` L ) .x. Y ) ) )
124 116 121 123 3eqtr3rd 
 |-  ( ph -> ( ( K .x. X ) .+ ( ( ( invg ` ( Scalar ` W ) ) ` L ) .x. Y ) ) = ( 0g ` W ) )
125 124 adantr 
 |-  ( ( ph /\ X =/= Y ) -> ( ( K .x. X ) .+ ( ( ( invg ` ( Scalar ` W ) ) ` L ) .x. Y ) ) = ( 0g ` W ) )
126 101 109 125 3eqtrd 
 |-  ( ( ph /\ X =/= Y ) -> ( W gsum ( b e. { X , Y } |-> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) ) ) = ( 0g ` W ) )
127 breq1 
 |-  ( a = { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } -> ( a finSupp .0. <-> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } finSupp .0. ) )
128 fveq1 
 |-  ( a = { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } -> ( a ` b ) = ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) )
129 128 oveq1d 
 |-  ( a = { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } -> ( ( a ` b ) .x. b ) = ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) )
130 129 mpteq2dv 
 |-  ( a = { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } -> ( b e. { X , Y } |-> ( ( a ` b ) .x. b ) ) = ( b e. { X , Y } |-> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) ) )
131 130 oveq2d 
 |-  ( a = { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } -> ( W gsum ( b e. { X , Y } |-> ( ( a ` b ) .x. b ) ) ) = ( W gsum ( b e. { X , Y } |-> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) ) ) )
132 131 eqeq1d 
 |-  ( a = { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } -> ( ( W gsum ( b e. { X , Y } |-> ( ( a ` b ) .x. b ) ) ) = ( 0g ` W ) <-> ( W gsum ( b e. { X , Y } |-> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) ) ) = ( 0g ` W ) ) )
133 127 132 anbi12d 
 |-  ( a = { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } -> ( ( a finSupp .0. /\ ( W gsum ( b e. { X , Y } |-> ( ( a ` b ) .x. b ) ) ) = ( 0g ` W ) ) <-> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } finSupp .0. /\ ( W gsum ( b e. { X , Y } |-> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) ) ) = ( 0g ` W ) ) ) )
134 eqeq1 
 |-  ( a = { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } -> ( a = ( { X , Y } X. { .0. } ) <-> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } = ( { X , Y } X. { .0. } ) ) )
135 133 134 imbi12d 
 |-  ( a = { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } -> ( ( ( a finSupp .0. /\ ( W gsum ( b e. { X , Y } |-> ( ( a ` b ) .x. b ) ) ) = ( 0g ` W ) ) -> a = ( { X , Y } X. { .0. } ) ) <-> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } finSupp .0. /\ ( W gsum ( b e. { X , Y } |-> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) ) ) = ( 0g ` W ) ) -> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } = ( { X , Y } X. { .0. } ) ) ) )
136 7 8 prssd 
 |-  ( ph -> { X , Y } C_ B )
137 136 24 sstrd 
 |-  ( ph -> { X , Y } C_ ( Base ` W ) )
138 lindsss 
 |-  ( ( W e. LMod /\ B e. ( LIndS ` W ) /\ { X , Y } C_ B ) -> { X , Y } e. ( LIndS ` W ) )
139 61 6 136 138 syl3anc 
 |-  ( ph -> { X , Y } e. ( LIndS ` W ) )
140 17 1 18 2 19 4 islinds5 
 |-  ( ( W e. LMod /\ { X , Y } C_ ( Base ` W ) ) -> ( { X , Y } e. ( LIndS ` W ) <-> A. a e. ( F ^m { X , Y } ) ( ( a finSupp .0. /\ ( W gsum ( b e. { X , Y } |-> ( ( a ` b ) .x. b ) ) ) = ( 0g ` W ) ) -> a = ( { X , Y } X. { .0. } ) ) ) )
141 140 biimpa 
 |-  ( ( ( W e. LMod /\ { X , Y } C_ ( Base ` W ) ) /\ { X , Y } e. ( LIndS ` W ) ) -> A. a e. ( F ^m { X , Y } ) ( ( a finSupp .0. /\ ( W gsum ( b e. { X , Y } |-> ( ( a ` b ) .x. b ) ) ) = ( 0g ` W ) ) -> a = ( { X , Y } X. { .0. } ) ) )
142 61 137 139 141 syl21anc 
 |-  ( ph -> A. a e. ( F ^m { X , Y } ) ( ( a finSupp .0. /\ ( W gsum ( b e. { X , Y } |-> ( ( a ` b ) .x. b ) ) ) = ( 0g ` W ) ) -> a = ( { X , Y } X. { .0. } ) ) )
143 142 adantr 
 |-  ( ( ph /\ X =/= Y ) -> A. a e. ( F ^m { X , Y } ) ( ( a finSupp .0. /\ ( W gsum ( b e. { X , Y } |-> ( ( a ` b ) .x. b ) ) ) = ( 0g ` W ) ) -> a = ( { X , Y } X. { .0. } ) ) )
144 1 fvexi 
 |-  F e. _V
145 144 a1i 
 |-  ( ( ph /\ X =/= Y ) -> F e. _V )
146 139 elexd 
 |-  ( ph -> { X , Y } e. _V )
147 146 adantr 
 |-  ( ( ph /\ X =/= Y ) -> { X , Y } e. _V )
148 145 147 elmapd 
 |-  ( ( ph /\ X =/= Y ) -> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } e. ( F ^m { X , Y } ) <-> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } : { X , Y } --> F ) )
149 74 148 mpbird 
 |-  ( ( ph /\ X =/= Y ) -> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } e. ( F ^m { X , Y } ) )
150 135 143 149 rspcdva 
 |-  ( ( ph /\ X =/= Y ) -> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } finSupp .0. /\ ( W gsum ( b e. { X , Y } |-> ( ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } ` b ) .x. b ) ) ) = ( 0g ` W ) ) -> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } = ( { X , Y } X. { .0. } ) ) )
151 59 126 150 mp2and 
 |-  ( ( ph /\ X =/= Y ) -> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } = ( { X , Y } X. { .0. } ) )
152 xpprsng 
 |-  ( ( X e. B /\ Y e. B /\ .0. e. _V ) -> ( { X , Y } X. { .0. } ) = { <. X , .0. >. , <. Y , .0. >. } )
153 35 50 58 152 syl3anc 
 |-  ( ( ph /\ X =/= Y ) -> ( { X , Y } X. { .0. } ) = { <. X , .0. >. , <. Y , .0. >. } )
154 151 153 eqtrd 
 |-  ( ( ph /\ X =/= Y ) -> { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } = { <. X , .0. >. , <. Y , .0. >. } )
155 opthprneg 
 |-  ( ( ( <. X , K >. e. _V /\ <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. e. _V ) /\ ( <. X , K >. =/= <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. /\ <. X , K >. =/= <. Y , .0. >. ) ) -> ( { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } = { <. X , .0. >. , <. Y , .0. >. } <-> ( <. X , K >. = <. X , .0. >. /\ <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. = <. Y , .0. >. ) ) )
156 155 biimpa 
 |-  ( ( ( ( <. X , K >. e. _V /\ <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. e. _V ) /\ ( <. X , K >. =/= <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. /\ <. X , K >. =/= <. Y , .0. >. ) ) /\ { <. X , K >. , <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. } = { <. X , .0. >. , <. Y , .0. >. } ) -> ( <. X , K >. = <. X , .0. >. /\ <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. = <. Y , .0. >. ) )
157 38 40 49 154 156 syl1111anc 
 |-  ( ( ph /\ X =/= Y ) -> ( <. X , K >. = <. X , .0. >. /\ <. Y , ( ( invg ` ( Scalar ` W ) ) ` L ) >. = <. Y , .0. >. ) )
158 157 simpld 
 |-  ( ( ph /\ X =/= Y ) -> <. X , K >. = <. X , .0. >. )
159 opthg 
 |-  ( ( X e. B /\ K e. F ) -> ( <. X , K >. = <. X , .0. >. <-> ( X = X /\ K = .0. ) ) )
160 159 simplbda 
 |-  ( ( ( X e. B /\ K e. F ) /\ <. X , K >. = <. X , .0. >. ) -> K = .0. )
161 35 36 158 160 syl21anc 
 |-  ( ( ph /\ X =/= Y ) -> K = .0. )
162 11 adantr 
 |-  ( ( ph /\ X =/= Y ) -> K =/= .0. )
163 161 162 pm2.21ddne 
 |-  ( ( ph /\ X =/= Y ) -> ( X = Y /\ K = L ) )
164 34 163 pm2.61dane 
 |-  ( ph -> ( X = Y /\ K = L ) )