Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉} = {〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} |
2 | 1 | grp1 17345 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → {〈(Base‘ndx), {𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} ∈ Grp) |
3 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) ∈ V |
4 | | lmod1.m |
. . . . . . . . 9
⊢ 𝑀 = ({〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) |
5 | | snex 4835 |
. . . . . . . . . . . . 13
⊢ {𝐼} ∈ V |
6 | 1 | grpbase 15816 |
. . . . . . . . . . . . 13
⊢ ({𝐼} ∈ V → {𝐼} =
(Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉})) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ {𝐼} =
(Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) |
8 | 7 | opeq2i 4344 |
. . . . . . . . . . 11
⊢
〈(Base‘ndx), {𝐼}〉 = 〈(Base‘ndx),
(Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉 |
9 | | tpeq1 4221 |
. . . . . . . . . . 11
⊢
(〈(Base‘ndx), {𝐼}〉 = 〈(Base‘ndx),
(Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉 →
{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} =
{〈(Base‘ndx), (Base‘{〈(Base‘ndx), {𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉}) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . 10
⊢
{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} =
{〈(Base‘ndx), (Base‘{〈(Base‘ndx), {𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} |
11 | 10 | uneq1i 3725 |
. . . . . . . . 9
⊢
({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) = ({〈(Base‘ndx),
(Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) |
12 | 4, 11 | eqtri 2632 |
. . . . . . . 8
⊢ 𝑀 = ({〈(Base‘ndx),
(Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) |
13 | 12 | lmodbase 15841 |
. . . . . . 7
⊢
((Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) ∈ V →
(Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) = (Base‘𝑀)) |
14 | 3, 13 | ax-mp 5 |
. . . . . 6
⊢
(Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) = (Base‘𝑀) |
15 | 14 | eqcomi 2619 |
. . . . 5
⊢
(Base‘𝑀) =
(Base‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) |
16 | | fvex 6113 |
. . . . . . 7
⊢
(+g‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) ∈ V |
17 | | snex 4835 |
. . . . . . . . . . . . 13
⊢
{〈〈𝐼,
𝐼〉, 𝐼〉} ∈ V |
18 | 1 | grpplusg 15817 |
. . . . . . . . . . . . 13
⊢
({〈〈𝐼,
𝐼〉, 𝐼〉} ∈ V → {〈〈𝐼, 𝐼〉, 𝐼〉} =
(+g‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉})) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
{〈〈𝐼,
𝐼〉, 𝐼〉} =
(+g‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) |
20 | 19 | opeq2i 4344 |
. . . . . . . . . . 11
⊢
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉 =
〈(+g‘ndx), (+g‘{〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉 |
21 | | tpeq2 4222 |
. . . . . . . . . . 11
⊢
(〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉 =
〈(+g‘ndx), (+g‘{〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉 →
{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} =
{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
(+g‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉,
〈(Scalar‘ndx), 𝑅〉}) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . 10
⊢
{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} =
{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
(+g‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉,
〈(Scalar‘ndx), 𝑅〉} |
23 | 22 | uneq1i 3725 |
. . . . . . . . 9
⊢
({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) = ({〈(Base‘ndx), {𝐼}〉,
〈(+g‘ndx), (+g‘{〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉,
〈(Scalar‘ndx), 𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) |
24 | 4, 23 | eqtri 2632 |
. . . . . . . 8
⊢ 𝑀 = ({〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), (+g‘{〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉})〉,
〈(Scalar‘ndx), 𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ {𝐼} ↦ 𝑦)〉}) |
25 | 24 | lmodplusg 15842 |
. . . . . . 7
⊢
((+g‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) ∈ V →
(+g‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) = (+g‘𝑀)) |
26 | 16, 25 | ax-mp 5 |
. . . . . 6
⊢
(+g‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) = (+g‘𝑀) |
27 | 26 | eqcomi 2619 |
. . . . 5
⊢
(+g‘𝑀) =
(+g‘{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉}) |
28 | 15, 27 | grpprop 17261 |
. . . 4
⊢ (𝑀 ∈ Grp ↔
{〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉} ∈ Grp) |
29 | 2, 28 | sylibr 223 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Grp) |
30 | 29 | adantr 480 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑀 ∈ Grp) |
31 | 4 | lmodsca 15843 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑀)) |
32 | 31 | eqcomd 2616 |
. . . 4
⊢ (𝑅 ∈ Ring →
(Scalar‘𝑀) = 𝑅) |
33 | 32 | adantl 481 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → (Scalar‘𝑀) = 𝑅) |
34 | | simpr 476 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) |
35 | 33, 34 | eqeltrd 2688 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → (Scalar‘𝑀) ∈ Ring) |
36 | 33 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) →
(Base‘(Scalar‘𝑀)) = (Base‘𝑅)) |
37 | 36 | eleq2d 2673 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → (𝑞 ∈ (Base‘(Scalar‘𝑀)) ↔ 𝑞 ∈ (Base‘𝑅))) |
38 | 36 | eleq2d 2673 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → (𝑟 ∈ (Base‘(Scalar‘𝑀)) ↔ 𝑟 ∈ (Base‘𝑅))) |
39 | 37, 38 | anbi12d 743 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ((𝑞 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑀))) ↔ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅)))) |
40 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → 𝐼 ∈ 𝑉) |
41 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → 𝑅 ∈ Ring) |
42 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → 𝑟 ∈ (Base‘𝑅)) |
43 | 40, 41, 42 | 3jca 1235 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → (𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅))) |
44 | 4 | lmod1lem1 42070 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼}) |
45 | 43, 44 | syl 17 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → (𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼}) |
46 | 4 | lmod1lem2 42071 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ (Base‘𝑅)) → (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) |
47 | 43, 46 | syl 17 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) |
48 | 4 | lmod1lem3 42072 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) |
49 | 45, 47, 48 | 3jca 1235 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)))) |
50 | 4 | lmod1lem4 42073 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → ((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼))) |
51 | 4 | lmod1lem5 42074 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) →
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼) |
52 | 51 | adantr 480 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) →
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼) |
53 | 49, 50, 52 | jca32 556 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) ∧ (𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅))) → (((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼))) |
54 | 53 | ex 449 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ((𝑞 ∈ (Base‘𝑅) ∧ 𝑟 ∈ (Base‘𝑅)) → (((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼)))) |
55 | 39, 54 | sylbid 229 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ((𝑞 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑀))) → (((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼)))) |
56 | 55 | ralrimivv 2953 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ∀𝑞 ∈
(Base‘(Scalar‘𝑀))∀𝑟 ∈ (Base‘(Scalar‘𝑀))(((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼))) |
57 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐼 → (𝑤(+g‘𝑀)𝑥) = (𝑤(+g‘𝑀)𝐼)) |
58 | 57 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐼 → (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼))) |
59 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐼 → (𝑟( ·𝑠
‘𝑀)𝑥) = (𝑟( ·𝑠
‘𝑀)𝐼)) |
60 | 59 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐼 → ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) |
61 | 58, 60 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐼 → ((𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) ↔ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)))) |
62 | 61 | 3anbi2d 1396 |
. . . . . . . . 9
⊢ (𝑥 = 𝐼 → (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ↔ ((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))))) |
63 | 62 | anbi1d 737 |
. . . . . . . 8
⊢ (𝑥 = 𝐼 → ((((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)) ↔ (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)))) |
64 | 63 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = 𝐼 → (∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)) ↔ ∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)))) |
65 | 64 | ralsng 4165 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (∀𝑥 ∈ {𝐼}∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)) ↔ ∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)))) |
66 | 65 | adantr 480 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → (∀𝑥 ∈ {𝐼}∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)) ↔ ∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)))) |
67 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐼 → (𝑟( ·𝑠
‘𝑀)𝑤) = (𝑟( ·𝑠
‘𝑀)𝐼)) |
68 | 67 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑤 = 𝐼 → ((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ↔ (𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼})) |
69 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝐼 → (𝑤(+g‘𝑀)𝐼) = (𝐼(+g‘𝑀)𝐼)) |
70 | 69 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐼 → (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼))) |
71 | 67 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐼 → ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) |
72 | 70, 71 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑤 = 𝐼 → ((𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ↔ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)))) |
73 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐼 → ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼)) |
74 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝐼 → (𝑞( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)𝐼)) |
75 | 74, 67 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐼 → ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤)) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) |
76 | 73, 75 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑤 = 𝐼 → (((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤)) ↔ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)))) |
77 | 68, 72, 76 | 3anbi123d 1391 |
. . . . . . . 8
⊢ (𝑤 = 𝐼 → (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ↔ ((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))))) |
78 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐼 → ((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼)) |
79 | 67 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐼 → (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼))) |
80 | 78, 79 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑤 = 𝐼 → (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ↔ ((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)))) |
81 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐼 →
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = ((1r‘(Scalar‘𝑀))(
·𝑠 ‘𝑀)𝐼)) |
82 | | id 22 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐼 → 𝑤 = 𝐼) |
83 | 81, 82 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑤 = 𝐼 →
(((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤 ↔
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼)) |
84 | 80, 83 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑤 = 𝐼 → ((((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤) ↔ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼))) |
85 | 77, 84 | anbi12d 743 |
. . . . . . 7
⊢ (𝑤 = 𝐼 → ((((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)) ↔ (((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼)))) |
86 | 85 | ralsng 4165 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)) ↔ (((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼)))) |
87 | 86 | adantr 480 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → (∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)) ↔ (((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼)))) |
88 | 66, 87 | bitrd 267 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → (∀𝑥 ∈ {𝐼}∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)) ↔ (((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼)))) |
89 | 88 | 2ralbidv 2972 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → (∀𝑞 ∈
(Base‘(Scalar‘𝑀))∀𝑟 ∈ (Base‘(Scalar‘𝑀))∀𝑥 ∈ {𝐼}∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)) ↔ ∀𝑞 ∈ (Base‘(Scalar‘𝑀))∀𝑟 ∈ (Base‘(Scalar‘𝑀))(((𝑟( ·𝑠
‘𝑀)𝐼) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝐼(+g‘𝑀)𝐼)) = ((𝑟( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = ((𝑞( ·𝑠
‘𝑀)𝐼)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝐼))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝐼) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝐼)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝐼) = 𝐼)))) |
90 | 56, 89 | mpbird 246 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ∀𝑞 ∈
(Base‘(Scalar‘𝑀))∀𝑟 ∈ (Base‘(Scalar‘𝑀))∀𝑥 ∈ {𝐼}∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤))) |
91 | 4 | lmodbase 15841 |
. . . 4
⊢ ({𝐼} ∈ V → {𝐼} = (Base‘𝑀)) |
92 | 5, 91 | ax-mp 5 |
. . 3
⊢ {𝐼} = (Base‘𝑀) |
93 | | eqid 2610 |
. . 3
⊢
(+g‘𝑀) = (+g‘𝑀) |
94 | | eqid 2610 |
. . 3
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
95 | | eqid 2610 |
. . 3
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
96 | | eqid 2610 |
. . 3
⊢
(Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀)) |
97 | | eqid 2610 |
. . 3
⊢
(+g‘(Scalar‘𝑀)) =
(+g‘(Scalar‘𝑀)) |
98 | | eqid 2610 |
. . 3
⊢
(.r‘(Scalar‘𝑀)) =
(.r‘(Scalar‘𝑀)) |
99 | | eqid 2610 |
. . 3
⊢
(1r‘(Scalar‘𝑀)) =
(1r‘(Scalar‘𝑀)) |
100 | 92, 93, 94, 95, 96, 97, 98, 99 | islmod 18690 |
. 2
⊢ (𝑀 ∈ LMod ↔ (𝑀 ∈ Grp ∧
(Scalar‘𝑀) ∈
Ring ∧ ∀𝑞 ∈
(Base‘(Scalar‘𝑀))∀𝑟 ∈ (Base‘(Scalar‘𝑀))∀𝑥 ∈ {𝐼}∀𝑤 ∈ {𝐼} (((𝑟( ·𝑠
‘𝑀)𝑤) ∈ {𝐼} ∧ (𝑟( ·𝑠
‘𝑀)(𝑤(+g‘𝑀)𝑥)) = ((𝑟( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = ((𝑞( ·𝑠
‘𝑀)𝑤)(+g‘𝑀)(𝑟( ·𝑠
‘𝑀)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑀))𝑟)( ·𝑠
‘𝑀)𝑤) = (𝑞( ·𝑠
‘𝑀)(𝑟(
·𝑠 ‘𝑀)𝑤)) ∧
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑀)𝑤) = 𝑤)))) |
101 | 30, 35, 90, 100 | syl3anbrc 1239 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑀 ∈ LMod) |