Metamath Proof Explorer

Theorem frlmlbs

Description: The unit vectors comprise a basis for a free module. (Contributed by Stefan O'Rear, 6-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmlbs.f 
|- F = ( R freeLMod I )
frlmlbs.u 
|- U = ( R unitVec I )
frlmlbs.j 
|- J = ( LBasis ` F )
Assertion frlmlbs 
|- ( ( R e. Ring /\ I e. V ) -> ran U e. J )

Proof

Step Hyp Ref Expression
1 frlmlbs.f 
 |-  F = ( R freeLMod I )
2 frlmlbs.u 
 |-  U = ( R unitVec I )
3 frlmlbs.j 
 |-  J = ( LBasis ` F )
4 eqid 
 |-  ( Base ` F ) = ( Base ` F )
5 2 1 4 uvcff 
 |-  ( ( R e. Ring /\ I e. V ) -> U : I --> ( Base ` F ) )
6 5 frnd 
 |-  ( ( R e. Ring /\ I e. V ) -> ran U C_ ( Base ` F ) )
7 suppssdm 
 |-  ( a supp ( 0g ` R ) ) C_ dom a
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 1 8 4 frlmbasf 
 |-  ( ( I e. V /\ a e. ( Base ` F ) ) -> a : I --> ( Base ` R ) )
10 9 adantll 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ a e. ( Base ` F ) ) -> a : I --> ( Base ` R ) )
11 7 10 fssdm 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ a e. ( Base ` F ) ) -> ( a supp ( 0g ` R ) ) C_ I )
12 11 ralrimiva 
 |-  ( ( R e. Ring /\ I e. V ) -> A. a e. ( Base ` F ) ( a supp ( 0g ` R ) ) C_ I )
13 rabid2 
 |-  ( ( Base ` F ) = { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ I } <-> A. a e. ( Base ` F ) ( a supp ( 0g ` R ) ) C_ I )
14 12 13 sylibr 
 |-  ( ( R e. Ring /\ I e. V ) -> ( Base ` F ) = { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ I } )
15 ssid 
 |-  I C_ I
16 eqid 
 |-  ( LSpan ` F ) = ( LSpan ` F )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 eqid 
 |-  { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ I } = { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ I }
19 1 2 16 4 17 18 frlmsslsp 
 |-  ( ( R e. Ring /\ I e. V /\ I C_ I ) -> ( ( LSpan ` F ) ` ( U " I ) ) = { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ I } )
20 15 19 mp3an3 
 |-  ( ( R e. Ring /\ I e. V ) -> ( ( LSpan ` F ) ` ( U " I ) ) = { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ I } )
21 ffn 
 |-  ( U : I --> ( Base ` F ) -> U Fn I )
