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 ⊢N=LSpan⁡W
lindsun.0 ⊢0˙=0W
lindsun.w ⊢φ→W∈LVec
lindsun.u ⊢φ→U∈LIndS⁡W
lindsun.v ⊢φ→V∈LIndS⁡W
lindsun.2 ⊢φ→N⁡U∩N⁡V=0˙
Assertion lindsun ⊢φ→U∪V∈LIndS⁡W

Proof

Step Hyp Ref Expression
1 lindsun.n ⊢N=LSpan⁡W
2 lindsun.0 ⊢0˙=0W
3 lindsun.w ⊢φ→W∈LVec
4 lindsun.u ⊢φ→U∈LIndS⁡W
5 lindsun.v ⊢φ→V∈LIndS⁡W
6 lindsun.2 ⊢φ→N⁡U∩N⁡V=0˙
7 lveclmod ⊢W∈LVec→W∈LMod
8 3 7 syl ⊢φ→W∈LMod
9 eqid ⊢BaseW=BaseW
10 9 linds1 ⊢U∈LIndS⁡W→U⊆BaseW
11 4 10 syl ⊢φ→U⊆BaseW
12 9 linds1 ⊢V∈LIndS⁡W→V⊆BaseW
13 5 12 syl ⊢φ→V⊆BaseW
14 11 13 unssd ⊢φ→U∪V⊆BaseW
15 3 ad3antrrr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U→W∈LVec
16 4 ad3antrrr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U→U∈LIndS⁡W
17 5 ad3antrrr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U→V∈LIndS⁡W
18 6 ad3antrrr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U→N⁡U∩N⁡V=0˙
19 eqid ⊢0Scalar⁡W=0Scalar⁡W
20 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
21 simpr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U→c∈U
22 simpllr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U→k∈BaseScalar⁡W∖0Scalar⁡W
23 simplr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U→k⋅Wc∈N⁡U∪V∖c
24 1 2 15 16 17 18 19 20 21 22 23 lindsunlem ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U→⊥
25 24 adantlr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U∪V∧c∈U→⊥
26 3 ad3antrrr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈V→W∈LVec
27 5 ad3antrrr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈V→V∈LIndS⁡W
28 4 ad3antrrr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈V→U∈LIndS⁡W
29 incom ⊢N⁡U∩N⁡V=N⁡V∩N⁡U
30 29 6 eqtr3id ⊢φ→N⁡V∩N⁡U=0˙
31 30 ad3antrrr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈V→N⁡V∩N⁡U=0˙
32 simpr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈V→c∈V
33 simpllr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈V→k∈BaseScalar⁡W∖0Scalar⁡W
34 simplr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈V→k⋅Wc∈N⁡U∪V∖c
35 uncom ⊢U∪V=V∪U
36 35 difeq1i ⊢U∪V∖c=V∪U∖c
37 36 fveq2i ⊢N⁡U∪V∖c=N⁡V∪U∖c
38 34 37 eleqtrdi ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈V→k⋅Wc∈N⁡V∪U∖c
39 1 2 26 27 28 31 19 20 32 33 38 lindsunlem ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈V→⊥
40 39 adantlr ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U∪V∧c∈V→⊥
41 elun ⊢c∈U∪V↔c∈U∨c∈V
42 41 biimpi ⊢c∈U∪V→c∈U∨c∈V
43 42 adantl ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U∪V→c∈U∨c∈V
44 25 40 43 mpjaodan ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧k⋅Wc∈N⁡U∪V∖c∧c∈U∪V→⊥
45 44 an32s ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧c∈U∪V∧k⋅Wc∈N⁡U∪V∖c→⊥
46 45 inegd ⊢φ∧k∈BaseScalar⁡W∖0Scalar⁡W∧c∈U∪V→¬k⋅Wc∈N⁡U∪V∖c
47 46 an32s ⊢φ∧c∈U∪V∧k∈BaseScalar⁡W∖0Scalar⁡W→¬k⋅Wc∈N⁡U∪V∖c
48 47 anasss ⊢φ∧c∈U∪V∧k∈BaseScalar⁡W∖0Scalar⁡W→¬k⋅Wc∈N⁡U∪V∖c
49 48 ralrimivva ⊢φ→∀c∈U∪V∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅Wc∈N⁡U∪V∖c
50 eqid ⊢⋅W=⋅W
51 eqid ⊢Scalar⁡W=Scalar⁡W
52 9 50 1 51 20 19 islinds2 ⊢W∈LMod→U∪V∈LIndS⁡W↔U∪V⊆BaseW∧∀c∈U∪V∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅Wc∈N⁡U∪V∖c
53 52 biimpar ⊢W∈LMod∧U∪V⊆BaseW∧∀c∈U∪V∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅Wc∈N⁡U∪V∖c→U∪V∈LIndS⁡W
54 8 14 49 53 syl12anc ⊢φ→U∪V∈LIndS⁡W