Metamath Proof Explorer

Theorem lindfind2

Description: In a linearly independent family 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 lindfind2 ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → ¬ F ⁡ E ∈ K ⁡ F dom ⁡ F ∖ E

Proof

Step Hyp Ref Expression
1 lindfind2.k ⊢ K = LSpan ⁡ W
2 lindfind2.l ⊢ L = Scalar ⁡ W
3 simp1l ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → W ∈ LMod
4 simp2 ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → F LIndF W
5 eqid ⊢ Base W = Base W
6 5 lindff ⊢ F LIndF W ∧ W ∈ LMod → F : dom ⁡ F ⟶ Base W
7 4 3 6 syl2anc ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → F : dom ⁡ F ⟶ Base W
8 simp3 ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → E ∈ dom ⁡ F
9 7 8 ffvelrnd ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → F ⁡ E ∈ Base W
10 eqid ⊢ ⋅ W = ⋅ W
11 eqid ⊢ 1 L = 1 L
12 5 2 10 11 lmodvs1 ⊢ W ∈ LMod ∧ F ⁡ E ∈ Base W → 1 L ⋅ W F ⁡ E = F ⁡ E
13 3 9 12 syl2anc ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → 1 L ⋅ W F ⁡ E = F ⁡ E
14 nzrring ⊢ L ∈ NzRing → L ∈ Ring
15 eqid ⊢ Base L = Base L
16 15 11 ringidcl ⊢ L ∈ Ring → 1 L ∈ Base L
17 14 16 syl ⊢ L ∈ NzRing → 1 L ∈ Base L
18 17 adantl ⊢ W ∈ LMod ∧ L ∈ NzRing → 1 L ∈ Base L
19 18 3ad2ant1 ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → 1 L ∈ Base L
20 eqid ⊢ 0 L = 0 L
21 11 20 nzrnz ⊢ L ∈ NzRing → 1 L ≠ 0 L
22 21 adantl ⊢ W ∈ LMod ∧ L ∈ NzRing → 1 L ≠ 0 L
23 22 3ad2ant1 ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → 1 L ≠ 0 L
24 10 1 2 20 15 lindfind ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ 1 L ∈ Base L ∧ 1 L ≠ 0 L → ¬ 1 L ⋅ W F ⁡ E ∈ K ⁡ F dom ⁡ F ∖ E
25 4 8 19 23 24 syl22anc ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → ¬ 1 L ⋅ W F ⁡ E ∈ K ⁡ F dom ⁡ F ∖ E
26 13 25 eqneltrrd ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F LIndF W ∧ E ∈ dom ⁡ F → ¬ F ⁡ E ∈ K ⁡ F dom ⁡ F ∖ E