Metamath Proof Explorer

Theorem lindsun

Description: Condition for the union of two independent sets to be an independent set. (Contributed by Thierry Arnoux, 9-May-2023)

Ref Expression
Hypotheses lindsun.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lindsun.0 ⊢ 0 = ( 0g ‘ 𝑊 )
lindsun.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lindsun.u ⊢ ( 𝜑 → 𝑈 ∈ ( LIndS ‘ 𝑊 ) )
lindsun.v ⊢ ( 𝜑 → 𝑉 ∈ ( LIndS ‘ 𝑊 ) )
lindsun.2 ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑈 ) ∩ ( 𝑁 ‘ 𝑉 ) ) = { 0 } )
Assertion lindsun ( 𝜑 → ( 𝑈 ∪ 𝑉 ) ∈ ( LIndS ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 lindsun.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
2 lindsun.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 lindsun.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
4 lindsun.u ⊢ ( 𝜑 → 𝑈 ∈ ( LIndS ‘ 𝑊 ) )
5 lindsun.v ⊢ ( 𝜑 → 𝑉 ∈ ( LIndS ‘ 𝑊 ) )
6 lindsun.2 ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑈 ) ∩ ( 𝑁 ‘ 𝑉 ) ) = { 0 } )
7 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
8 3 7 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
9 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10 9 linds1 ⊢ ( 𝑈 ∈ ( LIndS ‘ 𝑊 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
11 4 10 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
12 9 linds1 ⊢ ( 𝑉 ∈ ( LIndS ‘ 𝑊 ) → 𝑉 ⊆ ( Base ‘ 𝑊 ) )
13 5 12 syl ⊢ ( 𝜑 → 𝑉 ⊆ ( Base ‘ 𝑊 ) )
14 11 13 unssd ⊢ ( 𝜑 → ( 𝑈 ∪ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) )
15 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑈 ) → 𝑊 ∈ LVec )
16 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑈 ) → 𝑈 ∈ ( LIndS ‘ 𝑊 ) )
17 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑈 ) → 𝑉 ∈ ( LIndS ‘ 𝑊 ) )
18 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑈 ) → ( ( 𝑁 ‘ 𝑈 ) ∩ ( 𝑁 ‘ 𝑉 ) ) = { 0 } )
19 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
20 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
21 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑈 ) → 𝑐 ∈ 𝑈 )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑈 ) → 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
23 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑈 ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) )
24 1 2 15 16 17 18 19 20 21 22 23 lindsunlem ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑈 ) → ⊥ )
25 24 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ) ∧ 𝑐 ∈ 𝑈 ) → ⊥ )
26 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑊 ∈ LVec )
27 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑉 ∈ ( LIndS ‘ 𝑊 ) )
28 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑈 ∈ ( LIndS ‘ 𝑊 ) )
29 incom ⊢ ( ( 𝑁 ‘ 𝑈 ) ∩ ( 𝑁 ‘ 𝑉 ) ) = ( ( 𝑁 ‘ 𝑉 ) ∩ ( 𝑁 ‘ 𝑈 ) )
30 29 6 eqtr3id ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑉 ) ∩ ( 𝑁 ‘ 𝑈 ) ) = { 0 } )
31 30 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝑉 ) ∩ ( 𝑁 ‘ 𝑈 ) ) = { 0 } )
32 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑐 ∈ 𝑉 )
33 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑉 ) → 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
34 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑉 ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) )
35 uncom ⊢ ( 𝑈 ∪ 𝑉 ) = ( 𝑉 ∪ 𝑈 )
36 35 difeq1i ⊢ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) = ( ( 𝑉 ∪ 𝑈 ) ∖ { 𝑐 } )
37 36 fveq2i ⊢ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) = ( 𝑁 ‘ ( ( 𝑉 ∪ 𝑈 ) ∖ { 𝑐 } ) )
38 34 37 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑉 ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑉 ∪ 𝑈 ) ∖ { 𝑐 } ) ) )
39 1 2 26 27 28 31 19 20 32 33 38 lindsunlem ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ 𝑉 ) → ⊥ )
40 39 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) → ⊥ )
41 elun ⊢ ( 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ↔ ( 𝑐 ∈ 𝑈 ∨ 𝑐 ∈ 𝑉 ) )
42 41 bilani ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ) → ( 𝑐 ∈ 𝑈 ∨ 𝑐 ∈ 𝑉 ) )
43 25 40 42 mpjaodan ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ∧ 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ) → ⊥ )
44 43 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) → ⊥ )
45 44 inegd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ∧ 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) )
46 45 an32s ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) )
47 46 anasss ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) )
48 47 ralrimivva ⊢ ( 𝜑 → ∀ 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) )
49 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
50 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
51 9 49 1 50 20 19 islinds2 ⊢ ( 𝑊 ∈ LMod → ( ( 𝑈 ∪ 𝑉 ) ∈ ( LIndS ‘ 𝑊 ) ↔ ( ( 𝑈 ∪ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ) )
52 51 biimpar ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑈 ∪ 𝑉 ) ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑐 ∈ ( 𝑈 ∪ 𝑉 ) ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑐 ) ∈ ( 𝑁 ‘ ( ( 𝑈 ∪ 𝑉 ) ∖ { 𝑐 } ) ) ) ) → ( 𝑈 ∪ 𝑉 ) ∈ ( LIndS ‘ 𝑊 ) )
53 8 14 48 52 syl12anc ⊢ ( 𝜑 → ( 𝑈 ∪ 𝑉 ) ∈ ( LIndS ‘ 𝑊 ) )