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 32486
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 486 . . 3 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝑋 = π‘Œ)
2 linds2eq.12 . . . . . 6 (πœ‘ β†’ (𝐾 Β· 𝑋) = (𝐿 Β· π‘Œ))
32adantr 482 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ (𝐾 Β· 𝑋) = (𝐿 Β· π‘Œ))
41oveq2d 7422 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ (𝐿 Β· 𝑋) = (𝐿 Β· π‘Œ))
53, 4eqtr4d 2776 . . . 4 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ (𝐾 Β· 𝑋) = (𝐿 Β· 𝑋))
6 eqid 2733 . . . . 5 (Baseβ€˜π‘Š) = (Baseβ€˜π‘Š)
7 linds2eq.2 . . . . 5 Β· = ( ·𝑠 β€˜π‘Š)
8 eqid 2733 . . . . 5 (Scalarβ€˜π‘Š) = (Scalarβ€˜π‘Š)
9 linds2eq.1 . . . . 5 𝐹 = (Baseβ€˜(Scalarβ€˜π‘Š))
10 eqid 2733 . . . . 5 (0gβ€˜π‘Š) = (0gβ€˜π‘Š)
11 linds2eq.5 . . . . . 6 (πœ‘ β†’ π‘Š ∈ LVec)
1211adantr 482 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ π‘Š ∈ LVec)
13 linds2eq.9 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ 𝐹)
1413adantr 482 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝐾 ∈ 𝐹)
15 linds2eq.10 . . . . . 6 (πœ‘ β†’ 𝐿 ∈ 𝐹)
1615adantr 482 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝐿 ∈ 𝐹)
17 linds2eq.6 . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ (LIndSβ€˜π‘Š))
186linds1 21357 . . . . . . . 8 (𝐡 ∈ (LIndSβ€˜π‘Š) β†’ 𝐡 βŠ† (Baseβ€˜π‘Š))
1917, 18syl 17 . . . . . . 7 (πœ‘ β†’ 𝐡 βŠ† (Baseβ€˜π‘Š))
20 linds2eq.7 . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝐡)
2119, 20sseldd 3983 . . . . . 6 (πœ‘ β†’ 𝑋 ∈ (Baseβ€˜π‘Š))
2221adantr 482 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝑋 ∈ (Baseβ€˜π‘Š))
23100nellinds 32472 . . . . . . . 8 ((π‘Š ∈ LVec ∧ 𝐡 ∈ (LIndSβ€˜π‘Š)) β†’ Β¬ (0gβ€˜π‘Š) ∈ 𝐡)
2411, 17, 23syl2anc 585 . . . . . . 7 (πœ‘ β†’ Β¬ (0gβ€˜π‘Š) ∈ 𝐡)
25 nelne2 3041 . . . . . . 7 ((𝑋 ∈ 𝐡 ∧ Β¬ (0gβ€˜π‘Š) ∈ 𝐡) β†’ 𝑋 β‰  (0gβ€˜π‘Š))
2620, 24, 25syl2anc 585 . . . . . 6 (πœ‘ β†’ 𝑋 β‰  (0gβ€˜π‘Š))
2726adantr 482 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝑋 β‰  (0gβ€˜π‘Š))
286, 7, 8, 9, 10, 12, 14, 16, 22, 27lvecvscan2 20718 . . . 4 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ ((𝐾 Β· 𝑋) = (𝐿 Β· 𝑋) ↔ 𝐾 = 𝐿))
295, 28mpbid 231 . . 3 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝐾 = 𝐿)
301, 29jca 513 . 2 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ (𝑋 = π‘Œ ∧ 𝐾 = 𝐿))
3120adantr 482 . . . 4 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝑋 ∈ 𝐡)
3213adantr 482 . . . 4 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝐾 ∈ 𝐹)
33 opex 5464 . . . . . . 7 βŸ¨π‘‹, 𝐾⟩ ∈ V
3433a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βŸ¨π‘‹, 𝐾⟩ ∈ V)
35 opex 5464 . . . . . . 7 βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∈ V
3635a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∈ V)
37 animorrl 980 . . . . . . . 8 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)))
38 opthneg 5481 . . . . . . . . 9 ((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) β†’ (βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ↔ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ))))
3938biimpar 479 . . . . . . . 8 (((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) ∧ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ))) β†’ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩)
4031, 32, 37, 39syl21anc 837 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩)
41 animorrl 980 . . . . . . . 8 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  0 ))
42 opthneg 5481 . . . . . . . . 9 ((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) β†’ (βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩ ↔ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  0 )))
4342biimpar 479 . . . . . . . 8 (((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) ∧ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  0 )) β†’ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩)
4431, 32, 41, 43syl21anc 837 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩)
4540, 44jca 513 . . . . . 6 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∧ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩))
46 linds2eq.8 . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ ∈ 𝐡)
4746adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Œ ∈ 𝐡)
48 fvexd 6904 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ V)
49 simpr 486 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝑋 β‰  π‘Œ)
50 fprg 7150 . . . . . . . . . 10 (((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) ∧ (𝐾 ∈ 𝐹 ∧ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ V) ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}:{𝑋, π‘Œ}⟢{𝐾, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)})
5131, 47, 32, 48, 49, 50syl221anc 1382 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}:{𝑋, π‘Œ}⟢{𝐾, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)})
52 prfi 9319 . . . . . . . . . 10 {𝑋, π‘Œ} ∈ Fin
5352a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {𝑋, π‘Œ} ∈ Fin)
54 linds2eq.4 . . . . . . . . . . 11 0 = (0gβ€˜(Scalarβ€˜π‘Š))
5554fvexi 6903 . . . . . . . . . 10 0 ∈ V
5655a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 0 ∈ V)
5751, 53, 56fdmfifsupp 9370 . . . . . . . 8 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} finSupp 0 )
58 lveclmod 20710 . . . . . . . . . . . . 13 (π‘Š ∈ LVec β†’ π‘Š ∈ LMod)
5911, 58syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Š ∈ LMod)
60 lmodcmn 20513 . . . . . . . . . . . 12 (π‘Š ∈ LMod β†’ π‘Š ∈ CMnd)
6159, 60syl 17 . . . . . . . . . . 11 (πœ‘ β†’ π‘Š ∈ CMnd)
6261adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Š ∈ CMnd)
6359adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Š ∈ LMod)
648lmodring 20472 . . . . . . . . . . . . . . . . 17 (π‘Š ∈ LMod β†’ (Scalarβ€˜π‘Š) ∈ Ring)
65 ringgrp 20055 . . . . . . . . . . . . . . . . 17 ((Scalarβ€˜π‘Š) ∈ Ring β†’ (Scalarβ€˜π‘Š) ∈ Grp)
6659, 64, 653syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (Scalarβ€˜π‘Š) ∈ Grp)
67 eqid 2733 . . . . . . . . . . . . . . . . 17 (invgβ€˜(Scalarβ€˜π‘Š)) = (invgβ€˜(Scalarβ€˜π‘Š))
689, 67grpinvcl 18869 . . . . . . . . . . . . . . . 16 (((Scalarβ€˜π‘Š) ∈ Grp ∧ 𝐿 ∈ 𝐹) β†’ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ 𝐹)
6966, 15, 68syl2anc 585 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ 𝐹)
7013, 69prssd 4825 . . . . . . . . . . . . . 14 (πœ‘ β†’ {𝐾, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)} βŠ† 𝐹)
7170adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {𝐾, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)} βŠ† 𝐹)
7251, 71fssd 6733 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}:{𝑋, π‘Œ}⟢𝐹)
73 eqidd 2734 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝑋 = 𝑋)
7473orcd 872 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (𝑋 = 𝑋 ∨ 𝑋 = π‘Œ))
75 elprg 4649 . . . . . . . . . . . . . 14 (𝑋 ∈ 𝐡 β†’ (𝑋 ∈ {𝑋, π‘Œ} ↔ (𝑋 = 𝑋 ∨ 𝑋 = π‘Œ)))
7675biimpar 479 . . . . . . . . . . . . 13 ((𝑋 ∈ 𝐡 ∧ (𝑋 = 𝑋 ∨ 𝑋 = π‘Œ)) β†’ 𝑋 ∈ {𝑋, π‘Œ})
7731, 74, 76syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝑋 ∈ {𝑋, π‘Œ})
7872, 77ffvelcdmd 7085 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) ∈ 𝐹)
7921adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝑋 ∈ (Baseβ€˜π‘Š))
806, 8, 7, 9lmodvscl 20482 . . . . . . . . . . 11 ((π‘Š ∈ LMod ∧ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) ∈ 𝐹 ∧ 𝑋 ∈ (Baseβ€˜π‘Š)) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) ∈ (Baseβ€˜π‘Š))
8163, 78, 79, 80syl3anc 1372 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) ∈ (Baseβ€˜π‘Š))
82 eqidd 2734 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Œ = π‘Œ)
8382olcd 873 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (π‘Œ = 𝑋 ∨ π‘Œ = π‘Œ))
84 elprg 4649 . . . . . . . . . . . . . 14 (π‘Œ ∈ 𝐡 β†’ (π‘Œ ∈ {𝑋, π‘Œ} ↔ (π‘Œ = 𝑋 ∨ π‘Œ = π‘Œ)))
8584biimpar 479 . . . . . . . . . . . . 13 ((π‘Œ ∈ 𝐡 ∧ (π‘Œ = 𝑋 ∨ π‘Œ = π‘Œ)) β†’ π‘Œ ∈ {𝑋, π‘Œ})
8647, 83, 85syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Œ ∈ {𝑋, π‘Œ})
8772, 86ffvelcdmd 7085 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) ∈ 𝐹)
8819, 46sseldd 3983 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ (Baseβ€˜π‘Š))
8988adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Œ ∈ (Baseβ€˜π‘Š))
906, 8, 7, 9lmodvscl 20482 . . . . . . . . . . 11 ((π‘Š ∈ LMod ∧ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) ∈ 𝐹 ∧ π‘Œ ∈ (Baseβ€˜π‘Š)) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ) ∈ (Baseβ€˜π‘Š))
9163, 87, 89, 90syl3anc 1372 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ) ∈ (Baseβ€˜π‘Š))
92 linds2eq.3 . . . . . . . . . . 11 + = (+gβ€˜π‘Š)
93 fveq2 6889 . . . . . . . . . . . 12 (𝑏 = 𝑋 β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) = ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹))
94 id 22 . . . . . . . . . . . 12 (𝑏 = 𝑋 β†’ 𝑏 = 𝑋)
9593, 94oveq12d 7424 . . . . . . . . . . 11 (𝑏 = 𝑋 β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏) = (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋))
96 fveq2 6889 . . . . . . . . . . . 12 (𝑏 = π‘Œ β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) = ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ))
97 id 22 . . . . . . . . . . . 12 (𝑏 = π‘Œ β†’ 𝑏 = π‘Œ)
9896, 97oveq12d 7424 . . . . . . . . . . 11 (𝑏 = π‘Œ β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏) = (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ))
996, 92, 95, 98gsumpr 19818 . . . . . . . . . 10 ((π‘Š ∈ CMnd ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑋 β‰  π‘Œ) ∧ ((({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) ∈ (Baseβ€˜π‘Š) ∧ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ) ∈ (Baseβ€˜π‘Š))) β†’ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = ((({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) + (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ)))
10062, 31, 47, 49, 81, 91, 99syl132anc 1389 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = ((({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) + (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ)))
101 fvpr1g 7185 . . . . . . . . . . . 12 ((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹 ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) = 𝐾)
10231, 32, 49, 101syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) = 𝐾)
103102oveq1d 7421 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) = (𝐾 Β· 𝑋))
10469adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ 𝐹)
105 fvpr2g 7186 . . . . . . . . . . . 12 ((π‘Œ ∈ 𝐡 ∧ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ 𝐹 ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) = ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ))
10647, 104, 49, 105syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) = ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ))
107106oveq1d 7421 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ) = (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ))
108103, 107oveq12d 7424 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ((({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) + (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ)) = ((𝐾 Β· 𝑋) + (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ)))
1096, 8, 7, 9lmodvscl 20482 . . . . . . . . . . . . 13 ((π‘Š ∈ LMod ∧ 𝐾 ∈ 𝐹 ∧ 𝑋 ∈ (Baseβ€˜π‘Š)) β†’ (𝐾 Β· 𝑋) ∈ (Baseβ€˜π‘Š))
11059, 13, 21, 109syl3anc 1372 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐾 Β· 𝑋) ∈ (Baseβ€˜π‘Š))
1112, 110eqeltrrd 2835 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐿 Β· π‘Œ) ∈ (Baseβ€˜π‘Š))
112 eqid 2733 . . . . . . . . . . . . 13 (invgβ€˜π‘Š) = (invgβ€˜π‘Š)
113 eqid 2733 . . . . . . . . . . . . 13 (-gβ€˜π‘Š) = (-gβ€˜π‘Š)
1146, 92, 112, 113grpsubval 18867 . . . . . . . . . . . 12 (((𝐾 Β· 𝑋) ∈ (Baseβ€˜π‘Š) ∧ (𝐿 Β· π‘Œ) ∈ (Baseβ€˜π‘Š)) β†’ ((𝐾 Β· 𝑋)(-gβ€˜π‘Š)(𝐿 Β· π‘Œ)) = ((𝐾 Β· 𝑋) + ((invgβ€˜π‘Š)β€˜(𝐿 Β· π‘Œ))))
115110, 111, 114syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐾 Β· 𝑋)(-gβ€˜π‘Š)(𝐿 Β· π‘Œ)) = ((𝐾 Β· 𝑋) + ((invgβ€˜π‘Š)β€˜(𝐿 Β· π‘Œ))))
116 lmodgrp 20471 . . . . . . . . . . . . . 14 (π‘Š ∈ LMod β†’ π‘Š ∈ Grp)
11759, 116syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Š ∈ Grp)
1186, 10, 113grpsubeq0 18906 . . . . . . . . . . . . 13 ((π‘Š ∈ Grp ∧ (𝐾 Β· 𝑋) ∈ (Baseβ€˜π‘Š) ∧ (𝐿 Β· π‘Œ) ∈ (Baseβ€˜π‘Š)) β†’ (((𝐾 Β· 𝑋)(-gβ€˜π‘Š)(𝐿 Β· π‘Œ)) = (0gβ€˜π‘Š) ↔ (𝐾 Β· 𝑋) = (𝐿 Β· π‘Œ)))
119117, 110, 111, 118syl3anc 1372 . . . . . . . . . . . 12 (πœ‘ β†’ (((𝐾 Β· 𝑋)(-gβ€˜π‘Š)(𝐿 Β· π‘Œ)) = (0gβ€˜π‘Š) ↔ (𝐾 Β· 𝑋) = (𝐿 Β· π‘Œ)))
1202, 119mpbird 257 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐾 Β· 𝑋)(-gβ€˜π‘Š)(𝐿 Β· π‘Œ)) = (0gβ€˜π‘Š))
1216, 8, 7, 112, 9, 67, 59, 88, 15lmodvsneg 20509 . . . . . . . . . . . 12 (πœ‘ β†’ ((invgβ€˜π‘Š)β€˜(𝐿 Β· π‘Œ)) = (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ))
122121oveq2d 7422 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐾 Β· 𝑋) + ((invgβ€˜π‘Š)β€˜(𝐿 Β· π‘Œ))) = ((𝐾 Β· 𝑋) + (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ)))
123115, 120, 1223eqtr3rd 2782 . . . . . . . . . 10 (πœ‘ β†’ ((𝐾 Β· 𝑋) + (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ)) = (0gβ€˜π‘Š))
124123adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ((𝐾 Β· 𝑋) + (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ)) = (0gβ€˜π‘Š))
125100, 108, 1243eqtrd 2777 . . . . . . . 8 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š))
126 breq1 5151 . . . . . . . . . . 11 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (π‘Ž finSupp 0 ↔ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} finSupp 0 ))
127 fveq1 6888 . . . . . . . . . . . . . . 15 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (π‘Žβ€˜π‘) = ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘))
128127oveq1d 7421 . . . . . . . . . . . . . 14 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ ((π‘Žβ€˜π‘) Β· 𝑏) = (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))
129128mpteq2dv 5250 . . . . . . . . . . . . 13 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏)) = (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏)))
130129oveq2d 7422 . . . . . . . . . . . 12 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))))
131130eqeq1d 2735 . . . . . . . . . . 11 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ ((π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š) ↔ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)))
132126, 131anbi12d 632 . . . . . . . . . 10 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ ((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) ↔ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š))))
133 eqeq1 2737 . . . . . . . . . 10 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (π‘Ž = ({𝑋, π‘Œ} Γ— { 0 }) ↔ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = ({𝑋, π‘Œ} Γ— { 0 })))
134132, 133imbi12d 345 . . . . . . . . 9 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ π‘Ž = ({𝑋, π‘Œ} Γ— { 0 })) ↔ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = ({𝑋, π‘Œ} Γ— { 0 }))))
13520, 46prssd 4825 . . . . . . . . . . . 12 (πœ‘ β†’ {𝑋, π‘Œ} βŠ† 𝐡)
136135, 19sstrd 3992 . . . . . . . . . . 11 (πœ‘ β†’ {𝑋, π‘Œ} βŠ† (Baseβ€˜π‘Š))
137 lindsss 21371 . . . . . . . . . . . 12 ((π‘Š ∈ LMod ∧ 𝐡 ∈ (LIndSβ€˜π‘Š) ∧ {𝑋, π‘Œ} βŠ† 𝐡) β†’ {𝑋, π‘Œ} ∈ (LIndSβ€˜π‘Š))
13859, 17, 135, 137syl3anc 1372 . . . . . . . . . . 11 (πœ‘ β†’ {𝑋, π‘Œ} ∈ (LIndSβ€˜π‘Š))
1396, 9, 8, 7, 10, 54islinds5 32469 . . . . . . . . . . . 12 ((π‘Š ∈ LMod ∧ {𝑋, π‘Œ} βŠ† (Baseβ€˜π‘Š)) β†’ ({𝑋, π‘Œ} ∈ (LIndSβ€˜π‘Š) ↔ βˆ€π‘Ž ∈ (𝐹 ↑m {𝑋, π‘Œ})((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ π‘Ž = ({𝑋, π‘Œ} Γ— { 0 }))))
140139biimpa 478 . . . . . . . . . . 11 (((π‘Š ∈ LMod ∧ {𝑋, π‘Œ} βŠ† (Baseβ€˜π‘Š)) ∧ {𝑋, π‘Œ} ∈ (LIndSβ€˜π‘Š)) β†’ βˆ€π‘Ž ∈ (𝐹 ↑m {𝑋, π‘Œ})((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ π‘Ž = ({𝑋, π‘Œ} Γ— { 0 })))
14159, 136, 138, 140syl21anc 837 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘Ž ∈ (𝐹 ↑m {𝑋, π‘Œ})((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ π‘Ž = ({𝑋, π‘Œ} Γ— { 0 })))
142141adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βˆ€π‘Ž ∈ (𝐹 ↑m {𝑋, π‘Œ})((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ π‘Ž = ({𝑋, π‘Œ} Γ— { 0 })))
1439fvexi 6903 . . . . . . . . . . . 12 𝐹 ∈ V
144143a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝐹 ∈ V)
145138elexd 3495 . . . . . . . . . . . 12 (πœ‘ β†’ {𝑋, π‘Œ} ∈ V)
146145adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {𝑋, π‘Œ} ∈ V)
147144, 146elmapd 8831 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} ∈ (𝐹 ↑m {𝑋, π‘Œ}) ↔ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}:{𝑋, π‘Œ}⟢𝐹))
14872, 147mpbird 257 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} ∈ (𝐹 ↑m {𝑋, π‘Œ}))
149134, 142, 148rspcdva 3614 . . . . . . . 8 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = ({𝑋, π‘Œ} Γ— { 0 })))
15057, 125, 149mp2and 698 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = ({𝑋, π‘Œ} Γ— { 0 }))
151 xpprsng 7135 . . . . . . . 8 ((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 0 ∈ V) β†’ ({𝑋, π‘Œ} Γ— { 0 }) = {βŸ¨π‘‹, 0 ⟩, βŸ¨π‘Œ, 0 ⟩})
15231, 47, 56, 151syl3anc 1372 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({𝑋, π‘Œ} Γ— { 0 }) = {βŸ¨π‘‹, 0 ⟩, βŸ¨π‘Œ, 0 ⟩})
153150, 152eqtrd 2773 . . . . . 6 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = {βŸ¨π‘‹, 0 ⟩, βŸ¨π‘Œ, 0 ⟩})
154 opthprneg 4865 . . . . . . 7 (((βŸ¨π‘‹, 𝐾⟩ ∈ V ∧ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∈ V) ∧ (βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∧ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩)) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = {βŸ¨π‘‹, 0 ⟩, βŸ¨π‘Œ, 0 ⟩} ↔ (βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩ ∧ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ = βŸ¨π‘Œ, 0 ⟩)))
155154biimpa 478 . . . . . 6 ((((βŸ¨π‘‹, 𝐾⟩ ∈ V ∧ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∈ V) ∧ (βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∧ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩)) ∧ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = {βŸ¨π‘‹, 0 ⟩, βŸ¨π‘Œ, 0 ⟩}) β†’ (βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩ ∧ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ = βŸ¨π‘Œ, 0 ⟩))
15634, 36, 45, 153, 155syl1111anc 839 . . . . 5 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩ ∧ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ = βŸ¨π‘Œ, 0 ⟩))
157156simpld 496 . . . 4 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩)
158 opthg 5477 . . . . 5 ((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) β†’ (βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩ ↔ (𝑋 = 𝑋 ∧ 𝐾 = 0 )))
159158simplbda 501 . . . 4 (((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) ∧ βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩) β†’ 𝐾 = 0 )
16031, 32, 157, 159syl21anc 837 . . 3 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝐾 = 0 )
161 linds2eq.11 . . . 4 (πœ‘ β†’ 𝐾 β‰  0 )
162161adantr 482 . . 3 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝐾 β‰  0 )
163160, 162pm2.21ddne 3027 . 2 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (𝑋 = π‘Œ ∧ 𝐾 = 𝐿))
16430, 163pm2.61dane 3030 1 (πœ‘ β†’ (𝑋 = π‘Œ ∧ 𝐾 = 𝐿))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  Vcvv 3475   βŠ† wss 3948  {csn 4628  {cpr 4630  βŸ¨cop 4634   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406   ↑m cmap 8817  Fincfn 8936   finSupp cfsupp 9358  Basecbs 17141  +gcplusg 17194  Scalarcsca 17197   ·𝑠 cvsca 17198  0gc0g 17382   Ξ£g cgsu 17383  Grpcgrp 18816  invgcminusg 18817  -gcsg 18818  CMndccmn 19643  Ringcrg 20050  LModclmod 20464  LVecclvec 20706  LIndSclinds 21352
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-tpos 8208  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-map 8819  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-sup 9434  df-oi 9502  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-fz 13482  df-fzo 13625  df-seq 13964  df-hash 14288  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-sca 17210  df-vsca 17211  df-ip 17212  df-tset 17213  df-ple 17214  df-ds 17216  df-hom 17218  df-cco 17219  df-0g 17384  df-gsum 17385  df-prds 17390  df-pws 17392  df-mre 17527  df-mrc 17528  df-acs 17530  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-mhm 18668  df-submnd 18669  df-grp 18819  df-minusg 18820  df-sbg 18821  df-mulg 18946  df-subg 18998  df-ghm 19085  df-cntz 19176  df-cmn 19645  df-abl 19646  df-mgp 19983  df-ur 20000  df-ring 20052  df-oppr 20143  df-dvdsr 20164  df-unit 20165  df-invr 20195  df-nzr 20285  df-drng 20310  df-subrg 20354  df-lmod 20466  df-lss 20536  df-lsp 20576  df-lmhm 20626  df-lbs 20679  df-lvec 20707  df-sra 20778  df-rgmod 20779  df-dsmm 21279  df-frlm 21294  df-uvc 21330  df-lindf 21353  df-linds 21354
This theorem is referenced by:  fedgmul  32705
  Copyright terms: Public domain W3C validator