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 32928
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 484 . . 3 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝑋 = π‘Œ)
2 linds2eq.12 . . . . . 6 (πœ‘ β†’ (𝐾 Β· 𝑋) = (𝐿 Β· π‘Œ))
32adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ (𝐾 Β· 𝑋) = (𝐿 Β· π‘Œ))
41oveq2d 7417 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ (𝐿 Β· 𝑋) = (𝐿 Β· π‘Œ))
53, 4eqtr4d 2767 . . . 4 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ (𝐾 Β· 𝑋) = (𝐿 Β· 𝑋))
6 eqid 2724 . . . . 5 (Baseβ€˜π‘Š) = (Baseβ€˜π‘Š)
7 linds2eq.2 . . . . 5 Β· = ( ·𝑠 β€˜π‘Š)
8 eqid 2724 . . . . 5 (Scalarβ€˜π‘Š) = (Scalarβ€˜π‘Š)
9 linds2eq.1 . . . . 5 𝐹 = (Baseβ€˜(Scalarβ€˜π‘Š))
10 eqid 2724 . . . . 5 (0gβ€˜π‘Š) = (0gβ€˜π‘Š)
11 linds2eq.5 . . . . . 6 (πœ‘ β†’ π‘Š ∈ LVec)
1211adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ π‘Š ∈ LVec)
13 linds2eq.9 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ 𝐹)
1413adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝐾 ∈ 𝐹)
15 linds2eq.10 . . . . . 6 (πœ‘ β†’ 𝐿 ∈ 𝐹)
1615adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝐿 ∈ 𝐹)
17 linds2eq.6 . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ (LIndSβ€˜π‘Š))
186linds1 21665 . . . . . . . 8 (𝐡 ∈ (LIndSβ€˜π‘Š) β†’ 𝐡 βŠ† (Baseβ€˜π‘Š))
1917, 18syl 17 . . . . . . 7 (πœ‘ β†’ 𝐡 βŠ† (Baseβ€˜π‘Š))
20 linds2eq.7 . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝐡)
2119, 20sseldd 3975 . . . . . 6 (πœ‘ β†’ 𝑋 ∈ (Baseβ€˜π‘Š))
2221adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝑋 ∈ (Baseβ€˜π‘Š))
23100nellinds 32914 . . . . . . . 8 ((π‘Š ∈ LVec ∧ 𝐡 ∈ (LIndSβ€˜π‘Š)) β†’ Β¬ (0gβ€˜π‘Š) ∈ 𝐡)
2411, 17, 23syl2anc 583 . . . . . . 7 (πœ‘ β†’ Β¬ (0gβ€˜π‘Š) ∈ 𝐡)
25 nelne2 3032 . . . . . . 7 ((𝑋 ∈ 𝐡 ∧ Β¬ (0gβ€˜π‘Š) ∈ 𝐡) β†’ 𝑋 β‰  (0gβ€˜π‘Š))
2620, 24, 25syl2anc 583 . . . . . 6 (πœ‘ β†’ 𝑋 β‰  (0gβ€˜π‘Š))
2726adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝑋 β‰  (0gβ€˜π‘Š))
286, 7, 8, 9, 10, 12, 14, 16, 22, 27lvecvscan2 20948 . . . 4 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ ((𝐾 Β· 𝑋) = (𝐿 Β· 𝑋) ↔ 𝐾 = 𝐿))
295, 28mpbid 231 . . 3 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ 𝐾 = 𝐿)
301, 29jca 511 . 2 ((πœ‘ ∧ 𝑋 = π‘Œ) β†’ (𝑋 = π‘Œ ∧ 𝐾 = 𝐿))
3120adantr 480 . . . 4 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝑋 ∈ 𝐡)
3213adantr 480 . . . 4 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝐾 ∈ 𝐹)
33 opex 5454 . . . . . . 7 βŸ¨π‘‹, 𝐾⟩ ∈ V
3433a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βŸ¨π‘‹, 𝐾⟩ ∈ V)
35 opex 5454 . . . . . . 7 βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∈ V
3635a1i 11 . . . . . 6 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∈ V)
37 animorrl 977 . . . . . . . 8 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)))
38 opthneg 5471 . . . . . . . . 9 ((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) β†’ (βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ↔ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ))))
3938biimpar 477 . . . . . . . 8 (((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) ∧ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ))) β†’ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩)
4031, 32, 37, 39syl21anc 835 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩)
41 animorrl 977 . . . . . . . 8 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  0 ))
42 opthneg 5471 . . . . . . . . 9 ((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) β†’ (βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩ ↔ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  0 )))
4342biimpar 477 . . . . . . . 8 (((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) ∧ (𝑋 β‰  π‘Œ ∨ 𝐾 β‰  0 )) β†’ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩)
4431, 32, 41, 43syl21anc 835 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩)
4540, 44jca 511 . . . . . 6 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∧ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩))
46 linds2eq.8 . . . . . . . . . . 11 (πœ‘ β†’ π‘Œ ∈ 𝐡)
4746adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Œ ∈ 𝐡)
48 fvexd 6896 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ V)
49 simpr 484 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝑋 β‰  π‘Œ)
50 fprg 7145 . . . . . . . . . 10 (((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) ∧ (𝐾 ∈ 𝐹 ∧ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ V) ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}:{𝑋, π‘Œ}⟢{𝐾, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)})
5131, 47, 32, 48, 49, 50syl221anc 1378 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}:{𝑋, π‘Œ}⟢{𝐾, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)})
52 prfi 9317 . . . . . . . . . 10 {𝑋, π‘Œ} ∈ Fin
5352a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {𝑋, π‘Œ} ∈ Fin)
54 linds2eq.4 . . . . . . . . . . 11 0 = (0gβ€˜(Scalarβ€˜π‘Š))
5554fvexi 6895 . . . . . . . . . 10 0 ∈ V
5655a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 0 ∈ V)
5751, 53, 56fdmfifsupp 9368 . . . . . . . 8 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} finSupp 0 )
58 lveclmod 20939 . . . . . . . . . . . . 13 (π‘Š ∈ LVec β†’ π‘Š ∈ LMod)
5911, 58syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Š ∈ LMod)
60 lmodcmn 20741 . . . . . . . . . . . 12 (π‘Š ∈ LMod β†’ π‘Š ∈ CMnd)
6159, 60syl 17 . . . . . . . . . . 11 (πœ‘ β†’ π‘Š ∈ CMnd)
6261adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Š ∈ CMnd)
6359adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Š ∈ LMod)
648lmodring 20699 . . . . . . . . . . . . . . . . 17 (π‘Š ∈ LMod β†’ (Scalarβ€˜π‘Š) ∈ Ring)
65 ringgrp 20128 . . . . . . . . . . . . . . . . 17 ((Scalarβ€˜π‘Š) ∈ Ring β†’ (Scalarβ€˜π‘Š) ∈ Grp)
6659, 64, 653syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (Scalarβ€˜π‘Š) ∈ Grp)
67 eqid 2724 . . . . . . . . . . . . . . . . 17 (invgβ€˜(Scalarβ€˜π‘Š)) = (invgβ€˜(Scalarβ€˜π‘Š))
689, 67grpinvcl 18904 . . . . . . . . . . . . . . . 16 (((Scalarβ€˜π‘Š) ∈ Grp ∧ 𝐿 ∈ 𝐹) β†’ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ 𝐹)
6966, 15, 68syl2anc 583 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ 𝐹)
7013, 69prssd 4817 . . . . . . . . . . . . . 14 (πœ‘ β†’ {𝐾, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)} βŠ† 𝐹)
7170adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {𝐾, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)} βŠ† 𝐹)
7251, 71fssd 6725 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}:{𝑋, π‘Œ}⟢𝐹)
73 eqidd 2725 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝑋 = 𝑋)
7473orcd 870 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (𝑋 = 𝑋 ∨ 𝑋 = π‘Œ))
75 elprg 4641 . . . . . . . . . . . . . 14 (𝑋 ∈ 𝐡 β†’ (𝑋 ∈ {𝑋, π‘Œ} ↔ (𝑋 = 𝑋 ∨ 𝑋 = π‘Œ)))
7675biimpar 477 . . . . . . . . . . . . 13 ((𝑋 ∈ 𝐡 ∧ (𝑋 = 𝑋 ∨ 𝑋 = π‘Œ)) β†’ 𝑋 ∈ {𝑋, π‘Œ})
7731, 74, 76syl2anc 583 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝑋 ∈ {𝑋, π‘Œ})
7872, 77ffvelcdmd 7077 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) ∈ 𝐹)
7921adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝑋 ∈ (Baseβ€˜π‘Š))
806, 8, 7, 9lmodvscl 20709 . . . . . . . . . . 11 ((π‘Š ∈ LMod ∧ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) ∈ 𝐹 ∧ 𝑋 ∈ (Baseβ€˜π‘Š)) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) ∈ (Baseβ€˜π‘Š))
8163, 78, 79, 80syl3anc 1368 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) ∈ (Baseβ€˜π‘Š))
82 eqidd 2725 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Œ = π‘Œ)
8382olcd 871 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (π‘Œ = 𝑋 ∨ π‘Œ = π‘Œ))
84 elprg 4641 . . . . . . . . . . . . . 14 (π‘Œ ∈ 𝐡 β†’ (π‘Œ ∈ {𝑋, π‘Œ} ↔ (π‘Œ = 𝑋 ∨ π‘Œ = π‘Œ)))
8584biimpar 477 . . . . . . . . . . . . 13 ((π‘Œ ∈ 𝐡 ∧ (π‘Œ = 𝑋 ∨ π‘Œ = π‘Œ)) β†’ π‘Œ ∈ {𝑋, π‘Œ})
8647, 83, 85syl2anc 583 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Œ ∈ {𝑋, π‘Œ})
8772, 86ffvelcdmd 7077 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) ∈ 𝐹)
8819, 46sseldd 3975 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ (Baseβ€˜π‘Š))
8988adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ π‘Œ ∈ (Baseβ€˜π‘Š))
906, 8, 7, 9lmodvscl 20709 . . . . . . . . . . 11 ((π‘Š ∈ LMod ∧ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) ∈ 𝐹 ∧ π‘Œ ∈ (Baseβ€˜π‘Š)) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ) ∈ (Baseβ€˜π‘Š))
9163, 87, 89, 90syl3anc 1368 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ) ∈ (Baseβ€˜π‘Š))
92 linds2eq.3 . . . . . . . . . . 11 + = (+gβ€˜π‘Š)
93 fveq2 6881 . . . . . . . . . . . 12 (𝑏 = 𝑋 β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) = ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹))
94 id 22 . . . . . . . . . . . 12 (𝑏 = 𝑋 β†’ 𝑏 = 𝑋)
9593, 94oveq12d 7419 . . . . . . . . . . 11 (𝑏 = 𝑋 β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏) = (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋))
96 fveq2 6881 . . . . . . . . . . . 12 (𝑏 = π‘Œ β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) = ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ))
97 id 22 . . . . . . . . . . . 12 (𝑏 = π‘Œ β†’ 𝑏 = π‘Œ)
9896, 97oveq12d 7419 . . . . . . . . . . 11 (𝑏 = π‘Œ β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏) = (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ))
996, 92, 95, 98gsumpr 19860 . . . . . . . . . 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 7180 . . . . . . . . . . . 12 ((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹 ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) = 𝐾)
10231, 32, 49, 101syl3anc 1368 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) = 𝐾)
103102oveq1d 7416 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) = (𝐾 Β· 𝑋))
10469adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ 𝐹)
105 fvpr2g 7181 . . . . . . . . . . . 12 ((π‘Œ ∈ 𝐡 ∧ ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) ∈ 𝐹 ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) = ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ))
10647, 104, 49, 105syl3anc 1368 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) = ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ))
107106oveq1d 7416 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ) = (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ))
108103, 107oveq12d 7419 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ((({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘‹) Β· 𝑋) + (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘Œ) Β· π‘Œ)) = ((𝐾 Β· 𝑋) + (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ)))
1096, 8, 7, 9lmodvscl 20709 . . . . . . . . . . . . 13 ((π‘Š ∈ LMod ∧ 𝐾 ∈ 𝐹 ∧ 𝑋 ∈ (Baseβ€˜π‘Š)) β†’ (𝐾 Β· 𝑋) ∈ (Baseβ€˜π‘Š))
11059, 13, 21, 109syl3anc 1368 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐾 Β· 𝑋) ∈ (Baseβ€˜π‘Š))
1112, 110eqeltrrd 2826 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐿 Β· π‘Œ) ∈ (Baseβ€˜π‘Š))
112 eqid 2724 . . . . . . . . . . . . 13 (invgβ€˜π‘Š) = (invgβ€˜π‘Š)
113 eqid 2724 . . . . . . . . . . . . 13 (-gβ€˜π‘Š) = (-gβ€˜π‘Š)
1146, 92, 112, 113grpsubval 18902 . . . . . . . . . . . 12 (((𝐾 Β· 𝑋) ∈ (Baseβ€˜π‘Š) ∧ (𝐿 Β· π‘Œ) ∈ (Baseβ€˜π‘Š)) β†’ ((𝐾 Β· 𝑋)(-gβ€˜π‘Š)(𝐿 Β· π‘Œ)) = ((𝐾 Β· 𝑋) + ((invgβ€˜π‘Š)β€˜(𝐿 Β· π‘Œ))))
115110, 111, 114syl2anc 583 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐾 Β· 𝑋)(-gβ€˜π‘Š)(𝐿 Β· π‘Œ)) = ((𝐾 Β· 𝑋) + ((invgβ€˜π‘Š)β€˜(𝐿 Β· π‘Œ))))
116 lmodgrp 20698 . . . . . . . . . . . . . 14 (π‘Š ∈ LMod β†’ π‘Š ∈ Grp)
11759, 116syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Š ∈ Grp)
1186, 10, 113grpsubeq0 18941 . . . . . . . . . . . . 13 ((π‘Š ∈ Grp ∧ (𝐾 Β· 𝑋) ∈ (Baseβ€˜π‘Š) ∧ (𝐿 Β· π‘Œ) ∈ (Baseβ€˜π‘Š)) β†’ (((𝐾 Β· 𝑋)(-gβ€˜π‘Š)(𝐿 Β· π‘Œ)) = (0gβ€˜π‘Š) ↔ (𝐾 Β· 𝑋) = (𝐿 Β· π‘Œ)))
119117, 110, 111, 118syl3anc 1368 . . . . . . . . . . . 12 (πœ‘ β†’ (((𝐾 Β· 𝑋)(-gβ€˜π‘Š)(𝐿 Β· π‘Œ)) = (0gβ€˜π‘Š) ↔ (𝐾 Β· 𝑋) = (𝐿 Β· π‘Œ)))
1202, 119mpbird 257 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐾 Β· 𝑋)(-gβ€˜π‘Š)(𝐿 Β· π‘Œ)) = (0gβ€˜π‘Š))
1216, 8, 7, 112, 9, 67, 59, 88, 15lmodvsneg 20737 . . . . . . . . . . . 12 (πœ‘ β†’ ((invgβ€˜π‘Š)β€˜(𝐿 Β· π‘Œ)) = (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ))
122121oveq2d 7417 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐾 Β· 𝑋) + ((invgβ€˜π‘Š)β€˜(𝐿 Β· π‘Œ))) = ((𝐾 Β· 𝑋) + (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ)))
123115, 120, 1223eqtr3rd 2773 . . . . . . . . . 10 (πœ‘ β†’ ((𝐾 Β· 𝑋) + (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ)) = (0gβ€˜π‘Š))
124123adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ((𝐾 Β· 𝑋) + (((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ) Β· π‘Œ)) = (0gβ€˜π‘Š))
125100, 108, 1243eqtrd 2768 . . . . . . . 8 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š))
126 breq1 5141 . . . . . . . . . . 11 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (π‘Ž finSupp 0 ↔ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} finSupp 0 ))
127 fveq1 6880 . . . . . . . . . . . . . . 15 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (π‘Žβ€˜π‘) = ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘))
128127oveq1d 7416 . . . . . . . . . . . . . 14 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ ((π‘Žβ€˜π‘) Β· 𝑏) = (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))
129128mpteq2dv 5240 . . . . . . . . . . . . 13 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏)) = (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏)))
130129oveq2d 7417 . . . . . . . . . . . 12 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))))
131130eqeq1d 2726 . . . . . . . . . . 11 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ ((π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š) ↔ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)))
132126, 131anbi12d 630 . . . . . . . . . 10 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ ((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) ↔ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š))))
133 eqeq1 2728 . . . . . . . . . 10 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (π‘Ž = ({𝑋, π‘Œ} Γ— { 0 }) ↔ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = ({𝑋, π‘Œ} Γ— { 0 })))
134132, 133imbi12d 344 . . . . . . . . 9 (π‘Ž = {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} β†’ (((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ π‘Ž = ({𝑋, π‘Œ} Γ— { 0 })) ↔ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = ({𝑋, π‘Œ} Γ— { 0 }))))
13520, 46prssd 4817 . . . . . . . . . . . 12 (πœ‘ β†’ {𝑋, π‘Œ} βŠ† 𝐡)
136135, 19sstrd 3984 . . . . . . . . . . 11 (πœ‘ β†’ {𝑋, π‘Œ} βŠ† (Baseβ€˜π‘Š))
137 lindsss 21679 . . . . . . . . . . . 12 ((π‘Š ∈ LMod ∧ 𝐡 ∈ (LIndSβ€˜π‘Š) ∧ {𝑋, π‘Œ} βŠ† 𝐡) β†’ {𝑋, π‘Œ} ∈ (LIndSβ€˜π‘Š))
13859, 17, 135, 137syl3anc 1368 . . . . . . . . . . 11 (πœ‘ β†’ {𝑋, π‘Œ} ∈ (LIndSβ€˜π‘Š))
1396, 9, 8, 7, 10, 54islinds5 32911 . . . . . . . . . . . 12 ((π‘Š ∈ LMod ∧ {𝑋, π‘Œ} βŠ† (Baseβ€˜π‘Š)) β†’ ({𝑋, π‘Œ} ∈ (LIndSβ€˜π‘Š) ↔ βˆ€π‘Ž ∈ (𝐹 ↑m {𝑋, π‘Œ})((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ π‘Ž = ({𝑋, π‘Œ} Γ— { 0 }))))
140139biimpa 476 . . . . . . . . . . 11 (((π‘Š ∈ LMod ∧ {𝑋, π‘Œ} βŠ† (Baseβ€˜π‘Š)) ∧ {𝑋, π‘Œ} ∈ (LIndSβ€˜π‘Š)) β†’ βˆ€π‘Ž ∈ (𝐹 ↑m {𝑋, π‘Œ})((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ π‘Ž = ({𝑋, π‘Œ} Γ— { 0 })))
14159, 136, 138, 140syl21anc 835 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘Ž ∈ (𝐹 ↑m {𝑋, π‘Œ})((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ π‘Ž = ({𝑋, π‘Œ} Γ— { 0 })))
142141adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βˆ€π‘Ž ∈ (𝐹 ↑m {𝑋, π‘Œ})((π‘Ž finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ ((π‘Žβ€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ π‘Ž = ({𝑋, π‘Œ} Γ— { 0 })))
1439fvexi 6895 . . . . . . . . . . . 12 𝐹 ∈ V
144143a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝐹 ∈ V)
145138elexd 3487 . . . . . . . . . . . 12 (πœ‘ β†’ {𝑋, π‘Œ} ∈ V)
146145adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {𝑋, π‘Œ} ∈ V)
147144, 146elmapd 8829 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} ∈ (𝐹 ↑m {𝑋, π‘Œ}) ↔ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}:{𝑋, π‘Œ}⟢𝐹))
14872, 147mpbird 257 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} ∈ (𝐹 ↑m {𝑋, π‘Œ}))
149134, 142, 148rspcdva 3605 . . . . . . . 8 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} finSupp 0 ∧ (π‘Š Ξ£g (𝑏 ∈ {𝑋, π‘Œ} ↦ (({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩}β€˜π‘) Β· 𝑏))) = (0gβ€˜π‘Š)) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = ({𝑋, π‘Œ} Γ— { 0 })))
15057, 125, 149mp2and 696 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = ({𝑋, π‘Œ} Γ— { 0 }))
151 xpprsng 7130 . . . . . . . 8 ((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 0 ∈ V) β†’ ({𝑋, π‘Œ} Γ— { 0 }) = {βŸ¨π‘‹, 0 ⟩, βŸ¨π‘Œ, 0 ⟩})
15231, 47, 56, 151syl3anc 1368 . . . . . . 7 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ ({𝑋, π‘Œ} Γ— { 0 }) = {βŸ¨π‘‹, 0 ⟩, βŸ¨π‘Œ, 0 ⟩})
153150, 152eqtrd 2764 . . . . . 6 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = {βŸ¨π‘‹, 0 ⟩, βŸ¨π‘Œ, 0 ⟩})
154 opthprneg 4857 . . . . . . 7 (((βŸ¨π‘‹, 𝐾⟩ ∈ V ∧ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∈ V) ∧ (βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∧ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩)) β†’ ({βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = {βŸ¨π‘‹, 0 ⟩, βŸ¨π‘Œ, 0 ⟩} ↔ (βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩ ∧ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ = βŸ¨π‘Œ, 0 ⟩)))
155154biimpa 476 . . . . . 6 ((((βŸ¨π‘‹, 𝐾⟩ ∈ V ∧ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∈ V) ∧ (βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ ∧ βŸ¨π‘‹, 𝐾⟩ β‰  βŸ¨π‘Œ, 0 ⟩)) ∧ {βŸ¨π‘‹, 𝐾⟩, βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩} = {βŸ¨π‘‹, 0 ⟩, βŸ¨π‘Œ, 0 ⟩}) β†’ (βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩ ∧ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ = βŸ¨π‘Œ, 0 ⟩))
15634, 36, 45, 153, 155syl1111anc 837 . . . . 5 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩ ∧ βŸ¨π‘Œ, ((invgβ€˜(Scalarβ€˜π‘Š))β€˜πΏ)⟩ = βŸ¨π‘Œ, 0 ⟩))
157156simpld 494 . . . 4 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩)
158 opthg 5467 . . . . 5 ((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) β†’ (βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩ ↔ (𝑋 = 𝑋 ∧ 𝐾 = 0 )))
159158simplbda 499 . . . 4 (((𝑋 ∈ 𝐡 ∧ 𝐾 ∈ 𝐹) ∧ βŸ¨π‘‹, 𝐾⟩ = βŸ¨π‘‹, 0 ⟩) β†’ 𝐾 = 0 )
16031, 32, 157, 159syl21anc 835 . . 3 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝐾 = 0 )
161 linds2eq.11 . . . 4 (πœ‘ β†’ 𝐾 β‰  0 )
162161adantr 480 . . 3 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ 𝐾 β‰  0 )
163160, 162pm2.21ddne 3018 . 2 ((πœ‘ ∧ 𝑋 β‰  π‘Œ) β†’ (𝑋 = π‘Œ ∧ 𝐾 = 𝐿))
16430, 163pm2.61dane 3021 1 (πœ‘ β†’ (𝑋 = π‘Œ ∧ 𝐾 = 𝐿))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   = wceq 1533   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  Vcvv 3466   βŠ† wss 3940  {csn 4620  {cpr 4622  βŸ¨cop 4626   class class class wbr 5138   ↦ cmpt 5221   Γ— cxp 5664  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401   ↑m cmap 8815  Fincfn 8934   finSupp cfsupp 9356  Basecbs 17140  +gcplusg 17193  Scalarcsca 17196   ·𝑠 cvsca 17197  0gc0g 17381   Ξ£g cgsu 17382  Grpcgrp 18850  invgcminusg 18851  -gcsg 18852  CMndccmn 19685  Ringcrg 20123  LModclmod 20691  LVecclvec 20935  LIndSclinds 21660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8698  df-map 8817  df-ixp 8887  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-fsupp 9357  df-sup 9432  df-oi 9500  df-card 9929  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-fz 13481  df-fzo 13624  df-seq 13963  df-hash 14287  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-hom 17217  df-cco 17218  df-0g 17383  df-gsum 17384  df-prds 17389  df-pws 17391  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18560  df-sgrp 18639  df-mnd 18655  df-mhm 18700  df-submnd 18701  df-grp 18853  df-minusg 18854  df-sbg 18855  df-mulg 18983  df-subg 19035  df-ghm 19124  df-cntz 19218  df-cmn 19687  df-abl 19688  df-mgp 20025  df-rng 20043  df-ur 20072  df-ring 20125  df-oppr 20221  df-dvdsr 20244  df-unit 20245  df-invr 20275  df-nzr 20400  df-subrg 20456  df-drng 20574  df-lmod 20693  df-lss 20764  df-lsp 20804  df-lmhm 20855  df-lbs 20908  df-lvec 20936  df-sra 21006  df-rgmod 21007  df-dsmm 21587  df-frlm 21602  df-uvc 21638  df-lindf 21661  df-linds 21662
This theorem is referenced by:  fedgmul  33161
  Copyright terms: Public domain W3C validator