22 fnima 
 |-  ( U Fn I -> ( U " I ) = ran U )
23 5 21 22 3syl 
 |-  ( ( R e. Ring /\ I e. V ) -> ( U " I ) = ran U )
24 23 fveq2d 
 |-  ( ( R e. Ring /\ I e. V ) -> ( ( LSpan ` F ) ` ( U " I ) ) = ( ( LSpan ` F ) ` ran U ) )
25 14 20 24 3eqtr2rd 
 |-  ( ( R e. Ring /\ I e. V ) -> ( ( LSpan ` F ) ` ran U ) = ( Base ` F ) )
26 eqid 
 |-  ( .s ` F ) = ( .s ` F )
27 eqid 
 |-  { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ ( I \ { c } ) } = { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ ( I \ { c } ) }
28 simpll 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> R e. Ring )
29 simplr 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> I e. V )
30 difssd 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> ( I \ { c } ) C_ I )
31 vsnid 
 |-  c e. { c }
32 snssi 
 |-  ( c e. I -> { c } C_ I )
33 32 ad2antrl 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> { c } C_ I )
34 dfss4 
 |-  ( { c } C_ I <-> ( I \ ( I \ { c } ) ) = { c } )
35 33 34 sylib 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> ( I \ ( I \ { c } ) ) = { c } )
36 31 35 eleqtrrid 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> c e. ( I \ ( I \ { c } ) ) )
37 1 frlmsca 
 |-  ( ( R e. Ring /\ I e. V ) -> R = ( Scalar ` F ) )
38 37 fveq2d 
 |-  ( ( R e. Ring /\ I e. V ) -> ( Base ` R ) = ( Base ` ( Scalar ` F ) ) )
39 37 fveq2d 
 |-  ( ( R e. Ring /\ I e. V ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` F ) ) )
40 39 sneqd 
 |-  ( ( R e. Ring /\ I e. V ) -> { ( 0g ` R ) } = { ( 0g ` ( Scalar ` F ) ) } )
41 38 40 difeq12d 
 |-  ( ( R e. Ring /\ I e. V ) -> ( ( Base ` R ) \ { ( 0g ` R ) } ) = ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) )
42 41 eleq2d 
 |-  ( ( R e. Ring /\ I e. V ) -> ( b e. ( ( Base ` R ) \ { ( 0g ` R ) } ) <-> b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) )
43 42 biimpar 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) -> b e. ( ( Base ` R ) \ { ( 0g ` R ) } ) )
44 43 adantrl 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> b e. ( ( Base ` R ) \ { ( 0g ` R ) } ) )
45 1 2 4 8 26 17 27 28 29 30 36 44 frlmssuvc2 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> -. ( b ( .s ` F ) ( U ` c ) ) e. { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ ( I \ { c } ) } )
46 17 8 ringelnzr 
 |-  ( ( R e. Ring /\ b e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) -> R e. NzRing )
47 28 44 46 syl2anc 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> R e. NzRing )
48 2 1 4 uvcf1 
 |-  ( ( R e. NzRing /\ I e. V ) -> U : I -1-1-> ( Base ` F ) )
49 47 29 48 syl2anc 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> U : I -1-1-> ( Base ` F ) )
50 df-f1 
 |-  ( U : I -1-1-> ( Base ` F ) <-> ( U : I --> ( Base ` F ) /\ Fun `' U ) )
51 50 simprbi 
 |-  ( U : I -1-1-> ( Base ` F ) -> Fun `' U )
52 imadif 
 |-  ( Fun `' U -> ( U " ( I \ { c } ) ) = ( ( U " I ) \ ( U " { c } ) ) )
53 49 51 52 3syl 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> ( U " ( I \ { c } ) ) = ( ( U " I ) \ ( U " { c } ) ) )
54 f1fn 
 |-  ( U : I -1-1-> ( Base ` F ) -> U Fn I )
55 49 54 22 3syl 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> ( U " I ) = ran U )
56 49 54 syl 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> U Fn I )
57 simprl 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> c e. I )
58 fnsnfv 
 |-  ( ( U Fn I /\ c e. I ) -> { ( U ` c ) } = ( U " { c } ) )
59 56 57 58 syl2anc 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> { ( U ` c ) } = ( U " { c } ) )
60 59 eqcomd 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> ( U " { c } ) = { ( U ` c ) } )
61 55 60 difeq12d 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> ( ( U " I ) \ ( U " { c } ) ) = ( ran U \ { ( U ` c ) } ) )
62 53 61 eqtr2d 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> ( ran U \ { ( U ` c ) } ) = ( U " ( I \ { c } ) ) )
63 62 fveq2d 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> ( ( LSpan ` F ) ` ( ran U \ { ( U ` c ) } ) ) = ( ( LSpan ` F ) ` ( U " ( I \ { c } ) ) ) )
64 1 2 16 4 17 27 frlmsslsp 
 |-  ( ( R e. Ring /\ I e. V /\ ( I \ { c } ) C_ I ) -> ( ( LSpan ` F ) ` ( U " ( I \ { c } ) ) ) = { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ ( I \ { c } ) } )
65 28 29 30 64 syl3anc 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> ( ( LSpan ` F ) ` ( U " ( I \ { c } ) ) ) = { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ ( I \ { c } ) } )
66 63 65 eqtrd 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> ( ( LSpan ` F ) ` ( ran U \ { ( U ` c ) } ) ) = { a e. ( Base ` F ) | ( a supp ( 0g ` R ) ) C_ ( I \ { c } ) } )
67 45 66 neleqtrrd 
 |-  ( ( ( R e. Ring /\ I e. V ) /\ ( c e. I /\ b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) ) ) -> -. ( b ( .s ` F ) ( U ` c ) ) e. ( ( LSpan ` F ) ` ( ran U \ { ( U ` c ) } ) ) )
68 67 ralrimivva 
 |-  ( ( R e. Ring /\ I e. V ) -> A. c e. I A. b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) -. ( b ( .s ` F ) ( U ` c ) ) e. ( ( LSpan ` F ) ` ( ran U \ { ( U ` c ) } ) ) )
69 oveq2 
 |-  ( a = ( U ` c ) -> ( b ( .s ` F ) a ) = ( b ( .s ` F ) ( U ` c ) ) )
70 sneq 
 |-  ( a = ( U ` c ) -> { a } = { ( U ` c ) } )
71 70 difeq2d 
 |-  ( a = ( U ` c ) -> ( ran U \ { a } ) = ( ran U \ { ( U ` c ) } ) )
72 71 fveq2d 
 |-  ( a = ( U ` c ) -> ( ( LSpan ` F ) ` ( ran U \ { a } ) ) = ( ( LSpan ` F ) ` ( ran U \ { ( U ` c ) } ) ) )
73 69 72 eleq12d 
 |-  ( a = ( U ` c ) -> ( ( b ( .s ` F ) a ) e. ( ( LSpan ` F ) ` ( ran U \ { a } ) ) <-> ( b ( .s ` F ) ( U ` c ) ) e. ( ( LSpan ` F ) ` ( ran U \ { ( U ` c ) } ) ) ) )
74 73 notbid 
 |-  ( a = ( U ` c ) -> ( -. ( b ( .s ` F ) a ) e. ( ( LSpan ` F ) ` ( ran U \ { a } ) ) <-> -. ( b ( .s ` F ) ( U ` c ) ) e. ( ( LSpan ` F ) ` ( ran U \ { ( U ` c ) } ) ) ) )
75 74 ralbidv 
 |-  ( a = ( U ` c ) -> ( A. b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) -. ( b ( .s ` F ) a ) e. ( ( LSpan ` F ) ` ( ran U \ { a } ) ) <-> A. b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) -. ( b ( .s ` F ) ( U ` c ) ) e. ( ( LSpan ` F ) ` ( ran U \ { ( U ` c ) } ) ) ) )
76 75 ralrn 
 |-  ( U Fn I -> ( A. a e. ran U A. b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) -. ( b ( .s ` F ) a ) e. ( ( LSpan ` F ) ` ( ran U \ { a } ) ) <-> A. c e. I A. b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) -. ( b ( .s ` F ) ( U ` c ) ) e. ( ( LSpan ` F ) ` ( ran U \ { ( U ` c ) } ) ) ) )
77 5 21 76 3syl 
 |-  ( ( R e. Ring /\ I e. V ) -> ( A. a e. ran U A. b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) -. ( b ( .s ` F ) a ) e. ( ( LSpan ` F ) ` ( ran U \ { a } ) ) <-> A. c e. I A. b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) -. ( b ( .s ` F ) ( U ` c ) ) e. ( ( LSpan ` F ) ` ( ran U \ { ( U ` c ) } ) ) ) )
78 68 77 mpbird 
 |-  ( ( R e. Ring /\ I e. V ) -> A. a e. ran U A. b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) -. ( b ( .s ` F ) a ) e. ( ( LSpan ` F ) ` ( ran U \ { a } ) ) )
79 1 ovexi 
 |-  F e. _V
80 eqid 
 |-  ( Scalar ` F ) = ( Scalar ` F )
81 eqid 
 |-  ( Base ` ( Scalar ` F ) ) = ( Base ` ( Scalar ` F ) )
82 eqid 
 |-  ( 0g ` ( Scalar ` F ) ) = ( 0g ` ( Scalar ` F ) )
83 4 80 26 81 3 16 82 islbs 
 |-  ( F e. _V -> ( ran U e. J <-> ( ran U C_ ( Base ` F ) /\ ( ( LSpan ` F ) ` ran U ) = ( Base ` F ) /\ A. a e. ran U A. b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) -. ( b ( .s ` F ) a ) e. ( ( LSpan ` F ) ` ( ran U \ { a } ) ) ) ) )
84 79 83 ax-mp 
 |-  ( ran U e. J <-> ( ran U C_ ( Base ` F ) /\ ( ( LSpan ` F ) ` ran U ) = ( Base ` F ) /\ A. a e. ran U A. b e. ( ( Base ` ( Scalar ` F ) ) \ { ( 0g ` ( Scalar ` F ) ) } ) -. ( b ( .s ` F ) a ) e. ( ( LSpan ` F ) ` ( ran U \ { a } ) ) ) )
85 6 25 78 84 syl3anbrc 
 |-  ( ( R e. Ring /\ I e. V ) -> ran U e. J )