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 ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
lindfind2.l ⊢ 𝐿 = ( Scalar ‘ 𝑊 )
Assertion lindsind2 ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐸 ∈ 𝐹 ) → ¬ 𝐸 ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝐸 } ) ) )

Proof

Step Hyp Ref Expression
1 lindfind2.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
2 lindfind2.l ⊢ 𝐿 = ( Scalar ‘ 𝑊 )
3 simp1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐸 ∈ 𝐹 ) → ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) )
4 linds2 ⊢ ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) → ( I ↾ 𝐹 ) LIndF 𝑊 )
5 4 3ad2ant2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐸 ∈ 𝐹 ) → ( I ↾ 𝐹 ) LIndF 𝑊 )
6 dmresi ⊢ dom ( I ↾ 𝐹 ) = 𝐹
7 6 eleq2i ⊢ ( 𝐸 ∈ dom ( I ↾ 𝐹 ) ↔ 𝐸 ∈ 𝐹 )
8 7 biimpri ⊢ ( 𝐸 ∈ 𝐹 → 𝐸 ∈ dom ( I ↾ 𝐹 ) )
9 8 3ad2ant3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐸 ∈ 𝐹 ) → 𝐸 ∈ dom ( I ↾ 𝐹 ) )
10 1 2 lindfind2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ ( I ↾ 𝐹 ) LIndF 𝑊 ∧ 𝐸 ∈ dom ( I ↾ 𝐹 ) ) → ¬ ( ( I ↾ 𝐹 ) ‘ 𝐸 ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝐸 } ) ) ) )
11 3 5 9 10 syl3anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐸 ∈ 𝐹 ) → ¬ ( ( I ↾ 𝐹 ) ‘ 𝐸 ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝐸 } ) ) ) )
12 fvresi ⊢ ( 𝐸 ∈ 𝐹 → ( ( I ↾ 𝐹 ) ‘ 𝐸 ) = 𝐸 )
13 6 difeq1i ⊢ ( dom ( I ↾ 𝐹 ) ∖ { 𝐸 } ) = ( 𝐹 ∖ { 𝐸 } )
14 13 imaeq2i ⊢ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝐸 } ) ) = ( ( I ↾ 𝐹 ) “ ( 𝐹 ∖ { 𝐸 } ) )
15 difss ⊢ ( 𝐹 ∖ { 𝐸 } ) ⊆ 𝐹
16 resiima ⊢ ( ( 𝐹 ∖ { 𝐸 } ) ⊆ 𝐹 → ( ( I ↾ 𝐹 ) “ ( 𝐹 ∖ { 𝐸 } ) ) = ( 𝐹 ∖ { 𝐸 } ) )
17 15 16 ax-mp ⊢ ( ( I ↾ 𝐹 ) “ ( 𝐹 ∖ { 𝐸 } ) ) = ( 𝐹 ∖ { 𝐸 } )
18 14 17 eqtri ⊢ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝐸 } ) ) = ( 𝐹 ∖ { 𝐸 } )
19 18 fveq2i ⊢ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝐸 } ) ) ) = ( 𝐾 ‘ ( 𝐹 ∖ { 𝐸 } ) )
20 19 a1i ⊢ ( 𝐸 ∈ 𝐹 → ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝐸 } ) ) ) = ( 𝐾 ‘ ( 𝐹 ∖ { 𝐸 } ) ) )
21 12 20 eleq12d ⊢ ( 𝐸 ∈ 𝐹 → ( ( ( I ↾ 𝐹 ) ‘ 𝐸 ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝐸 } ) ) ) ↔ 𝐸 ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝐸 } ) ) ) )
22 21 3ad2ant3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐸 ∈ 𝐹 ) → ( ( ( I ↾ 𝐹 ) ‘ 𝐸 ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝐸 } ) ) ) ↔ 𝐸 ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝐸 } ) ) ) )
23 11 22 mtbid ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐿 ∈ NzRing ) ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐸 ∈ 𝐹 ) → ¬ 𝐸 ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝐸 } ) ) )