# Metamath Proof Explorer

## Theorem islininds2

Description: Implication of being a linearly independent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Hypotheses islindeps2.b 𝐵 = ( Base ‘ 𝑀 )
islindeps2.z 𝑍 = ( 0g𝑀 )
islindeps2.r 𝑅 = ( Scalar ‘ 𝑀 )
islindeps2.e 𝐸 = ( Base ‘ 𝑅 )
islindeps2.0 0 = ( 0g𝑅 )
Assertion islininds2 ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵𝑅 ∈ NzRing ) → ( 𝑆 linIndS 𝑀 → ∀ 𝑠𝑆𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) ) )

### Proof

Step Hyp Ref Expression
1 islindeps2.b 𝐵 = ( Base ‘ 𝑀 )
2 islindeps2.z 𝑍 = ( 0g𝑀 )
3 islindeps2.r 𝑅 = ( Scalar ‘ 𝑀 )
4 islindeps2.e 𝐸 = ( Base ‘ 𝑅 )
5 islindeps2.0 0 = ( 0g𝑅 )
6 lindepsnlininds ( ( 𝑆 ∈ 𝒫 𝐵𝑀 ∈ LMod ) → ( 𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀 ) )
7 6 ancoms ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀 ) )
8 7 3adant3 ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵𝑅 ∈ NzRing ) → ( 𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀 ) )
9 8 con2bid ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵𝑅 ∈ NzRing ) → ( 𝑆 linIndS 𝑀 ↔ ¬ 𝑆 linDepS 𝑀 ) )
10 notnotb ( 𝑓 finSupp 0 ↔ ¬ ¬ 𝑓 finSupp 0 )
11 nne ( ¬ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ↔ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 )
12 11 bicomi ( ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ↔ ¬ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 )
13 10 12 anbi12i ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ↔ ( ¬ ¬ 𝑓 finSupp 0 ∧ ¬ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) )
14 pm4.56 ( ( ¬ ¬ 𝑓 finSupp 0 ∧ ¬ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) ↔ ¬ ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) )
15 13 14 bitri ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ↔ ¬ ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) )
16 15 rexbii ( ∃ 𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ↔ ∃ 𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ¬ ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) )
17 rexnal ( ∃ 𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ¬ ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) ↔ ¬ ∀ 𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) )
18 16 17 bitri ( ∃ 𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ↔ ¬ ∀ 𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) )
19 18 rexbii ( ∃ 𝑠𝑆𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ↔ ∃ 𝑠𝑆 ¬ ∀ 𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) )
20 rexnal ( ∃ 𝑠𝑆 ¬ ∀ 𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) ↔ ¬ ∀ 𝑠𝑆𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) )
21 19 20 bitri ( ∃ 𝑠𝑆𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ↔ ¬ ∀ 𝑠𝑆𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) )
22 1 2 3 4 5 islindeps2 ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵𝑅 ∈ NzRing ) → ( ∃ 𝑠𝑆𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) → 𝑆 linDepS 𝑀 ) )
23 21 22 syl5bir ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵𝑅 ∈ NzRing ) → ( ¬ ∀ 𝑠𝑆𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) → 𝑆 linDepS 𝑀 ) )
24 23 con1d ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵𝑅 ∈ NzRing ) → ( ¬ 𝑆 linDepS 𝑀 → ∀ 𝑠𝑆𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) ) )
25 9 24 sylbid ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵𝑅 ∈ NzRing ) → ( 𝑆 linIndS 𝑀 → ∀ 𝑠𝑆𝑓 ∈ ( 𝐸m ( 𝑆 ∖ { 𝑠 } ) ) ( ¬ 𝑓 finSupp 0 ∨ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) ) )