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 ˙ = 0 W
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 ˙ = 0 W
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 ⊢ Base W = Base W
10 9 linds1 ⊢ U ∈ LIndS ⁡ W → U ⊆ Base W
11 4 10 syl ⊢ φ → U ⊆ Base W
12 9 linds1 ⊢ V ∈ LIndS ⁡ W → V ⊆ Base W
13 5 12 syl ⊢ φ → V ⊆ Base W
14 11 13 unssd ⊢ φ → U ∪ V ⊆ Base W
15 3 ad3antrrr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U → W ∈ LVec
16 4 ad3antrrr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U → U ∈ LIndS ⁡ W
17 5 ad3antrrr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U → V ∈ LIndS ⁡ W
18 6 ad3antrrr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U → N ⁡ U ∩ N ⁡ V = 0 ˙
19 eqid ⊢ 0 Scalar ⁡ W = 0 Scalar ⁡ W
20 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
21 simpr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U → c ∈ U
22 simpllr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U → k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W
23 simplr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U → k ⋅ W c ∈ N ⁡ U ∪ V ∖ c
24 1 2 15 16 17 18 19 20 21 22 23 lindsunlem ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U → ⊥
25 24 adantlr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U ∪ V ∧ c ∈ U → ⊥
26 3 ad3antrrr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ V → W ∈ LVec
27 5 ad3antrrr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ V → V ∈ LIndS ⁡ W
28 4 ad3antrrr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ 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 ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ V → N ⁡ V ∩ N ⁡ U = 0 ˙
32 simpr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ V → c ∈ V
33 simpllr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ V → k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W
34 simplr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ V → k ⋅ W c ∈ 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 ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ V → k ⋅ W c ∈ N ⁡ V ∪ U ∖ c
39 1 2 26 27 28 31 19 20 32 33 38 lindsunlem ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ V → ⊥
40 39 adantlr ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ 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 ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U ∪ V → c ∈ U ∨ c ∈ V
44 25 40 43 mpjaodan ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c ∧ c ∈ U ∪ V → ⊥
45 44 an32s ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ c ∈ U ∪ V ∧ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c → ⊥
46 45 inegd ⊢ φ ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ∧ c ∈ U ∪ V → ¬ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c
47 46 an32s ⊢ φ ∧ c ∈ U ∪ V ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W → ¬ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c
48 47 anasss ⊢ φ ∧ c ∈ U ∪ V ∧ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W → ¬ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c
49 48 ralrimivva ⊢ φ → ∀ c ∈ U ∪ V ∀ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ k ⋅ W c ∈ 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 ⊆ Base W ∧ ∀ c ∈ U ∪ V ∀ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c
53 52 biimpar ⊢ W ∈ LMod ∧ U ∪ V ⊆ Base W ∧ ∀ c ∈ U ∪ V ∀ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ k ⋅ W c ∈ N ⁡ U ∪ V ∖ c → U ∪ V ∈ LIndS ⁡ W
54 8 14 49 53 syl12anc ⊢ φ → U ∪ V ∈ LIndS ⁡ W