Step | Hyp | Ref
| Expression |
1 | | frlmlbs.u |
. . . 4
⊢ 𝑈 = (𝑅 unitVec 𝐼) |
2 | | frlmlbs.f |
. . . 4
⊢ 𝐹 = (𝑅 freeLMod 𝐼) |
3 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐹) =
(Base‘𝐹) |
4 | 1, 2, 3 | uvcff 20753 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑈:𝐼⟶(Base‘𝐹)) |
5 | 4 | frnd 6553 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ran 𝑈 ⊆ (Base‘𝐹)) |
6 | | suppssdm 7919 |
. . . . . 6
⊢ (𝑎 supp (0g‘𝑅)) ⊆ dom 𝑎 |
7 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
8 | 2, 7, 3 | frlmbasf 20722 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑎 ∈ (Base‘𝐹)) → 𝑎:𝐼⟶(Base‘𝑅)) |
9 | 8 | adantll 714 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ 𝑎 ∈ (Base‘𝐹)) → 𝑎:𝐼⟶(Base‘𝑅)) |
10 | 6, 9 | fssdm 6565 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ 𝑎 ∈ (Base‘𝐹)) → (𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
11 | 10 | ralrimiva 3105 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ∀𝑎 ∈ (Base‘𝐹)(𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
12 | | rabid2 3293 |
. . . 4
⊢
((Base‘𝐹) =
{𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼} ↔ ∀𝑎 ∈ (Base‘𝐹)(𝑎 supp (0g‘𝑅)) ⊆ 𝐼) |
13 | 11, 12 | sylibr 237 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (Base‘𝐹) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼}) |
14 | | ssid 3923 |
. . . 4
⊢ 𝐼 ⊆ 𝐼 |
15 | | eqid 2737 |
. . . . 5
⊢
(LSpan‘𝐹) =
(LSpan‘𝐹) |
16 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
17 | | eqid 2737 |
. . . . 5
⊢ {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼} = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼} |
18 | 2, 1, 15, 3, 16, 17 | frlmsslsp 20758 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐼) → ((LSpan‘𝐹)‘(𝑈 “ 𝐼)) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼}) |
19 | 14, 18 | mp3an3 1452 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((LSpan‘𝐹)‘(𝑈 “ 𝐼)) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ 𝐼}) |
20 | | ffn 6545 |
. . . . 5
⊢ (𝑈:𝐼⟶(Base‘𝐹) → 𝑈 Fn 𝐼) |
21 | | fnima 6508 |
. . . . 5
⊢ (𝑈 Fn 𝐼 → (𝑈 “ 𝐼) = ran 𝑈) |
22 | 4, 20, 21 | 3syl 18 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝑈 “ 𝐼) = ran 𝑈) |
23 | 22 | fveq2d 6721 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((LSpan‘𝐹)‘(𝑈 “ 𝐼)) = ((LSpan‘𝐹)‘ran 𝑈)) |
24 | 13, 19, 23 | 3eqtr2rd 2784 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹)) |
25 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝐹) = ( ·𝑠
‘𝐹) |
26 | | eqid 2737 |
. . . . . 6
⊢ {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})} = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})} |
27 | | simpll 767 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑅 ∈ Ring) |
28 | | simplr 769 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝐼 ∈ 𝑉) |
29 | | difssd 4047 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝐼 ∖ {𝑐}) ⊆ 𝐼) |
30 | | vsnid 4578 |
. . . . . . 7
⊢ 𝑐 ∈ {𝑐} |
31 | | snssi 4721 |
. . . . . . . . 9
⊢ (𝑐 ∈ 𝐼 → {𝑐} ⊆ 𝐼) |
32 | 31 | ad2antrl 728 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → {𝑐} ⊆ 𝐼) |
33 | | dfss4 4173 |
. . . . . . . 8
⊢ ({𝑐} ⊆ 𝐼 ↔ (𝐼 ∖ (𝐼 ∖ {𝑐})) = {𝑐}) |
34 | 32, 33 | sylib 221 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝐼 ∖ (𝐼 ∖ {𝑐})) = {𝑐}) |
35 | 30, 34 | eleqtrrid 2845 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑐 ∈ (𝐼 ∖ (𝐼 ∖ {𝑐}))) |
36 | 2 | frlmsca 20715 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → 𝑅 = (Scalar‘𝐹)) |
37 | 36 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (Base‘𝑅) = (Base‘(Scalar‘𝐹))) |
38 | 36 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (0g‘𝑅) =
(0g‘(Scalar‘𝐹))) |
39 | 38 | sneqd 4553 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → {(0g‘𝑅)} =
{(0g‘(Scalar‘𝐹))}) |
40 | 37, 39 | difeq12d 4038 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ((Base‘𝑅) ∖ {(0g‘𝑅)}) =
((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))})) |
41 | 40 | eleq2d 2823 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (𝑏 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)}) ↔ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) |
42 | 41 | biimpar 481 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))})) → 𝑏 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) |
43 | 42 | adantrl 716 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑏 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) |
44 | 2, 1, 3, 7, 25, 16, 26, 27, 28, 29, 35, 43 | frlmssuvc2 20757 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
45 | 16, 7 | ringelnzr 20304 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑏 ∈ ((Base‘𝑅) ∖
{(0g‘𝑅)}))
→ 𝑅 ∈
NzRing) |
46 | 27, 43, 45 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑅 ∈ NzRing) |
47 | 1, 2, 3 | uvcf1 20754 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑉) → 𝑈:𝐼–1-1→(Base‘𝐹)) |
48 | 46, 28, 47 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑈:𝐼–1-1→(Base‘𝐹)) |
49 | | df-f1 6385 |
. . . . . . . . . 10
⊢ (𝑈:𝐼–1-1→(Base‘𝐹) ↔ (𝑈:𝐼⟶(Base‘𝐹) ∧ Fun ◡𝑈)) |
50 | 49 | simprbi 500 |
. . . . . . . . 9
⊢ (𝑈:𝐼–1-1→(Base‘𝐹) → Fun ◡𝑈) |
51 | | imadif 6464 |
. . . . . . . . 9
⊢ (Fun
◡𝑈 → (𝑈 “ (𝐼 ∖ {𝑐})) = ((𝑈 “ 𝐼) ∖ (𝑈 “ {𝑐}))) |
52 | 48, 50, 51 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝑈 “ (𝐼 ∖ {𝑐})) = ((𝑈 “ 𝐼) ∖ (𝑈 “ {𝑐}))) |
53 | | f1fn 6616 |
. . . . . . . . . 10
⊢ (𝑈:𝐼–1-1→(Base‘𝐹) → 𝑈 Fn 𝐼) |
54 | 48, 53, 21 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝑈 “ 𝐼) = ran 𝑈) |
55 | 48, 53 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑈 Fn 𝐼) |
56 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → 𝑐 ∈ 𝐼) |
57 | | fnsnfv 6790 |
. . . . . . . . . . 11
⊢ ((𝑈 Fn 𝐼 ∧ 𝑐 ∈ 𝐼) → {(𝑈‘𝑐)} = (𝑈 “ {𝑐})) |
58 | 55, 56, 57 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → {(𝑈‘𝑐)} = (𝑈 “ {𝑐})) |
59 | 58 | eqcomd 2743 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (𝑈 “ {𝑐}) = {(𝑈‘𝑐)}) |
60 | 54, 59 | difeq12d 4038 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((𝑈 “ 𝐼) ∖ (𝑈 “ {𝑐})) = (ran 𝑈 ∖ {(𝑈‘𝑐)})) |
61 | 52, 60 | eqtr2d 2778 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → (ran 𝑈 ∖ {(𝑈‘𝑐)}) = (𝑈 “ (𝐼 ∖ {𝑐}))) |
62 | 61 | fveq2d 6721 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})) = ((LSpan‘𝐹)‘(𝑈 “ (𝐼 ∖ {𝑐})))) |
63 | 2, 1, 15, 3, 16, 26 | frlmsslsp 20758 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ (𝐼 ∖ {𝑐}) ⊆ 𝐼) → ((LSpan‘𝐹)‘(𝑈 “ (𝐼 ∖ {𝑐}))) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
64 | 27, 28, 29, 63 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((LSpan‘𝐹)‘(𝑈 “ (𝐼 ∖ {𝑐}))) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
65 | 62, 64 | eqtrd 2777 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})) = {𝑎 ∈ (Base‘𝐹) ∣ (𝑎 supp (0g‘𝑅)) ⊆ (𝐼 ∖ {𝑐})}) |
66 | 44, 65 | neleqtrrd 2860 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) ∧ (𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}))) → ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)}))) |
67 | 66 | ralrimivva 3112 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ∀𝑐 ∈ 𝐼 ∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)}))) |
68 | | oveq2 7221 |
. . . . . . . 8
⊢ (𝑎 = (𝑈‘𝑐) → (𝑏( ·𝑠
‘𝐹)𝑎) = (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐))) |
69 | | sneq 4551 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑈‘𝑐) → {𝑎} = {(𝑈‘𝑐)}) |
70 | 69 | difeq2d 4037 |
. . . . . . . . 9
⊢ (𝑎 = (𝑈‘𝑐) → (ran 𝑈 ∖ {𝑎}) = (ran 𝑈 ∖ {(𝑈‘𝑐)})) |
71 | 70 | fveq2d 6721 |
. . . . . . . 8
⊢ (𝑎 = (𝑈‘𝑐) → ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) = ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)}))) |
72 | 68, 71 | eleq12d 2832 |
. . . . . . 7
⊢ (𝑎 = (𝑈‘𝑐) → ((𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
73 | 72 | notbid 321 |
. . . . . 6
⊢ (𝑎 = (𝑈‘𝑐) → (¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
74 | 73 | ralbidv 3118 |
. . . . 5
⊢ (𝑎 = (𝑈‘𝑐) → (∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ ∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
75 | 74 | ralrn 6907 |
. . . 4
⊢ (𝑈 Fn 𝐼 → (∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ ∀𝑐 ∈ 𝐼 ∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
76 | 4, 20, 75 | 3syl 18 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → (∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})) ↔ ∀𝑐 ∈ 𝐼 ∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)(𝑈‘𝑐)) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {(𝑈‘𝑐)})))) |
77 | 67, 76 | mpbird 260 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎}))) |
78 | 2 | ovexi 7247 |
. . 3
⊢ 𝐹 ∈ V |
79 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝐹) =
(Scalar‘𝐹) |
80 | | eqid 2737 |
. . . 4
⊢
(Base‘(Scalar‘𝐹)) = (Base‘(Scalar‘𝐹)) |
81 | | frlmlbs.j |
. . . 4
⊢ 𝐽 = (LBasis‘𝐹) |
82 | | eqid 2737 |
. . . 4
⊢
(0g‘(Scalar‘𝐹)) =
(0g‘(Scalar‘𝐹)) |
83 | 3, 79, 25, 80, 81, 15, 82 | islbs 20113 |
. . 3
⊢ (𝐹 ∈ V → (ran 𝑈 ∈ 𝐽 ↔ (ran 𝑈 ⊆ (Base‘𝐹) ∧ ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹) ∧ ∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎}))))) |
84 | 78, 83 | ax-mp 5 |
. 2
⊢ (ran
𝑈 ∈ 𝐽 ↔ (ran 𝑈 ⊆ (Base‘𝐹) ∧ ((LSpan‘𝐹)‘ran 𝑈) = (Base‘𝐹) ∧ ∀𝑎 ∈ ran 𝑈∀𝑏 ∈ ((Base‘(Scalar‘𝐹)) ∖
{(0g‘(Scalar‘𝐹))}) ¬ (𝑏( ·𝑠
‘𝐹)𝑎) ∈ ((LSpan‘𝐹)‘(ran 𝑈 ∖ {𝑎})))) |
85 | 5, 24, 77, 84 | syl3anbrc 1345 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉) → ran 𝑈 ∈ 𝐽) |