Metamath Proof Explorer

Theorem 0nellinds

Description: The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023)

Ref Expression
Hypothesis 0nellinds.1 ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion 0nellinds ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) → ¬ 0 ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 0nellinds.1 ⊢ 0 = ( 0g ‘ 𝑊 )
2 oveq2 ⊢ ( 𝑥 = 0 → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) )
3 sneq ⊢ ( 𝑥 = 0 → { 𝑥 } = { 0 } )
4 3 difeq2d ⊢ ( 𝑥 = 0 → ( 𝐹 ∖ { 𝑥 } ) = ( 𝐹 ∖ { 0 } ) )
5 4 fveq2d ⊢ ( 𝑥 = 0 → ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑥 } ) ) = ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) )
6 2 5 eleq12d ⊢ ( 𝑥 = 0 → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑥 } ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) ) )
7 6 notbid ⊢ ( 𝑥 = 0 → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑥 } ) ) ↔ ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) ) )
8 7 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑥 } ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) ) )
9 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
11 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
12 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
13 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
14 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
15 9 10 11 12 13 14 islinds2 ⊢ ( 𝑊 ∈ LVec → ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝐹 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) )
16 15 simplbda ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑥 } ) ) )
17 16 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 𝑥 } ) ) )
18 simpr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → 0 ∈ 𝐹 )
19 8 17 18 rspcdva ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) )
20 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
21 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
22 12 13 21 lmod1cl ⊢ ( 𝑊 ∈ LMod → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
23 20 22 syl ⊢ ( 𝑊 ∈ LVec → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
24 23 adantr ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
25 12 lvecdrng ⊢ ( 𝑊 ∈ LVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
26 14 21 drngunz ⊢ ( ( Scalar ‘ 𝑊 ) ∈ DivRing → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
27 25 26 syl ⊢ ( 𝑊 ∈ LVec → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
28 27 adantr ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
29 eldifsn ⊢ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ↔ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
30 24 28 29 sylanbrc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
31 30 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
32 20 ad2antrr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → 𝑊 ∈ LMod )
33 12 10 13 1 lmodvs0 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 0 ) = 0 )
34 32 22 33 syl2anc2 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 0 ) = 0 )
35 9 linds1 ⊢ ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) → 𝐹 ⊆ ( Base ‘ 𝑊 ) )
36 35 ad2antlr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → 𝐹 ⊆ ( Base ‘ 𝑊 ) )
37 36 ssdifssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → ( 𝐹 ∖ { 0 } ) ⊆ ( Base ‘ 𝑊 ) )
38 1 9 11 0ellsp ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐹 ∖ { 0 } ) ⊆ ( Base ‘ 𝑊 ) ) → 0 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) )
39 32 37 38 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → 0 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) )
40 34 39 eqeltrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) )
41 oveq1 ⊢ ( 𝑘 = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) = ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 0 ) )
42 41 eleq1d ⊢ ( 𝑘 = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) ↔ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) ) )
43 42 rspcev ⊢ ( ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) ) → ∃ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) )
44 31 40 43 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → ∃ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) )
45 dfrex2 ⊢ ( ∃ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) ↔ ¬ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) )
46 44 45 sylib ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ∧ 0 ∈ 𝐹 ) → ¬ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 0 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 ∖ { 0 } ) ) )
47 19 46 pm2.65da ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) → ¬ 0 ∈ 𝐹 )