Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  linds2eq Structured version   Visualization version   GIF version

Theorem linds2eq 30998
Description: Deduce equality of elements in an independent set. (Contributed by Thierry Arnoux, 18-Jul-2023.)
Hypotheses
Ref Expression
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
Ref Expression
linds2eq (𝜑 → (𝑋 = 𝑌𝐾 = 𝐿))

Proof of Theorem linds2eq
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 488 . . 3 ((𝜑𝑋 = 𝑌) → 𝑋 = 𝑌)
2 linds2eq.12 . . . . . 6 (𝜑 → (𝐾 · 𝑋) = (𝐿 · 𝑌))
32adantr 484 . . . . 5 ((𝜑𝑋 = 𝑌) → (𝐾 · 𝑋) = (𝐿 · 𝑌))
41oveq2d 7155 . . . . 5 ((𝜑𝑋 = 𝑌) → (𝐿 · 𝑋) = (𝐿 · 𝑌))
53, 4eqtr4d 2839 . . . 4 ((𝜑𝑋 = 𝑌) → (𝐾 · 𝑋) = (𝐿 · 𝑋))
6 eqid 2801 . . . . 5 (Base‘𝑊) = (Base‘𝑊)
7 linds2eq.2 . . . . 5 · = ( ·𝑠𝑊)
8 eqid 2801 . . . . 5 (Scalar‘𝑊) = (Scalar‘𝑊)
9 linds2eq.1 . . . . 5 𝐹 = (Base‘(Scalar‘𝑊))
10 eqid 2801 . . . . 5 (0g𝑊) = (0g𝑊)
11 linds2eq.5 . . . . . 6 (𝜑𝑊 ∈ LVec)
1211adantr 484 . . . . 5 ((𝜑𝑋 = 𝑌) → 𝑊 ∈ LVec)
13 linds2eq.9 . . . . . 6 (𝜑𝐾𝐹)
1413adantr 484 . . . . 5 ((𝜑𝑋 = 𝑌) → 𝐾𝐹)
15 linds2eq.10 . . . . . 6 (𝜑𝐿𝐹)
1615adantr 484 . . . . 5 ((𝜑𝑋 = 𝑌) → 𝐿𝐹)
17 linds2eq.6 . . . . . . . 8 (𝜑𝐵 ∈ (LIndS‘𝑊))
186linds1 20502 . . . . . . . 8 (𝐵 ∈ (LIndS‘𝑊) → 𝐵 ⊆ (Base‘𝑊))
1917, 18syl 17 . . . . . . 7 (𝜑𝐵 ⊆ (Base‘𝑊))
20 linds2eq.7 . . . . . . 7 (𝜑𝑋𝐵)
2119, 20sseldd 3919 . . . . . 6 (𝜑𝑋 ∈ (Base‘𝑊))
2221adantr 484 . . . . 5 ((𝜑𝑋 = 𝑌) → 𝑋 ∈ (Base‘𝑊))
23100nellinds 30989 . . . . . . . 8 ((𝑊 ∈ LVec ∧ 𝐵 ∈ (LIndS‘𝑊)) → ¬ (0g𝑊) ∈ 𝐵)
2411, 17, 23syl2anc 587 . . . . . . 7 (𝜑 → ¬ (0g𝑊) ∈ 𝐵)
25 nelne2 3087 . . . . . . 7 ((𝑋𝐵 ∧ ¬ (0g𝑊) ∈ 𝐵) → 𝑋 ≠ (0g𝑊))
2620, 24, 25syl2anc 587 . . . . . 6 (𝜑𝑋 ≠ (0g𝑊))
2726adantr 484 . . . . 5 ((𝜑𝑋 = 𝑌) → 𝑋 ≠ (0g𝑊))
286, 7, 8, 9, 10, 12, 14, 16, 22, 27lvecvscan2 19880 . . . 4 ((𝜑𝑋 = 𝑌) → ((𝐾 · 𝑋) = (𝐿 · 𝑋) ↔ 𝐾 = 𝐿))
295, 28mpbid 235 . . 3 ((𝜑𝑋 = 𝑌) → 𝐾 = 𝐿)
301, 29jca 515 . 2 ((𝜑𝑋 = 𝑌) → (𝑋 = 𝑌𝐾 = 𝐿))
3120adantr 484 . . . 4 ((𝜑𝑋𝑌) → 𝑋𝐵)
3213adantr 484 . . . 4 ((𝜑𝑋𝑌) → 𝐾𝐹)
33 opex 5324 . . . . . . 7 𝑋, 𝐾⟩ ∈ V
3433a1i 11 . . . . . 6 ((𝜑𝑋𝑌) → ⟨𝑋, 𝐾⟩ ∈ V)
35 opex 5324 . . . . . . 7 𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ ∈ V
3635a1i 11 . . . . . 6 ((𝜑𝑋𝑌) → ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ ∈ V)
37 animorrl 978 . . . . . . . 8 ((𝜑𝑋𝑌) → (𝑋𝑌𝐾 ≠ ((invg‘(Scalar‘𝑊))‘𝐿)))
38 opthneg 5341 . . . . . . . . 9 ((𝑋𝐵𝐾𝐹) → (⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ ↔ (𝑋𝑌𝐾 ≠ ((invg‘(Scalar‘𝑊))‘𝐿))))
3938biimpar 481 . . . . . . . 8 (((𝑋𝐵𝐾𝐹) ∧ (𝑋𝑌𝐾 ≠ ((invg‘(Scalar‘𝑊))‘𝐿))) → ⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩)
4031, 32, 37, 39syl21anc 836 . . . . . . 7 ((𝜑𝑋𝑌) → ⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩)
41 animorrl 978 . . . . . . . 8 ((𝜑𝑋𝑌) → (𝑋𝑌𝐾0 ))
42 opthneg 5341 . . . . . . . . 9 ((𝑋𝐵𝐾𝐹) → (⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, 0 ⟩ ↔ (𝑋𝑌𝐾0 )))
4342biimpar 481 . . . . . . . 8 (((𝑋𝐵𝐾𝐹) ∧ (𝑋𝑌𝐾0 )) → ⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, 0 ⟩)
4431, 32, 41, 43syl21anc 836 . . . . . . 7 ((𝜑𝑋𝑌) → ⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, 0 ⟩)
4540, 44jca 515 . . . . . 6 ((𝜑𝑋𝑌) → (⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ ∧ ⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, 0 ⟩))
46 linds2eq.8 . . . . . . . . . . 11 (𝜑𝑌𝐵)
4746adantr 484 . . . . . . . . . 10 ((𝜑𝑋𝑌) → 𝑌𝐵)
48 fvexd 6664 . . . . . . . . . 10 ((𝜑𝑋𝑌) → ((invg‘(Scalar‘𝑊))‘𝐿) ∈ V)
49 simpr 488 . . . . . . . . . 10 ((𝜑𝑋𝑌) → 𝑋𝑌)
50 fprg 6898 . . . . . . . . . 10 (((𝑋𝐵𝑌𝐵) ∧ (𝐾𝐹 ∧ ((invg‘(Scalar‘𝑊))‘𝐿) ∈ V) ∧ 𝑋𝑌) → {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}:{𝑋, 𝑌}⟶{𝐾, ((invg‘(Scalar‘𝑊))‘𝐿)})
5131, 47, 32, 48, 49, 50syl221anc 1378 . . . . . . . . 9 ((𝜑𝑋𝑌) → {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}:{𝑋, 𝑌}⟶{𝐾, ((invg‘(Scalar‘𝑊))‘𝐿)})
52 prfi 8781 . . . . . . . . . 10 {𝑋, 𝑌} ∈ Fin
5352a1i 11 . . . . . . . . 9 ((𝜑𝑋𝑌) → {𝑋, 𝑌} ∈ Fin)
54 linds2eq.4 . . . . . . . . . . 11 0 = (0g‘(Scalar‘𝑊))
5554fvexi 6663 . . . . . . . . . 10 0 ∈ V
5655a1i 11 . . . . . . . . 9 ((𝜑𝑋𝑌) → 0 ∈ V)
5751, 53, 56fdmfifsupp 8831 . . . . . . . 8 ((𝜑𝑋𝑌) → {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} finSupp 0 )
58 lveclmod 19874 . . . . . . . . . . . . 13 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
5911, 58syl 17 . . . . . . . . . . . 12 (𝜑𝑊 ∈ LMod)
60 lmodcmn 19678 . . . . . . . . . . . 12 (𝑊 ∈ LMod → 𝑊 ∈ CMnd)
6159, 60syl 17 . . . . . . . . . . 11 (𝜑𝑊 ∈ CMnd)
6261adantr 484 . . . . . . . . . 10 ((𝜑𝑋𝑌) → 𝑊 ∈ CMnd)
6359adantr 484 . . . . . . . . . . 11 ((𝜑𝑋𝑌) → 𝑊 ∈ LMod)
648lmodring 19638 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ LMod → (Scalar‘𝑊) ∈ Ring)
65 ringgrp 19298 . . . . . . . . . . . . . . . . 17 ((Scalar‘𝑊) ∈ Ring → (Scalar‘𝑊) ∈ Grp)
6659, 64, 653syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (Scalar‘𝑊) ∈ Grp)
67 eqid 2801 . . . . . . . . . . . . . . . . 17 (invg‘(Scalar‘𝑊)) = (invg‘(Scalar‘𝑊))
689, 67grpinvcl 18146 . . . . . . . . . . . . . . . 16 (((Scalar‘𝑊) ∈ Grp ∧ 𝐿𝐹) → ((invg‘(Scalar‘𝑊))‘𝐿) ∈ 𝐹)
6966, 15, 68syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑 → ((invg‘(Scalar‘𝑊))‘𝐿) ∈ 𝐹)
7013, 69prssd 4718 . . . . . . . . . . . . . 14 (𝜑 → {𝐾, ((invg‘(Scalar‘𝑊))‘𝐿)} ⊆ 𝐹)
7170adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑋𝑌) → {𝐾, ((invg‘(Scalar‘𝑊))‘𝐿)} ⊆ 𝐹)
7251, 71fssd 6506 . . . . . . . . . . . 12 ((𝜑𝑋𝑌) → {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}:{𝑋, 𝑌}⟶𝐹)
73 eqidd 2802 . . . . . . . . . . . . . 14 ((𝜑𝑋𝑌) → 𝑋 = 𝑋)
7473orcd 870 . . . . . . . . . . . . 13 ((𝜑𝑋𝑌) → (𝑋 = 𝑋𝑋 = 𝑌))
75 elprg 4549 . . . . . . . . . . . . . 14 (𝑋𝐵 → (𝑋 ∈ {𝑋, 𝑌} ↔ (𝑋 = 𝑋𝑋 = 𝑌)))
7675biimpar 481 . . . . . . . . . . . . 13 ((𝑋𝐵 ∧ (𝑋 = 𝑋𝑋 = 𝑌)) → 𝑋 ∈ {𝑋, 𝑌})
7731, 74, 76syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑋𝑌) → 𝑋 ∈ {𝑋, 𝑌})
7872, 77ffvelrnd 6833 . . . . . . . . . . 11 ((𝜑𝑋𝑌) → ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) ∈ 𝐹)
7921adantr 484 . . . . . . . . . . 11 ((𝜑𝑋𝑌) → 𝑋 ∈ (Base‘𝑊))
806, 8, 7, 9lmodvscl 19647 . . . . . . . . . . 11 ((𝑊 ∈ LMod ∧ ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) ∈ 𝐹𝑋 ∈ (Base‘𝑊)) → (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) · 𝑋) ∈ (Base‘𝑊))
8163, 78, 79, 80syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑋𝑌) → (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) · 𝑋) ∈ (Base‘𝑊))
82 eqidd 2802 . . . . . . . . . . . . . 14 ((𝜑𝑋𝑌) → 𝑌 = 𝑌)
8382olcd 871 . . . . . . . . . . . . 13 ((𝜑𝑋𝑌) → (𝑌 = 𝑋𝑌 = 𝑌))
84 elprg 4549 . . . . . . . . . . . . . 14 (𝑌𝐵 → (𝑌 ∈ {𝑋, 𝑌} ↔ (𝑌 = 𝑋𝑌 = 𝑌)))
8584biimpar 481 . . . . . . . . . . . . 13 ((𝑌𝐵 ∧ (𝑌 = 𝑋𝑌 = 𝑌)) → 𝑌 ∈ {𝑋, 𝑌})
8647, 83, 85syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑋𝑌) → 𝑌 ∈ {𝑋, 𝑌})
8772, 86ffvelrnd 6833 . . . . . . . . . . 11 ((𝜑𝑋𝑌) → ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) ∈ 𝐹)
8819, 46sseldd 3919 . . . . . . . . . . . 12 (𝜑𝑌 ∈ (Base‘𝑊))
8988adantr 484 . . . . . . . . . . 11 ((𝜑𝑋𝑌) → 𝑌 ∈ (Base‘𝑊))
906, 8, 7, 9lmodvscl 19647 . . . . . . . . . . 11 ((𝑊 ∈ LMod ∧ ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) ∈ 𝐹𝑌 ∈ (Base‘𝑊)) → (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) · 𝑌) ∈ (Base‘𝑊))
9163, 87, 89, 90syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑋𝑌) → (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) · 𝑌) ∈ (Base‘𝑊))
92 linds2eq.3 . . . . . . . . . . 11 + = (+g𝑊)
93 fveq2 6649 . . . . . . . . . . . 12 (𝑏 = 𝑋 → ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) = ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋))
94 id 22 . . . . . . . . . . . 12 (𝑏 = 𝑋𝑏 = 𝑋)
9593, 94oveq12d 7157 . . . . . . . . . . 11 (𝑏 = 𝑋 → (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏) = (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) · 𝑋))
96 fveq2 6649 . . . . . . . . . . . 12 (𝑏 = 𝑌 → ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) = ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌))
97 id 22 . . . . . . . . . . . 12 (𝑏 = 𝑌𝑏 = 𝑌)
9896, 97oveq12d 7157 . . . . . . . . . . 11 (𝑏 = 𝑌 → (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏) = (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) · 𝑌))
996, 92, 95, 98gsumpr 19071 . . . . . . . . . 10 ((𝑊 ∈ CMnd ∧ (𝑋𝐵𝑌𝐵𝑋𝑌) ∧ ((({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) · 𝑋) ∈ (Base‘𝑊) ∧ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) · 𝑌) ∈ (Base‘𝑊))) → (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏))) = ((({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) · 𝑋) + (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) · 𝑌)))
10062, 31, 47, 49, 81, 91, 99syl132anc 1385 . . . . . . . . 9 ((𝜑𝑋𝑌) → (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏))) = ((({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) · 𝑋) + (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) · 𝑌)))
101 fvpr1g 6935 . . . . . . . . . . . 12 ((𝑋𝐵𝐾𝐹𝑋𝑌) → ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) = 𝐾)
10231, 32, 49, 101syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑋𝑌) → ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) = 𝐾)
103102oveq1d 7154 . . . . . . . . . 10 ((𝜑𝑋𝑌) → (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) · 𝑋) = (𝐾 · 𝑋))
10469adantr 484 . . . . . . . . . . . 12 ((𝜑𝑋𝑌) → ((invg‘(Scalar‘𝑊))‘𝐿) ∈ 𝐹)
105 fvpr2g 6936 . . . . . . . . . . . 12 ((𝑌𝐵 ∧ ((invg‘(Scalar‘𝑊))‘𝐿) ∈ 𝐹𝑋𝑌) → ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) = ((invg‘(Scalar‘𝑊))‘𝐿))
10647, 104, 49, 105syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑋𝑌) → ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) = ((invg‘(Scalar‘𝑊))‘𝐿))
107106oveq1d 7154 . . . . . . . . . 10 ((𝜑𝑋𝑌) → (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) · 𝑌) = (((invg‘(Scalar‘𝑊))‘𝐿) · 𝑌))
108103, 107oveq12d 7157 . . . . . . . . 9 ((𝜑𝑋𝑌) → ((({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑋) · 𝑋) + (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑌) · 𝑌)) = ((𝐾 · 𝑋) + (((invg‘(Scalar‘𝑊))‘𝐿) · 𝑌)))
1096, 8, 7, 9lmodvscl 19647 . . . . . . . . . . . . 13 ((𝑊 ∈ LMod ∧ 𝐾𝐹𝑋 ∈ (Base‘𝑊)) → (𝐾 · 𝑋) ∈ (Base‘𝑊))
11059, 13, 21, 109syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → (𝐾 · 𝑋) ∈ (Base‘𝑊))
1112, 110eqeltrrd 2894 . . . . . . . . . . . 12 (𝜑 → (𝐿 · 𝑌) ∈ (Base‘𝑊))
112 eqid 2801 . . . . . . . . . . . . 13 (invg𝑊) = (invg𝑊)
113 eqid 2801 . . . . . . . . . . . . 13 (-g𝑊) = (-g𝑊)
1146, 92, 112, 113grpsubval 18144 . . . . . . . . . . . 12 (((𝐾 · 𝑋) ∈ (Base‘𝑊) ∧ (𝐿 · 𝑌) ∈ (Base‘𝑊)) → ((𝐾 · 𝑋)(-g𝑊)(𝐿 · 𝑌)) = ((𝐾 · 𝑋) + ((invg𝑊)‘(𝐿 · 𝑌))))
115110, 111, 114syl2anc 587 . . . . . . . . . . 11 (𝜑 → ((𝐾 · 𝑋)(-g𝑊)(𝐿 · 𝑌)) = ((𝐾 · 𝑋) + ((invg𝑊)‘(𝐿 · 𝑌))))
116 lmodgrp 19637 . . . . . . . . . . . . . 14 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
11759, 116syl 17 . . . . . . . . . . . . 13 (𝜑𝑊 ∈ Grp)
1186, 10, 113grpsubeq0 18180 . . . . . . . . . . . . 13 ((𝑊 ∈ Grp ∧ (𝐾 · 𝑋) ∈ (Base‘𝑊) ∧ (𝐿 · 𝑌) ∈ (Base‘𝑊)) → (((𝐾 · 𝑋)(-g𝑊)(𝐿 · 𝑌)) = (0g𝑊) ↔ (𝐾 · 𝑋) = (𝐿 · 𝑌)))
119117, 110, 111, 118syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → (((𝐾 · 𝑋)(-g𝑊)(𝐿 · 𝑌)) = (0g𝑊) ↔ (𝐾 · 𝑋) = (𝐿 · 𝑌)))
1202, 119mpbird 260 . . . . . . . . . . 11 (𝜑 → ((𝐾 · 𝑋)(-g𝑊)(𝐿 · 𝑌)) = (0g𝑊))
1216, 8, 7, 112, 9, 67, 59, 88, 15lmodvsneg 19674 . . . . . . . . . . . 12 (𝜑 → ((invg𝑊)‘(𝐿 · 𝑌)) = (((invg‘(Scalar‘𝑊))‘𝐿) · 𝑌))
122121oveq2d 7155 . . . . . . . . . . 11 (𝜑 → ((𝐾 · 𝑋) + ((invg𝑊)‘(𝐿 · 𝑌))) = ((𝐾 · 𝑋) + (((invg‘(Scalar‘𝑊))‘𝐿) · 𝑌)))
123115, 120, 1223eqtr3rd 2845 . . . . . . . . . 10 (𝜑 → ((𝐾 · 𝑋) + (((invg‘(Scalar‘𝑊))‘𝐿) · 𝑌)) = (0g𝑊))
124123adantr 484 . . . . . . . . 9 ((𝜑𝑋𝑌) → ((𝐾 · 𝑋) + (((invg‘(Scalar‘𝑊))‘𝐿) · 𝑌)) = (0g𝑊))
125100, 108, 1243eqtrd 2840 . . . . . . . 8 ((𝜑𝑋𝑌) → (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏))) = (0g𝑊))
126 breq1 5036 . . . . . . . . . . 11 (𝑎 = {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} → (𝑎 finSupp 0 ↔ {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} finSupp 0 ))
127 fveq1 6648 . . . . . . . . . . . . . . 15 (𝑎 = {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} → (𝑎𝑏) = ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏))
128127oveq1d 7154 . . . . . . . . . . . . . 14 (𝑎 = {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} → ((𝑎𝑏) · 𝑏) = (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏))
129128mpteq2dv 5129 . . . . . . . . . . . . 13 (𝑎 = {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} → (𝑏 ∈ {𝑋, 𝑌} ↦ ((𝑎𝑏) · 𝑏)) = (𝑏 ∈ {𝑋, 𝑌} ↦ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏)))
130129oveq2d 7155 . . . . . . . . . . . 12 (𝑎 = {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} → (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ ((𝑎𝑏) · 𝑏))) = (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏))))
131130eqeq1d 2803 . . . . . . . . . . 11 (𝑎 = {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} → ((𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ ((𝑎𝑏) · 𝑏))) = (0g𝑊) ↔ (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏))) = (0g𝑊)))
132126, 131anbi12d 633 . . . . . . . . . 10 (𝑎 = {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} → ((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ ((𝑎𝑏) · 𝑏))) = (0g𝑊)) ↔ ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} finSupp 0 ∧ (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏))) = (0g𝑊))))
133 eqeq1 2805 . . . . . . . . . 10 (𝑎 = {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} → (𝑎 = ({𝑋, 𝑌} × { 0 }) ↔ {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} = ({𝑋, 𝑌} × { 0 })))
134132, 133imbi12d 348 . . . . . . . . 9 (𝑎 = {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} → (((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ ((𝑎𝑏) · 𝑏))) = (0g𝑊)) → 𝑎 = ({𝑋, 𝑌} × { 0 })) ↔ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} finSupp 0 ∧ (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏))) = (0g𝑊)) → {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} = ({𝑋, 𝑌} × { 0 }))))
13520, 46prssd 4718 . . . . . . . . . . . 12 (𝜑 → {𝑋, 𝑌} ⊆ 𝐵)
136135, 19sstrd 3928 . . . . . . . . . . 11 (𝜑 → {𝑋, 𝑌} ⊆ (Base‘𝑊))
137 lindsss 20516 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ 𝐵 ∈ (LIndS‘𝑊) ∧ {𝑋, 𝑌} ⊆ 𝐵) → {𝑋, 𝑌} ∈ (LIndS‘𝑊))
13859, 17, 135, 137syl3anc 1368 . . . . . . . . . . 11 (𝜑 → {𝑋, 𝑌} ∈ (LIndS‘𝑊))
1396, 9, 8, 7, 10, 54islinds5 30986 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ {𝑋, 𝑌} ⊆ (Base‘𝑊)) → ({𝑋, 𝑌} ∈ (LIndS‘𝑊) ↔ ∀𝑎 ∈ (𝐹m {𝑋, 𝑌})((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ ((𝑎𝑏) · 𝑏))) = (0g𝑊)) → 𝑎 = ({𝑋, 𝑌} × { 0 }))))
140139biimpa 480 . . . . . . . . . . 11 (((𝑊 ∈ LMod ∧ {𝑋, 𝑌} ⊆ (Base‘𝑊)) ∧ {𝑋, 𝑌} ∈ (LIndS‘𝑊)) → ∀𝑎 ∈ (𝐹m {𝑋, 𝑌})((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ ((𝑎𝑏) · 𝑏))) = (0g𝑊)) → 𝑎 = ({𝑋, 𝑌} × { 0 })))
14159, 136, 138, 140syl21anc 836 . . . . . . . . . 10 (𝜑 → ∀𝑎 ∈ (𝐹m {𝑋, 𝑌})((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ ((𝑎𝑏) · 𝑏))) = (0g𝑊)) → 𝑎 = ({𝑋, 𝑌} × { 0 })))
142141adantr 484 . . . . . . . . 9 ((𝜑𝑋𝑌) → ∀𝑎 ∈ (𝐹m {𝑋, 𝑌})((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ ((𝑎𝑏) · 𝑏))) = (0g𝑊)) → 𝑎 = ({𝑋, 𝑌} × { 0 })))
1439fvexi 6663 . . . . . . . . . . . 12 𝐹 ∈ V
144143a1i 11 . . . . . . . . . . 11 ((𝜑𝑋𝑌) → 𝐹 ∈ V)
145138elexd 3464 . . . . . . . . . . . 12 (𝜑 → {𝑋, 𝑌} ∈ V)
146145adantr 484 . . . . . . . . . . 11 ((𝜑𝑋𝑌) → {𝑋, 𝑌} ∈ V)
147144, 146elmapd 8407 . . . . . . . . . 10 ((𝜑𝑋𝑌) → ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} ∈ (𝐹m {𝑋, 𝑌}) ↔ {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}:{𝑋, 𝑌}⟶𝐹))
14872, 147mpbird 260 . . . . . . . . 9 ((𝜑𝑋𝑌) → {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} ∈ (𝐹m {𝑋, 𝑌}))
149134, 142, 148rspcdva 3576 . . . . . . . 8 ((𝜑𝑋𝑌) → (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} finSupp 0 ∧ (𝑊 Σg (𝑏 ∈ {𝑋, 𝑌} ↦ (({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩}‘𝑏) · 𝑏))) = (0g𝑊)) → {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} = ({𝑋, 𝑌} × { 0 })))
15057, 125, 149mp2and 698 . . . . . . 7 ((𝜑𝑋𝑌) → {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} = ({𝑋, 𝑌} × { 0 }))
151 xpprsng 6883 . . . . . . . 8 ((𝑋𝐵𝑌𝐵0 ∈ V) → ({𝑋, 𝑌} × { 0 }) = {⟨𝑋, 0 ⟩, ⟨𝑌, 0 ⟩})
15231, 47, 56, 151syl3anc 1368 . . . . . . 7 ((𝜑𝑋𝑌) → ({𝑋, 𝑌} × { 0 }) = {⟨𝑋, 0 ⟩, ⟨𝑌, 0 ⟩})
153150, 152eqtrd 2836 . . . . . 6 ((𝜑𝑋𝑌) → {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} = {⟨𝑋, 0 ⟩, ⟨𝑌, 0 ⟩})
154 opthprneg 4758 . . . . . . 7 (((⟨𝑋, 𝐾⟩ ∈ V ∧ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ ∈ V) ∧ (⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ ∧ ⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, 0 ⟩)) → ({⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} = {⟨𝑋, 0 ⟩, ⟨𝑌, 0 ⟩} ↔ (⟨𝑋, 𝐾⟩ = ⟨𝑋, 0 ⟩ ∧ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ = ⟨𝑌, 0 ⟩)))
155154biimpa 480 . . . . . 6 ((((⟨𝑋, 𝐾⟩ ∈ V ∧ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ ∈ V) ∧ (⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ ∧ ⟨𝑋, 𝐾⟩ ≠ ⟨𝑌, 0 ⟩)) ∧ {⟨𝑋, 𝐾⟩, ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩} = {⟨𝑋, 0 ⟩, ⟨𝑌, 0 ⟩}) → (⟨𝑋, 𝐾⟩ = ⟨𝑋, 0 ⟩ ∧ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ = ⟨𝑌, 0 ⟩))
15634, 36, 45, 153, 155syl1111anc 838 . . . . 5 ((𝜑𝑋𝑌) → (⟨𝑋, 𝐾⟩ = ⟨𝑋, 0 ⟩ ∧ ⟨𝑌, ((invg‘(Scalar‘𝑊))‘𝐿)⟩ = ⟨𝑌, 0 ⟩))
157156simpld 498 . . . 4 ((𝜑𝑋𝑌) → ⟨𝑋, 𝐾⟩ = ⟨𝑋, 0 ⟩)
158 opthg 5337 . . . . 5 ((𝑋𝐵𝐾𝐹) → (⟨𝑋, 𝐾⟩ = ⟨𝑋, 0 ⟩ ↔ (𝑋 = 𝑋𝐾 = 0 )))
159158simplbda 503 . . . 4 (((𝑋𝐵𝐾𝐹) ∧ ⟨𝑋, 𝐾⟩ = ⟨𝑋, 0 ⟩) → 𝐾 = 0 )
16031, 32, 157, 159syl21anc 836 . . 3 ((𝜑𝑋𝑌) → 𝐾 = 0 )
161 linds2eq.11 . . . 4 (𝜑𝐾0 )
162161adantr 484 . . 3 ((𝜑𝑋𝑌) → 𝐾0 )
163160, 162pm2.21ddne 3074 . 2 ((𝜑𝑋𝑌) → (𝑋 = 𝑌𝐾 = 𝐿))
16430, 163pm2.61dane 3077 1 (𝜑 → (𝑋 = 𝑌𝐾 = 𝐿))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844   = wceq 1538  wcel 2112  wne 2990  wral 3109  Vcvv 3444  wss 3884  {csn 4528  {cpr 4530  cop 4534   class class class wbr 5033  cmpt 5113   × cxp 5521  wf 6324  cfv 6328  (class class class)co 7139  m cmap 8393  Fincfn 8496   finSupp cfsupp 8821  Basecbs 16478  +gcplusg 16560  Scalarcsca 16563   ·𝑠 cvsca 16564  0gc0g 16708   Σg cgsu 16709  Grpcgrp 18098  invgcminusg 18099  -gcsg 18100  CMndccmn 18901  Ringcrg 19293  LModclmod 19630  LVecclvec 19870  LIndSclinds 20497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-tpos 7879  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-map 8395  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-sup 8894  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-fz 12890  df-fzo 13033  df-seq 13369  df-hash 13691  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-hom 16584  df-cco 16585  df-0g 16710  df-gsum 16711  df-prds 16716  df-pws 16718  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-mhm 17951  df-submnd 17952  df-grp 18101  df-minusg 18102  df-sbg 18103  df-mulg 18220  df-subg 18271  df-ghm 18351  df-cntz 18442  df-cmn 18903  df-abl 18904  df-mgp 19236  df-ur 19248  df-ring 19295  df-oppr 19372  df-dvdsr 19390  df-unit 19391  df-invr 19421  df-drng 19500  df-subrg 19529  df-lmod 19632  df-lss 19700  df-lsp 19740  df-lmhm 19790  df-lbs 19843  df-lvec 19871  df-sra 19940  df-rgmod 19941  df-nzr 20027  df-dsmm 20424  df-frlm 20439  df-uvc 20475  df-lindf 20498  df-linds 20499
This theorem is referenced by:  fedgmul  31115
  Copyright terms: Public domain W3C validator