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 ↾ F LIndF W
5 4 3ad2ant2 ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F ∈ LIndS ⁡ W ∧ E ∈ F → I ↾ F LIndF W
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 ↾ F LIndF W ∧ E ∈ dom ⁡ I ↾ F → ¬ I ↾ F ⁡ E ∈ K ⁡ I ↾ F dom ⁡ I ↾ F ∖ E
11 3 5 9 10 syl3anc ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F ∈ LIndS ⁡ W ∧ E ∈ F → ¬ I ↾ F ⁡ E ∈ K ⁡ I ↾ F dom ⁡ I ↾ F ∖ E
12 fvresi ⊢ E ∈ F → I ↾ F ⁡ E = E
13 6 difeq1i ⊢ dom ⁡ I ↾ F ∖ E = F ∖ E
14 13 imaeq2i ⊢ I ↾ F dom ⁡ I ↾ F ∖ E = I ↾ F F ∖ E
15 difss ⊢ F ∖ E ⊆ F
16 resiima ⊢ F ∖ E ⊆ F → I ↾ F F ∖ E = F ∖ E
17 15 16 ax-mp ⊢ I ↾ F F ∖ E = F ∖ E
18 14 17 eqtri ⊢ I ↾ F dom ⁡ I ↾ F ∖ E = F ∖ E
19 18 fveq2i ⊢ K ⁡ I ↾ F dom ⁡ I ↾ F ∖ E = K ⁡ F ∖ E
20 19 a1i ⊢ E ∈ F → K ⁡ I ↾ F dom ⁡ I ↾ F ∖ E = K ⁡ F ∖ E
21 12 20 eleq12d ⊢ E ∈ F → I ↾ F ⁡ E ∈ K ⁡ I ↾ F dom ⁡ I ↾ F ∖ E ↔ E ∈ K ⁡ F ∖ E
22 21 3ad2ant3 ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F ∈ LIndS ⁡ W ∧ E ∈ F → I ↾ F ⁡ E ∈ K ⁡ I ↾ F dom ⁡ I ↾ F ∖ E ↔ E ∈ K ⁡ F ∖ E
23 11 22 mtbid ⊢ W ∈ LMod ∧ L ∈ NzRing ∧ F ∈ LIndS ⁡ W ∧ E ∈ F → ¬ E ∈ K ⁡ F ∖ E