Step | Hyp | Ref
| Expression |
1 | | frlmlbs.u |
. . . 4
⊢ 𝑈 = (𝑅 unitVec 𝐼) |
2 | | frlmlbs.f |
. . . 4
⊢ 𝐹 = (𝑅 freeLMod 𝐼) |
3 | | eqid 2622 |
. . . 4
⊢
(Base‘𝐹) =
(Base‘𝐹) |
4 | 1, 2, 3 | uvcff 20130 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑈:𝐼⟶(Base‘𝐹)) |
5 | | frn 6053 |
. . 3
⊢ (𝑈:𝐼⟶(Base‘𝐹) → ran 𝑈 ⊆ (Base‘𝐹)) |
6 | 4, 5 | syl 17 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ran 𝑈 ⊆ (Base‘𝐹)) |
7 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
8 | 2, 7, 3 | frlmbasf 20104 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑎 ∈ (Base‘𝐹)) → 𝑎:𝐼⟶(Base‘𝑅)) |
9 | 8 | adantll 750 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ 𝑎 ∈ (Base‘𝐹)) → 𝑎:𝐼⟶(Base‘𝑅)) |
10 | | suppssdm 7308 |
. . . . . . 7
⊢ (𝑎 supp (0g‘𝑅)) ⊆ dom 𝑎 |
11 | | fdm 6051 |
. . . . . . 7
⊢ (𝑎:𝐼⟶(Base‘𝑅) → dom 𝑎 = 𝐼) |
12 | 10, 11 | syl5sseq 3653 |
. . . . . 6
⊢ (𝑎:𝐼⟶(Base‘𝑅) → (𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
13 | 9, 12 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ 𝑎 ∈ (Base‘𝐹)) → (𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
14 | 13 | ralrimiva 2966 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ∀𝑎 ∈ (Base‘𝐹)(𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
15 | | rabid2 3118 |
. . . 4
⊢
((Base‘𝐹) =
{𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼} ↔ ∀𝑎 ∈ (Base‘𝐹)(𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
16 | 14, 15 | sylibr 224 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (Base‘𝐹) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼}) |
17 | | ssid 3624 |
. . . 4
⊢ 𝐼 ⊆ 𝐼 |
18 | | eqid 2622 |
. . . . 5
⊢
(LSpan‘𝐹) =
(LSpan‘𝐹) |
19 | | eqid 2622 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
20 | | eqid 2622 |
. . . . 5
⊢ {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼} = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼} |
21 | 2, 1, 18, 3, 19, 20 | frlmsslsp 20135 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐼) → ((LSpan‘𝐹)‘(𝑈 “ 𝐼)) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼}) |
22 | 17, 21 | mp3an3 1413 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((LSpan‘𝐹)‘(𝑈 “ 𝐼)) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼}) |
23 | | ffn 6045 |
. . . . 5
⊢ (𝑈:𝐼⟶(Base‘𝐹) → 𝑈 Fn 𝐼) |
24 | | fnima 6010 |
. . . . 5
⊢ (𝑈 Fn 𝐼 → (𝑈 “ 𝐼) = ran 𝑈) |
25 | 4, 23, 24 | 3syl 18 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝑈 “ 𝐼) = ran 𝑈) |
26 | 25 | fveq2d 6195 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((LSpan‘𝐹)‘(𝑈 “ 𝐼)) = ((LSpan‘𝐹)‘ran 𝑈)) |
27 | 16, 22, 26 | 3eqtr2rd 2663 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹)) |
28 | | eqid 2622 |
. . . . . 6
⊢ (
·𝑠 ‘𝐹) = ( ·𝑠
‘𝐹) |
29 | | eqid 2622 |
. . . . . 6
⊢ {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})} = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})} |
30 | | simpll 790 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑅 ∈ Ring) |
31 | | simplr 792 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝐼 ∈ 𝑉) |
32 | | difssd 3738 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝐼 ∖ {𝑐}) ⊆ 𝐼) |
33 | | vsnid 4209 |
. . . . . . 7
⊢ 𝑐 ∈ {𝑐} |
34 | | snssi 4339 |
. . . . . . . . 9
⊢ (𝑐 ∈ 𝐼 → {𝑐} ⊆ 𝐼) |
35 | 34 | ad2antrl 764 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → {𝑐} ⊆ 𝐼) |
36 | | dfss4 3858 |
. . . . . . . 8
⊢ ({𝑐} ⊆ 𝐼 ↔ (𝐼 ∖ (𝐼 ∖ {𝑐})) = {𝑐}) |
37 | 35, 36 | sylib 208 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝐼 ∖ (𝐼 ∖ {𝑐})) = {𝑐}) |
38 | 33, 37 | syl5eleqr 2708 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑐 ∈ (𝐼 ∖ (𝐼 ∖ {𝑐}))) |
39 | 2 | frlmsca 20097 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑅 = (Scalar‘𝐹)) |
40 | 39 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (Base‘𝑅) = (Base‘(Scalar‘𝐹))) |
41 | 39 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (0g‘𝑅) =
(0g‘(Scalar‘𝐹))) |
42 | 41 | sneqd 4189 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → {(0g‘𝑅)} =
{(0g‘(Scalar‘𝐹))}) |
43 | 40, 42 | difeq12d 3729 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((Base‘𝑅) ∖ {(0g‘𝑅)}) =
((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))})) |
44 | 43 | eleq2d 2687 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝑏 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)}) ↔ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) |
45 | 44 | biimpar 502 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))})) → 𝑏 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) |
46 | 45 | adantrl 752 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑏 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) |
47 | 2, 1, 3, 7, 28, 19, 29, 30, 31, 32, 38, 46 | frlmssuvc2 20134 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
48 | 19, 7 | ringelnzr 19266 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ ((Base‘𝑅) ∖
{(0g‘𝑅)}))
→ 𝑅 ∈
NzRing) |
49 | 30, 46, 48 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑅 ∈ NzRing) |
50 | 1, 2, 3 | uvcf1 20131 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑉) → 𝑈:𝐼–1-1→(Base‘𝐹)) |
51 | 49, 31, 50 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑈:𝐼–1-1→(Base‘𝐹)) |
52 | | df-f1 5893 |
. . . . . . . . . 10
⊢ (𝑈:𝐼–1-1→(Base‘𝐹) ↔ (𝑈:𝐼⟶(Base‘𝐹) ∧ Fun ◡𝑈)) |
53 | 52 | simprbi 480 |
. . . . . . . . 9
⊢ (𝑈:𝐼–1-1→(Base‘𝐹) → Fun ◡𝑈) |
54 | | imadif 5973 |
. . . . . . . . 9
⊢ (Fun
◡𝑈 → (𝑈 “ (𝐼 ∖ {𝑐})) = ((𝑈 “ 𝐼) ∖ (𝑈 “ {𝑐}))) |
55 | 51, 53, 54 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝑈 “ (𝐼 ∖ {𝑐})) = ((𝑈 “ 𝐼) ∖ (𝑈 “ {𝑐}))) |
56 | | f1fn 6102 |
. . . . . . . . . 10
⊢ (𝑈:𝐼–1-1→(Base‘𝐹) → 𝑈 Fn 𝐼) |
57 | 51, 56, 24 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝑈 “ 𝐼) = ran 𝑈) |
58 | 51, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑈 Fn 𝐼) |
59 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑐 ∈ 𝐼) |
60 | | fnsnfv 6258 |
. . . . . . . . . . 11
⊢ ((𝑈 Fn 𝐼 ∧ 𝑐 ∈ 𝐼) → {(𝑈‘𝑐)} = (𝑈 “ {𝑐})) |
61 | 58, 59, 60 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → {(𝑈‘𝑐)} = (𝑈 “ {𝑐})) |
62 | 61 | eqcomd 2628 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝑈 “ {𝑐}) = {(𝑈‘𝑐)}) |
63 | 57, 62 | difeq12d 3729 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((𝑈 “ 𝐼) ∖ (𝑈 “ {𝑐})) = (ran 𝑈 ∖ {(𝑈‘𝑐)})) |
64 | 55, 63 | eqtr2d 2657 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (ran 𝑈 ∖ {(𝑈‘𝑐)}) = (𝑈 “ (𝐼 ∖ {𝑐}))) |
65 | 64 | fveq2d 6195 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})) = ((LSpan‘𝐹)‘(𝑈 “ (𝐼 ∖ {𝑐})))) |
66 | 2, 1, 18, 3, 19, 29 | frlmsslsp 20135 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ (𝐼 ∖ {𝑐}) ⊆ 𝐼) → ((LSpan‘𝐹)‘(𝑈 “ (𝐼 ∖ {𝑐}))) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
67 | 30, 31, 32, 66 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((LSpan‘𝐹)‘(𝑈 “ (𝐼 ∖ {𝑐}))) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
68 | 65, 67 | eqtrd 2656 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
69 | 47, 68 | neleqtrrd 2723 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)}))) |
70 | 69 | ralrimivva 2971 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ∀𝑐 ∈ 𝐼 ∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)}))) |
71 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑎 = (𝑈‘𝑐) → (𝑏( ·𝑠
‘𝐹)𝑎) = (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐))) |
72 | | sneq 4187 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑈‘𝑐) → {𝑎} = {(𝑈‘𝑐)}) |
73 | 72 | difeq2d 3728 |
. . . . . . . . 9
⊢ (𝑎 = (𝑈‘𝑐) → (ran 𝑈 ∖ {𝑎}) = (ran 𝑈 ∖ {(𝑈‘𝑐)})) |
74 | 73 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑎 = (𝑈‘𝑐) → ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) = ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)}))) |
75 | 71, 74 | eleq12d 2695 |
. . . . . . 7
⊢ (𝑎 = (𝑈‘𝑐) → ((𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
76 | 75 | notbid 308 |
. . . . . 6
⊢ (𝑎 = (𝑈‘𝑐) → (¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
77 | 76 | ralbidv 2986 |
. . . . 5
⊢ (𝑎 = (𝑈‘𝑐) → (∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
78 | 77 | ralrn 6362 |
. . . 4
⊢ (𝑈 Fn 𝐼 → (∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ ∀𝑐 ∈ 𝐼 ∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
79 | 4, 23, 78 | 3syl 18 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ ∀𝑐 ∈ 𝐼 ∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
80 | 70, 79 | mpbird 247 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎}))) |
81 | | ovex 6678 |
. . . 4
⊢ (𝑅 freeLMod 𝐼) ∈ V |
82 | 2, 81 | eqeltri 2697 |
. . 3
⊢ 𝐹 ∈ V |
83 | | eqid 2622 |
. . . 4
⊢
(Scalar‘𝐹) =
(Scalar‘𝐹) |
84 | | eqid 2622 |
. . . 4
⊢
(Base‘(Scalar‘𝐹)) = (Base‘(Scalar‘𝐹)) |
85 | | frlmlbs.j |
. . . 4
⊢ 𝐽 = (LBasis‘𝐹) |
86 | | eqid 2622 |
. . . 4
⊢
(0g‘(Scalar‘𝐹)) =
(0g‘(Scalar‘𝐹)) |
87 | 3, 83, 28, 84, 85, 18, 86 | islbs 19076 |
. . 3
⊢ (𝐹 ∈ V → (ran 𝑈 ∈ 𝐽 ↔ (ran 𝑈 ⊆ (Base‘𝐹) ∧ ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹) ∧ ∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎}))))) |
88 | 82, 87 | ax-mp 5 |
. 2
⊢ (ran
𝑈 ∈ 𝐽 ↔ (ran 𝑈 ⊆ (Base‘𝐹) ∧ ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹) ∧ ∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})))) |
89 | 6, 27, 80, 88 | syl3anbrc 1246 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ran 𝑈 ∈ 𝐽) |