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 ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) ≠ 𝑠 ) ) )