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=RfreeLModI
frlmlbs.u ⊢U=RunitVecI
frlmlbs.j ⊢J=LBasis⁡F
Assertion frlmlbs ⊢R∈Ring∧I∈V→ran⁡U∈J

Proof

Step Hyp Ref Expression
1 frlmlbs.f ⊢F=RfreeLModI
2 frlmlbs.u ⊢U=RunitVecI
3 frlmlbs.j ⊢J=LBasis⁡F
4 eqid ⊢BaseF=BaseF
5 2 1 4 uvcff ⊢R∈Ring∧I∈V→U:I⟶BaseF
6 5 frnd ⊢R∈Ring∧I∈V→ran⁡U⊆BaseF
7 suppssdm ⊢asupp0R⊆dom⁡a
8 eqid ⊢BaseR=BaseR
9 1 8 4 frlmbasf ⊢I∈V∧a∈BaseF→a:I⟶BaseR
10 9 adantll ⊢R∈Ring∧I∈V∧a∈BaseF→a:I⟶BaseR
11 7 10 fssdm ⊢R∈Ring∧I∈V∧a∈BaseF→asupp0R⊆I
12 11 ralrimiva ⊢R∈Ring∧I∈V→∀a∈BaseFasupp0R⊆I
13 rabid2 ⊢BaseF=a∈BaseF|asupp0R⊆I↔∀a∈BaseFasupp0R⊆I
14 12 13 sylibr ⊢R∈Ring∧I∈V→BaseF=a∈BaseF|asupp0R⊆I
15 ssid ⊢I⊆I
16 eqid ⊢LSpan⁡F=LSpan⁡F
17 eqid ⊢0R=0R
18 eqid ⊢a∈BaseF|asupp0R⊆I=a∈BaseF|asupp0R⊆I
19 1 2 16 4 17 18 frlmsslsp ⊢R∈Ring∧I∈V∧I⊆I→LSpan⁡F⁡UI=a∈BaseF|asupp0R⊆I
20 15 19 mp3an3 ⊢R∈Ring∧I∈V→LSpan⁡F⁡UI=a∈BaseF|asupp0R⊆I
21 ffn ⊢U:I⟶BaseF→UFnI
22 fnima ⊢UFnI→UI=ran⁡U
23 5 21 22 3syl ⊢R∈Ring∧I∈V→UI=ran⁡U
24 23 fveq2d ⊢R∈Ring∧I∈V→LSpan⁡F⁡UI=LSpan⁡F⁡ran⁡U
25 14 20 24 3eqtr2rd ⊢R∈Ring∧I∈V→LSpan⁡F⁡ran⁡U=BaseF
26 eqid ⊢⋅F=⋅F
27 eqid ⊢a∈BaseF|asupp0R⊆I∖c=a∈BaseF|asupp0R⊆I∖c
28 simpll ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→R∈Ring
29 simplr ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→I∈V
30 difssd ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→I∖c⊆I
31 vsnid ⊢c∈c
32 snssi ⊢c∈I→c⊆I
33 32 ad2antrl ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→c⊆I
34 dfss4 ⊢c⊆I↔I∖I∖c=c
35 33 34 sylib ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→I∖I∖c=c
36 31 35 eleqtrrid ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→c∈I∖I∖c
37 1 frlmsca ⊢R∈Ring∧I∈V→R=Scalar⁡F
38 37 fveq2d ⊢R∈Ring∧I∈V→BaseR=BaseScalar⁡F
39 37 fveq2d ⊢R∈Ring∧I∈V→0R=0Scalar⁡F
40 39 sneqd ⊢R∈Ring∧I∈V→0R=0Scalar⁡F
41 38 40 difeq12d ⊢R∈Ring∧I∈V→BaseR∖0R=BaseScalar⁡F∖0Scalar⁡F
42 41 eleq2d ⊢R∈Ring∧I∈V→b∈BaseR∖0R↔b∈BaseScalar⁡F∖0Scalar⁡F
43 42 biimpar ⊢R∈Ring∧I∈V∧b∈BaseScalar⁡F∖0Scalar⁡F→b∈BaseR∖0R
44 43 adantrl ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→b∈BaseR∖0R
45 1 2 4 8 26 17 27 28 29 30 36 44 frlmssuvc2 ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→¬b⋅FU⁡c∈a∈BaseF|asupp0R⊆I∖c
46 17 8 ringelnzr ⊢R∈Ring∧b∈BaseR∖0R→R∈NzRing
47 28 44 46 syl2anc ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→R∈NzRing
48 2 1 4 uvcf1 ⊢R∈NzRing∧I∈V→U:I⟶1-1BaseF
49 47 29 48 syl2anc ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→U:I⟶1-1BaseF
50 df-f1 ⊢U:I⟶1-1BaseF↔U:I⟶BaseF∧Fun⁡U-1
51 50 simprbi ⊢U:I⟶1-1BaseF→Fun⁡U-1
52 imadif ⊢Fun⁡U-1→UI∖c=UI∖Uc
53 49 51 52 3syl ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→UI∖c=UI∖Uc
54 f1fn ⊢U:I⟶1-1BaseF→UFnI
55 49 54 22 3syl ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→UI=ran⁡U
56 49 54 syl ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→UFnI
57 simprl ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→c∈I
58 fnsnfv ⊢UFnI∧c∈I→U⁡c=Uc
59 56 57 58 syl2anc ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→U⁡c=Uc
60 59 eqcomd ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→Uc=U⁡c
61 55 60 difeq12d ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→UI∖Uc=ran⁡U∖U⁡c
62 53 61 eqtr2d ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→ran⁡U∖U⁡c=UI∖c
63 62 fveq2d ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→LSpan⁡F⁡ran⁡U∖U⁡c=LSpan⁡F⁡UI∖c
64 1 2 16 4 17 27 frlmsslsp ⊢R∈Ring∧I∈V∧I∖c⊆I→LSpan⁡F⁡UI∖c=a∈BaseF|asupp0R⊆I∖c
65 28 29 30 64 syl3anc ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→LSpan⁡F⁡UI∖c=a∈BaseF|asupp0R⊆I∖c
66 63 65 eqtrd ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→LSpan⁡F⁡ran⁡U∖U⁡c=a∈BaseF|asupp0R⊆I∖c
67 45 66 neleqtrrd ⊢R∈Ring∧I∈V∧c∈I∧b∈BaseScalar⁡F∖0Scalar⁡F→¬b⋅FU⁡c∈LSpan⁡F⁡ran⁡U∖U⁡c
68 67 ralrimivva ⊢R∈Ring∧I∈V→∀c∈I∀b∈BaseScalar⁡F∖0Scalar⁡F¬b⋅FU⁡c∈LSpan⁡F⁡ran⁡U∖U⁡c
69 oveq2 ⊢a=U⁡c→b⋅Fa=b⋅FU⁡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⋅Fa∈LSpan⁡F⁡ran⁡U∖a↔b⋅FU⁡c∈LSpan⁡F⁡ran⁡U∖U⁡c
74 73 notbid ⊢a=U⁡c→¬b⋅Fa∈LSpan⁡F⁡ran⁡U∖a↔¬b⋅FU⁡c∈LSpan⁡F⁡ran⁡U∖U⁡c
75 74 ralbidv ⊢a=U⁡c→∀b∈BaseScalar⁡F∖0Scalar⁡F¬b⋅Fa∈LSpan⁡F⁡ran⁡U∖a↔∀b∈BaseScalar⁡F∖0Scalar⁡F¬b⋅FU⁡c∈LSpan⁡F⁡ran⁡U∖U⁡c
76 75 ralrn ⊢UFnI→∀a∈ran⁡U∀b∈BaseScalar⁡F∖0Scalar⁡F¬b⋅Fa∈LSpan⁡F⁡ran⁡U∖a↔∀c∈I∀b∈BaseScalar⁡F∖0Scalar⁡F¬b⋅FU⁡c∈LSpan⁡F⁡ran⁡U∖U⁡c
77 5 21 76 3syl ⊢R∈Ring∧I∈V→∀a∈ran⁡U∀b∈BaseScalar⁡F∖0Scalar⁡F¬b⋅Fa∈LSpan⁡F⁡ran⁡U∖a↔∀c∈I∀b∈BaseScalar⁡F∖0Scalar⁡F¬b⋅FU⁡c∈LSpan⁡F⁡ran⁡U∖U⁡c
78 68 77 mpbird ⊢R∈Ring∧I∈V→∀a∈ran⁡U∀b∈BaseScalar⁡F∖0Scalar⁡F¬b⋅Fa∈LSpan⁡F⁡ran⁡U∖a
79 1 ovexi ⊢F∈V
80 eqid ⊢Scalar⁡F=Scalar⁡F
81 eqid ⊢BaseScalar⁡F=BaseScalar⁡F
82 eqid ⊢0Scalar⁡F=0Scalar⁡F
83 4 80 26 81 3 16 82 islbs ⊢F∈V→ran⁡U∈J↔ran⁡U⊆BaseF∧LSpan⁡F⁡ran⁡U=BaseF∧∀a∈ran⁡U∀b∈BaseScalar⁡F∖0Scalar⁡F¬b⋅Fa∈LSpan⁡F⁡ran⁡U∖a
84 79 83 ax-mp ⊢ran⁡U∈J↔ran⁡U⊆BaseF∧LSpan⁡F⁡ran⁡U=BaseF∧∀a∈ran⁡U∀b∈BaseScalar⁡F∖0Scalar⁡F¬b⋅Fa∈LSpan⁡F⁡ran⁡U∖a
85 6 25 78 84 syl3anbrc ⊢R∈Ring∧I∈V→ran⁡U∈J