Step | Hyp | Ref
| Expression |
1 | | frlmlbs.u |
. . . 4
⊢ 𝑈 = (𝑅 unitVec 𝐼) |
2 | | frlmlbs.f |
. . . 4
⊢ 𝐹 = (𝑅 freeLMod 𝐼) |
3 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐹) =
(Base‘𝐹) |
4 | 1, 2, 3 | uvcff 19949 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑈:𝐼⟶(Base‘𝐹)) |
5 | | frn 5966 |
. . 3
⊢ (𝑈:𝐼⟶(Base‘𝐹) → ran 𝑈 ⊆ (Base‘𝐹)) |
6 | 4, 5 | syl 17 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ran 𝑈 ⊆ (Base‘𝐹)) |
7 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
8 | 2, 7, 3 | frlmbasf 19923 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑎 ∈ (Base‘𝐹)) → 𝑎:𝐼⟶(Base‘𝑅)) |
9 | 8 | adantll 746 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ 𝑎 ∈ (Base‘𝐹)) → 𝑎:𝐼⟶(Base‘𝑅)) |
10 | | suppssdm 7195 |
. . . . . . 7
⊢ (𝑎 supp (0g‘𝑅)) ⊆ dom 𝑎 |
11 | | fdm 5964 |
. . . . . . 7
⊢ (𝑎:𝐼⟶(Base‘𝑅) → dom 𝑎 = 𝐼) |
12 | 10, 11 | syl5sseq 3616 |
. . . . . 6
⊢ (𝑎:𝐼⟶(Base‘𝑅) → (𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
13 | 9, 12 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ 𝑎 ∈ (Base‘𝐹)) → (𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
14 | 13 | ralrimiva 2949 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ∀𝑎 ∈ (Base‘𝐹)(𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
15 | | rabid2 3096 |
. . . 4
⊢
((Base‘𝐹) =
{𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼} ↔ ∀𝑎 ∈ (Base‘𝐹)(𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
16 | 14, 15 | sylibr 223 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (Base‘𝐹) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼}) |
17 | | ssid 3587 |
. . . 4
⊢ 𝐼 ⊆ 𝐼 |
18 | | eqid 2610 |
. . . . 5
⊢
(LSpan‘𝐹) =
(LSpan‘𝐹) |
19 | | eqid 2610 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
20 | | eqid 2610 |
. . . . 5
⊢ {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼} = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼} |
21 | 2, 1, 18, 3, 19, 20 | frlmsslsp 19954 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐼) → ((LSpan‘𝐹)‘(𝑈 “ 𝐼)) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼}) |
22 | 17, 21 | mp3an3 1405 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((LSpan‘𝐹)‘(𝑈 “ 𝐼)) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼}) |
23 | | ffn 5958 |
. . . . 5
⊢ (𝑈:𝐼⟶(Base‘𝐹) → 𝑈 Fn 𝐼) |
24 | | fnima 5923 |
. . . . 5
⊢ (𝑈 Fn 𝐼 → (𝑈 “ 𝐼) = ran 𝑈) |
25 | 4, 23, 24 | 3syl 18 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝑈 “ 𝐼) = ran 𝑈) |
26 | 25 | fveq2d 6107 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((LSpan‘𝐹)‘(𝑈 “ 𝐼)) = ((LSpan‘𝐹)‘ran 𝑈)) |
27 | 16, 22, 26 | 3eqtr2rd 2651 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹)) |
28 | | eqid 2610 |
. . . . . 6
⊢ (
·𝑠 ‘𝐹) = ( ·𝑠
‘𝐹) |
29 | | eqid 2610 |
. . . . . 6
⊢ {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})} = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})} |
30 | | simpll 786 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑅 ∈ Ring) |
31 | | simplr 788 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝐼 ∈ 𝑉) |
32 | | difssd 3700 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝐼 ∖ {𝑐}) ⊆ 𝐼) |
33 | | vsnid 4156 |
. . . . . . 7
⊢ 𝑐 ∈ {𝑐} |
34 | | snssi 4280 |
. . . . . . . . 9
⊢ (𝑐 ∈ 𝐼 → {𝑐} ⊆ 𝐼) |
35 | 34 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → {𝑐} ⊆ 𝐼) |
36 | | dfss4 3820 |
. . . . . . . 8
⊢ ({𝑐} ⊆ 𝐼 ↔ (𝐼 ∖ (𝐼 ∖ {𝑐})) = {𝑐}) |
37 | 35, 36 | sylib 207 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝐼 ∖ (𝐼 ∖ {𝑐})) = {𝑐}) |
38 | 33, 37 | syl5eleqr 2695 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑐 ∈ (𝐼 ∖ (𝐼 ∖ {𝑐}))) |
39 | 2 | frlmsca 19916 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑅 = (Scalar‘𝐹)) |
40 | 39 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (Base‘𝑅) = (Base‘(Scalar‘𝐹))) |
41 | 39 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (0g‘𝑅) =
(0g‘(Scalar‘𝐹))) |
42 | 41 | sneqd 4137 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → {(0g‘𝑅)} =
{(0g‘(Scalar‘𝐹))}) |
43 | 40, 42 | difeq12d 3691 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((Base‘𝑅) ∖ {(0g‘𝑅)}) =
((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))})) |
44 | 43 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝑏 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)}) ↔ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) |
45 | 44 | biimpar 501 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))})) → 𝑏 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) |
46 | 45 | adantrl 748 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑏 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) |
47 | 2, 1, 3, 7, 28, 19, 29, 30, 31, 32, 38, 46 | frlmssuvc2 19953 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
48 | 19, 7 | ringelnzr 19087 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ ((Base‘𝑅) ∖
{(0g‘𝑅)}))
→ 𝑅 ∈
NzRing) |
49 | 30, 46, 48 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑅 ∈ NzRing) |
50 | 1, 2, 3 | uvcf1 19950 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑉) → 𝑈:𝐼–1-1→(Base‘𝐹)) |
51 | 49, 31, 50 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑈:𝐼–1-1→(Base‘𝐹)) |
52 | | df-f1 5809 |
. . . . . . . . . 10
⊢ (𝑈:𝐼–1-1→(Base‘𝐹) ↔ (𝑈:𝐼⟶(Base‘𝐹) ∧ Fun ◡𝑈)) |
53 | 52 | simprbi 479 |
. . . . . . . . 9
⊢ (𝑈:𝐼–1-1→(Base‘𝐹) → Fun ◡𝑈) |
54 | | imadif 5887 |
. . . . . . . . 9
⊢ (Fun
◡𝑈 → (𝑈 “ (𝐼 ∖ {𝑐})) = ((𝑈 “ 𝐼) ∖ (𝑈 “ {𝑐}))) |
55 | 51, 53, 54 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝑈 “ (𝐼 ∖ {𝑐})) = ((𝑈 “ 𝐼) ∖ (𝑈 “ {𝑐}))) |
56 | | f1fn 6015 |
. . . . . . . . . 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 790 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑐 ∈ 𝐼) |
60 | | fnsnfv 6168 |
. . . . . . . . . . 11
⊢ ((𝑈 Fn 𝐼 ∧ 𝑐 ∈ 𝐼) → {(𝑈‘𝑐)} = (𝑈 “ {𝑐})) |
61 | 58, 59, 60 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → {(𝑈‘𝑐)} = (𝑈 “ {𝑐})) |
62 | 61 | eqcomd 2616 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝑈 “ {𝑐}) = {(𝑈‘𝑐)}) |
63 | 57, 62 | difeq12d 3691 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((𝑈 “ 𝐼) ∖ (𝑈 “ {𝑐})) = (ran 𝑈 ∖ {(𝑈‘𝑐)})) |
64 | 55, 63 | eqtr2d 2645 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (ran 𝑈 ∖ {(𝑈‘𝑐)}) = (𝑈 “ (𝐼 ∖ {𝑐}))) |
65 | 64 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})) = ((LSpan‘𝐹)‘(𝑈 “ (𝐼 ∖ {𝑐})))) |
66 | 2, 1, 18, 3, 19, 29 | frlmsslsp 19954 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ (𝐼 ∖ {𝑐}) ⊆ 𝐼) → ((LSpan‘𝐹)‘(𝑈 “ (𝐼 ∖ {𝑐}))) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
67 | 30, 31, 32, 66 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((LSpan‘𝐹)‘(𝑈 “ (𝐼 ∖ {𝑐}))) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
68 | 65, 67 | eqtrd 2644 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
69 | 47, 68 | neleqtrrd 2710 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)}))) |
70 | 69 | ralrimivva 2954 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ∀𝑐 ∈ 𝐼 ∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)}))) |
71 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑎 = (𝑈‘𝑐) → (𝑏( ·𝑠
‘𝐹)𝑎) = (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐))) |
72 | | sneq 4135 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑈‘𝑐) → {𝑎} = {(𝑈‘𝑐)}) |
73 | 72 | difeq2d 3690 |
. . . . . . . . 9
⊢ (𝑎 = (𝑈‘𝑐) → (ran 𝑈 ∖ {𝑎}) = (ran 𝑈 ∖ {(𝑈‘𝑐)})) |
74 | 73 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑎 = (𝑈‘𝑐) → ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) = ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)}))) |
75 | 71, 74 | eleq12d 2682 |
. . . . . . 7
⊢ (𝑎 = (𝑈‘𝑐) → ((𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
76 | 75 | notbid 307 |
. . . . . 6
⊢ (𝑎 = (𝑈‘𝑐) → (¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
77 | 76 | ralbidv 2969 |
. . . . 5
⊢ (𝑎 = (𝑈‘𝑐) → (∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
78 | 77 | ralrn 6270 |
. . . 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 246 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎}))) |
81 | | ovex 6577 |
. . . 4
⊢ (𝑅 freeLMod 𝐼) ∈ V |
82 | 2, 81 | eqeltri 2684 |
. . 3
⊢ 𝐹 ∈ V |
83 | | eqid 2610 |
. . . 4
⊢
(Scalar‘𝐹) =
(Scalar‘𝐹) |
84 | | eqid 2610 |
. . . 4
⊢
(Base‘(Scalar‘𝐹)) = (Base‘(Scalar‘𝐹)) |
85 | | frlmlbs.j |
. . . 4
⊢ 𝐽 = (LBasis‘𝐹) |
86 | | eqid 2610 |
. . . 4
⊢
(0g‘(Scalar‘𝐹)) =
(0g‘(Scalar‘𝐹)) |
87 | 3, 83, 28, 84, 85, 18, 86 | islbs 18897 |
. . 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 1239 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ran 𝑈 ∈ 𝐽) |