Metamath Proof Explorer

Theorem lindsind2

Description: In a linearly independent set in a module over a nonzero ring, no element is contained in the span of any non-containing set. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses lindfind2.k ⊢K=LSpan⁡W
lindfind2.l ⊢L=Scalar⁡W
Assertion lindsind2 ⊢W∈LMod∧L∈NzRing∧F∈LIndS⁡W∧E∈F→¬E∈K⁡F∖E

Proof

Step Hyp Ref Expression
1 lindfind2.k ⊢K=LSpan⁡W
2 lindfind2.l ⊢L=Scalar⁡W
3 simp1 ⊢W∈LMod∧L∈NzRing∧F∈LIndS⁡W∧E∈F→W∈LMod∧L∈NzRing
4 linds2 ⊢F∈LIndS⁡W→I↾FLIndFW
5 4 3ad2ant2 ⊢W∈LMod∧L∈NzRing∧F∈LIndS⁡W∧E∈F→I↾FLIndFW
6 dmresi ⊢dom⁡I↾F=F
7 6 eleq2i ⊢E∈dom⁡I↾F↔E∈F
8 7 biimpri ⊢E∈F→E∈dom⁡I↾F
9 8 3ad2ant3 ⊢W∈LMod∧L∈NzRing∧F∈LIndS⁡W∧E∈F→E∈dom⁡I↾F
10 1 2 lindfind2 ⊢W∈LMod∧L∈NzRing∧I↾FLIndFW∧E∈dom⁡I↾F→¬I↾F⁡E∈K⁡I↾Fdom⁡I↾F∖E
11 3 5 9 10 syl3anc ⊢W∈LMod∧L∈NzRing∧F∈LIndS⁡W∧E∈F→¬I↾F⁡E∈K⁡I↾Fdom⁡I↾F∖E
12 fvresi ⊢E∈F→I↾F⁡E=E
13 6 difeq1i ⊢dom⁡I↾F∖E=F∖E
14 13 imaeq2i ⊢I↾Fdom⁡I↾F∖E=I↾FF∖E
15 difss ⊢F∖E⊆F
16 resiima ⊢F∖E⊆F→I↾FF∖E=F∖E
17 15 16 ax-mp ⊢I↾FF∖E=F∖E
18 14 17 eqtri ⊢I↾Fdom⁡I↾F∖E=F∖E
19 18 fveq2i ⊢K⁡I↾Fdom⁡I↾F∖E=K⁡F∖E
20 19 a1i ⊢E∈F→K⁡I↾Fdom⁡I↾F∖E=K⁡F∖E
21 12 20 eleq12d ⊢E∈F→I↾F⁡E∈K⁡I↾Fdom⁡I↾F∖E↔E∈K⁡F∖E
22 21 3ad2ant3 ⊢W∈LMod∧L∈NzRing∧F∈LIndS⁡W∧E∈F→I↾F⁡E∈K⁡I↾Fdom⁡I↾F∖E↔E∈K⁡F∖E
23 11 22 mtbid ⊢W∈LMod∧L∈NzRing∧F∈LIndS⁡W∧E∈F→¬E∈K⁡F∖E