# Metamath Proof Explorer

## Theorem lmodindp1

Description: Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015)

Ref Expression
Hypotheses lmodindp1.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lmodindp1.p
lmodindp1.o
lmodindp1.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lmodindp1.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lmodindp1.x ${⊢}{\phi }\to {X}\in {V}$
lmodindp1.y ${⊢}{\phi }\to {Y}\in {V}$
lmodindp1.q ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
Assertion lmodindp1

### Proof

Step Hyp Ref Expression
1 lmodindp1.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lmodindp1.p
3 lmodindp1.o
4 lmodindp1.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
5 lmodindp1.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
6 lmodindp1.x ${⊢}{\phi }\to {X}\in {V}$
7 lmodindp1.y ${⊢}{\phi }\to {Y}\in {V}$
8 lmodindp1.q ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
9 eqid ${⊢}{inv}_{g}\left({W}\right)={inv}_{g}\left({W}\right)$
10 1 9 4 lspsnneg ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {N}\left(\left\{{inv}_{g}\left({W}\right)\left({X}\right)\right\}\right)={N}\left(\left\{{X}\right\}\right)$
11 5 6 10 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{inv}_{g}\left({W}\right)\left({X}\right)\right\}\right)={N}\left(\left\{{X}\right\}\right)$
12 11 eqcomd ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{inv}_{g}\left({W}\right)\left({X}\right)\right\}\right)$
14 lmodgrp ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Grp}$
15 5 14 syl ${⊢}{\phi }\to {W}\in \mathrm{Grp}$