Step | Hyp | Ref
| Expression |
1 | | frlmpws.b |
. . 3
โข ๐ต = (Baseโ๐น) |
2 | | frlmval.f |
. . . . 5
โข ๐น = (๐
freeLMod ๐ผ) |
3 | 2 | frlmval 21170 |
. . . 4
โข ((๐
โ Ring โง ๐ผ โ ๐) โ ๐น = (๐
โm (๐ผ ร {(ringLModโ๐
)}))) |
4 | 3 | fveq2d 6847 |
. . 3
โข ((๐
โ Ring โง ๐ผ โ ๐) โ (Baseโ๐น) = (Baseโ(๐
โm (๐ผ ร {(ringLModโ๐
)})))) |
5 | 1, 4 | eqtrid 2785 |
. 2
โข ((๐
โ Ring โง ๐ผ โ ๐) โ ๐ต = (Baseโ(๐
โm (๐ผ ร {(ringLModโ๐
)})))) |
6 | | simpr 486 |
. . . 4
โข ((๐
โ Ring โง ๐ผ โ ๐) โ ๐ผ โ ๐) |
7 | | simpl 484 |
. . . 4
โข ((๐
โ Ring โง ๐ผ โ ๐) โ ๐
โ Ring) |
8 | | rlmlmod 20690 |
. . . . . 6
โข (๐
โ Ring โ
(ringLModโ๐
) โ
LMod) |
9 | 8 | adantr 482 |
. . . . 5
โข ((๐
โ Ring โง ๐ผ โ ๐) โ (ringLModโ๐
) โ LMod) |
10 | | fconst6g 6732 |
. . . . 5
โข
((ringLModโ๐
)
โ LMod โ (๐ผ
ร {(ringLModโ๐
)}):๐ผโถLMod) |
11 | 9, 10 | syl 17 |
. . . 4
โข ((๐
โ Ring โง ๐ผ โ ๐) โ (๐ผ ร {(ringLModโ๐
)}):๐ผโถLMod) |
12 | | fvex 6856 |
. . . . . . . 8
โข
(ringLModโ๐
)
โ V |
13 | 12 | fvconst2 7154 |
. . . . . . 7
โข (๐ โ ๐ผ โ ((๐ผ ร {(ringLModโ๐
)})โ๐) = (ringLModโ๐
)) |
14 | 13 | adantl 483 |
. . . . . 6
โข (((๐
โ Ring โง ๐ผ โ ๐) โง ๐ โ ๐ผ) โ ((๐ผ ร {(ringLModโ๐
)})โ๐) = (ringLModโ๐
)) |
15 | 14 | fveq2d 6847 |
. . . . 5
โข (((๐
โ Ring โง ๐ผ โ ๐) โง ๐ โ ๐ผ) โ (Scalarโ((๐ผ ร {(ringLModโ๐
)})โ๐)) = (Scalarโ(ringLModโ๐
))) |
16 | | rlmsca 20685 |
. . . . . 6
โข (๐
โ Ring โ ๐
=
(Scalarโ(ringLModโ๐
))) |
17 | 16 | ad2antrr 725 |
. . . . 5
โข (((๐
โ Ring โง ๐ผ โ ๐) โง ๐ โ ๐ผ) โ ๐
= (Scalarโ(ringLModโ๐
))) |
18 | 15, 17 | eqtr4d 2776 |
. . . 4
โข (((๐
โ Ring โง ๐ผ โ ๐) โง ๐ โ ๐ผ) โ (Scalarโ((๐ผ ร {(ringLModโ๐
)})โ๐)) = ๐
) |
19 | | eqid 2733 |
. . . 4
โข (๐
Xs(๐ผ ร {(ringLModโ๐
)})) = (๐
Xs(๐ผ ร {(ringLModโ๐
)})) |
20 | | eqid 2733 |
. . . 4
โข
(LSubSpโ(๐
Xs(๐ผ ร {(ringLModโ๐
)}))) = (LSubSpโ(๐
Xs(๐ผ ร {(ringLModโ๐
)}))) |
21 | | eqid 2733 |
. . . 4
โข
(Baseโ(๐
โm (๐ผ
ร {(ringLModโ๐
)}))) = (Baseโ(๐
โm (๐ผ ร {(ringLModโ๐
)}))) |
22 | 6, 7, 11, 18, 19, 20, 21 | dsmmlss 21166 |
. . 3
โข ((๐
โ Ring โง ๐ผ โ ๐) โ (Baseโ(๐
โm (๐ผ ร {(ringLModโ๐
)}))) โ (LSubSpโ(๐
Xs(๐ผ ร {(ringLModโ๐
)})))) |
23 | | eqid 2733 |
. . . . . . . . 9
โข
((ringLModโ๐
)
โs ๐ผ) = ((ringLModโ๐
) โs ๐ผ) |
24 | | eqid 2733 |
. . . . . . . . 9
โข
(Scalarโ(ringLModโ๐
)) = (Scalarโ(ringLModโ๐
)) |
25 | 23, 24 | pwsval 17373 |
. . . . . . . 8
โข
(((ringLModโ๐
)
โ V โง ๐ผ โ
๐) โ
((ringLModโ๐
)
โs ๐ผ) = ((Scalarโ(ringLModโ๐
))Xs(๐ผ ร {(ringLModโ๐
)}))) |
26 | 12, 25 | mpan 689 |
. . . . . . 7
โข (๐ผ โ ๐ โ ((ringLModโ๐
) โs ๐ผ) =
((Scalarโ(ringLModโ๐
))Xs(๐ผ ร {(ringLModโ๐
)}))) |
27 | 26 | adantl 483 |
. . . . . 6
โข ((๐
โ Ring โง ๐ผ โ ๐) โ ((ringLModโ๐
) โs ๐ผ) =
((Scalarโ(ringLModโ๐
))Xs(๐ผ ร {(ringLModโ๐
)}))) |
28 | 16 | eqcomd 2739 |
. . . . . . . 8
โข (๐
โ Ring โ
(Scalarโ(ringLModโ๐
)) = ๐
) |
29 | 28 | adantr 482 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ผ โ ๐) โ (Scalarโ(ringLModโ๐
)) = ๐
) |
30 | 29 | oveq1d 7373 |
. . . . . 6
โข ((๐
โ Ring โง ๐ผ โ ๐) โ
((Scalarโ(ringLModโ๐
))Xs(๐ผ ร {(ringLModโ๐
)})) = (๐
Xs(๐ผ ร {(ringLModโ๐
)}))) |
31 | 27, 30 | eqtr2d 2774 |
. . . . 5
โข ((๐
โ Ring โง ๐ผ โ ๐) โ (๐
Xs(๐ผ ร {(ringLModโ๐
)})) = ((ringLModโ๐
) โs ๐ผ)) |
32 | 31 | fveq2d 6847 |
. . . 4
โข ((๐
โ Ring โง ๐ผ โ ๐) โ (LSubSpโ(๐
Xs(๐ผ ร {(ringLModโ๐
)}))) = (LSubSpโ((ringLModโ๐
) โs
๐ผ))) |
33 | | frlmlss.u |
. . . 4
โข ๐ =
(LSubSpโ((ringLModโ๐
) โs ๐ผ)) |
34 | 32, 33 | eqtr4di 2791 |
. . 3
โข ((๐
โ Ring โง ๐ผ โ ๐) โ (LSubSpโ(๐
Xs(๐ผ ร {(ringLModโ๐
)}))) = ๐) |
35 | 22, 34 | eleqtrd 2836 |
. 2
โข ((๐
โ Ring โง ๐ผ โ ๐) โ (Baseโ(๐
โm (๐ผ ร {(ringLModโ๐
)}))) โ ๐) |
36 | 5, 35 | eqeltrd 2834 |
1
โข ((๐
โ Ring โง ๐ผ โ ๐) โ ๐ต โ ๐) |