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 ⊢ 𝐹 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
linds2eq.2 ⊢ · = ( ·𝑠 ‘ 𝑊 )
linds2eq.3 ⊢ + = ( +g ‘ 𝑊 )
linds2eq.4 ⊢ 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
linds2eq.5 ⊢ ( 𝜑 → 𝑊 ∈ LVec )
linds2eq.6 ⊢ ( 𝜑 → 𝐵 ∈ ( LIndS ‘ 𝑊 ) )
linds2eq.7 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
linds2eq.8 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
linds2eq.9 ⊢ ( 𝜑 → 𝐾 ∈ 𝐹 )
linds2eq.10 ⊢ ( 𝜑 → 𝐿 ∈ 𝐹 )
linds2eq.11 ⊢ ( 𝜑 → 𝐾 ≠ 0 )
linds2eq.12 ⊢ ( 𝜑 → ( 𝐾 · 𝑋 ) = ( 𝐿 · 𝑌 ) )
Assertion linds2eq ( 𝜑 → ( 𝑋 = 𝑌 ∧ 𝐾 = 𝐿 ) )

Proof

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