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. = ( 0g ` W )
lindsun.w 
|- ( ph -> W e. LVec )
lindsun.u 
|- ( ph -> U e. ( LIndS ` W ) )
lindsun.v 
|- ( ph -> V e. ( LIndS ` W ) )
lindsun.2 
|- ( ph -> ( ( N ` U ) i^i ( N ` V ) ) = { .0. } )
Assertion lindsun 
|- ( ph -> ( U u. V ) e. ( LIndS ` W ) )

Proof

Step Hyp Ref Expression
1 lindsun.n 
 |-  N = ( LSpan ` W )
2 lindsun.0 
 |-  .0. = ( 0g ` W )
3 lindsun.w 
 |-  ( ph -> W e. LVec )
4 lindsun.u 
 |-  ( ph -> U e. ( LIndS ` W ) )
5 lindsun.v 
 |-  ( ph -> V e. ( LIndS ` W ) )
6 lindsun.2 
 |-  ( ph -> ( ( N ` U ) i^i ( N ` V ) ) = { .0. } )
7 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
8 3 7 syl 
 |-  ( ph -> W e. LMod )
9 eqid 
 |-  ( Base ` W ) = ( Base ` W )
10 9 linds1 
 |-  ( U e. ( LIndS ` W ) -> U C_ ( Base ` W ) )
11 4 10 syl 
 |-  ( ph -> U C_ ( Base ` W ) )
12 9 linds1 
 |-  ( V e. ( LIndS ` W ) -> V C_ ( Base ` W ) )
13 5 12 syl 
 |-  ( ph -> V C_ ( Base ` W ) )
14 11 13 unssd 
 |-  ( ph -> ( U u. V ) C_ ( Base ` W ) )
15 3 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. U ) -> W e. LVec )
16 4 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. U ) -> U e. ( LIndS ` W ) )
17 5 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. U ) -> V e. ( LIndS ` W ) )
18 6 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. U ) -> ( ( N ` U ) i^i ( N ` V ) ) = { .0. } )
19 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
20 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
21 simpr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. U ) -> c e. U )
22 simpllr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. U ) -> k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) )
23 simplr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. U ) -> ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) )
24 1 2 15 16 17 18 19 20 21 22 23 lindsunlem 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. U ) -> F. )
25 24 adantlr 
 |-  ( ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. ( U u. V ) ) /\ c e. U ) -> F. )
26 3 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. V ) -> W e. LVec )
27 5 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. V ) -> V e. ( LIndS ` W ) )
28 4 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. V ) -> U e. ( LIndS ` W ) )
29 incom 
 |-  ( ( N ` U ) i^i ( N ` V ) ) = ( ( N ` V ) i^i ( N ` U ) )
30 29 6 eqtr3id 
 |-  ( ph -> ( ( N ` V ) i^i ( N ` U ) ) = { .0. } )
31 30 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. V ) -> ( ( N ` V ) i^i ( N ` U ) ) = { .0. } )
32 simpr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. V ) -> c e. V )
33 simpllr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. V ) -> k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) )
34 simplr 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. V ) -> ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) )
35 uncom 
 |-  ( U u. V ) = ( V u. U )
36 35 difeq1i 
 |-  ( ( U u. V ) \ { c } ) = ( ( V u. U ) \ { c } )
37 36 fveq2i 
 |-  ( N ` ( ( U u. V ) \ { c } ) ) = ( N ` ( ( V u. U ) \ { c } ) )
38 34 37 eleqtrdi 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. V ) -> ( k ( .s ` W ) c ) e. ( N ` ( ( V u. U ) \ { c } ) ) )
39 1 2 26 27 28 31 19 20 32 33 38 lindsunlem 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. V ) -> F. )
40 39 adantlr 
 |-  ( ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. ( U u. V ) ) /\ c e. V ) -> F. )
41 elun 
 |-  ( c e. ( U u. V ) <-> ( c e. U \/ c e. V ) )
42 41 biimpi 
 |-  ( c e. ( U u. V ) -> ( c e. U \/ c e. V ) )
43 42 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. ( U u. V ) ) -> ( c e. U \/ c e. V ) )
44 25 40 43 mpjaodan 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) /\ c e. ( U u. V ) ) -> F. )
45 44 an32s 
 |-  ( ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ c e. ( U u. V ) ) /\ ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) -> F. )
46 45 inegd 
 |-  ( ( ( ph /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) /\ c e. ( U u. V ) ) -> -. ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) )
47 46 an32s 
 |-  ( ( ( ph /\ c e. ( U u. V ) ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) -> -. ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) )
48 47 anasss 
 |-  ( ( ph /\ ( c e. ( U u. V ) /\ k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) )
49 48 ralrimivva 
 |-  ( ph -> A. c e. ( U u. V ) A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) )
50 eqid 
 |-  ( .s ` W ) = ( .s ` W )
51 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
52 9 50 1 51 20 19 islinds2 
 |-  ( W e. LMod -> ( ( U u. V ) e. ( LIndS ` W ) <-> ( ( U u. V ) C_ ( Base ` W ) /\ A. c e. ( U u. V ) A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) ) )
53 52 biimpar 
 |-  ( ( W e. LMod /\ ( ( U u. V ) C_ ( Base ` W ) /\ A. c e. ( U u. V ) A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) c ) e. ( N ` ( ( U u. V ) \ { c } ) ) ) ) -> ( U u. V ) e. ( LIndS ` W ) )
54 8 14 49 53 syl12anc 
 |-  ( ph -> ( U u. V ) e. ( LIndS ` W ) )