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