Step | Hyp | Ref
| Expression |
1 | | lmod1zr.m |
. . 3
⊢ 𝑀 = ({〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), {〈〈𝑍, 𝐼〉, 𝐼〉}〉}) |
2 | | elsni 4338 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ {〈𝑍, 𝐼〉} → 𝑝 = 〈𝑍, 𝐼〉) |
3 | | fveq2 6352 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑍, 𝐼〉 → (2nd ‘𝑝) = (2nd
‘〈𝑍, 𝐼〉)) |
4 | 3 | adantl 473 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑝 = 〈𝑍, 𝐼〉) → (2nd ‘𝑝) = (2nd
‘〈𝑍, 𝐼〉)) |
5 | | op2ndg 7346 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍 ∈ 𝑊 ∧ 𝐼 ∈ 𝑉) → (2nd ‘〈𝑍, 𝐼〉) = 𝐼) |
6 | 5 | ancoms 468 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (2nd ‘〈𝑍, 𝐼〉) = 𝐼) |
7 | | snidg 4351 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ {𝐼}) |
8 | 7 | adantr 472 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝐼 ∈ {𝐼}) |
9 | 6, 8 | eqeltrd 2839 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (2nd ‘〈𝑍, 𝐼〉) ∈ {𝐼}) |
10 | 9 | adantr 472 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑝 = 〈𝑍, 𝐼〉) → (2nd
‘〈𝑍, 𝐼〉) ∈ {𝐼}) |
11 | 4, 10 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑝 = 〈𝑍, 𝐼〉) → (2nd ‘𝑝) ∈ {𝐼}) |
12 | 2, 11 | sylan2 492 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑝 ∈ {〈𝑍, 𝐼〉}) → (2nd ‘𝑝) ∈ {𝐼}) |
13 | | eqid 2760 |
. . . . . . . . . 10
⊢ (𝑝 ∈ {〈𝑍, 𝐼〉} ↦ (2nd ‘𝑝)) = (𝑝 ∈ {〈𝑍, 𝐼〉} ↦ (2nd ‘𝑝)) |
14 | 12, 13 | fmptd 6548 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑝 ∈ {〈𝑍, 𝐼〉} ↦ (2nd ‘𝑝)):{〈𝑍, 𝐼〉}⟶{𝐼}) |
15 | | opex 5081 |
. . . . . . . . . 10
⊢
〈𝑍, 𝐼〉 ∈ V |
16 | | simpl 474 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝐼 ∈ 𝑉) |
17 | | fsng 6567 |
. . . . . . . . . 10
⊢
((〈𝑍, 𝐼〉 ∈ V ∧ 𝐼 ∈ 𝑉) → ((𝑝 ∈ {〈𝑍, 𝐼〉} ↦ (2nd ‘𝑝)):{〈𝑍, 𝐼〉}⟶{𝐼} ↔ (𝑝 ∈ {〈𝑍, 𝐼〉} ↦ (2nd ‘𝑝)) = {〈〈𝑍, 𝐼〉, 𝐼〉})) |
18 | 15, 16, 17 | sylancr 698 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝑝 ∈ {〈𝑍, 𝐼〉} ↦ (2nd ‘𝑝)):{〈𝑍, 𝐼〉}⟶{𝐼} ↔ (𝑝 ∈ {〈𝑍, 𝐼〉} ↦ (2nd ‘𝑝)) = {〈〈𝑍, 𝐼〉, 𝐼〉})) |
19 | 14, 18 | mpbid 222 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑝 ∈ {〈𝑍, 𝐼〉} ↦ (2nd ‘𝑝)) = {〈〈𝑍, 𝐼〉, 𝐼〉}) |
20 | | xpsng 6569 |
. . . . . . . . . . 11
⊢ ((𝑍 ∈ 𝑊 ∧ 𝐼 ∈ 𝑉) → ({𝑍} × {𝐼}) = {〈𝑍, 𝐼〉}) |
21 | 20 | ancoms 468 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ({𝑍} × {𝐼}) = {〈𝑍, 𝐼〉}) |
22 | 21 | eqcomd 2766 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {〈𝑍, 𝐼〉} = ({𝑍} × {𝐼})) |
23 | 22 | mpteq1d 4890 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑝 ∈ {〈𝑍, 𝐼〉} ↦ (2nd ‘𝑝)) = (𝑝 ∈ ({𝑍} × {𝐼}) ↦ (2nd ‘𝑝))) |
24 | 19, 23 | eqtr3d 2796 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {〈〈𝑍, 𝐼〉, 𝐼〉} = (𝑝 ∈ ({𝑍} × {𝐼}) ↦ (2nd ‘𝑝))) |
25 | | vex 3343 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
26 | | vex 3343 |
. . . . . . . . . 10
⊢ 𝑖 ∈ V |
27 | 25, 26 | op2ndd 7344 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑧, 𝑖〉 → (2nd ‘𝑝) = 𝑖) |
28 | 27 | mpt2mpt 6917 |
. . . . . . . 8
⊢ (𝑝 ∈ ({𝑍} × {𝐼}) ↦ (2nd ‘𝑝)) = (𝑧 ∈ {𝑍}, 𝑖 ∈ {𝐼} ↦ 𝑖) |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑝 ∈ ({𝑍} × {𝐼}) ↦ (2nd ‘𝑝)) = (𝑧 ∈ {𝑍}, 𝑖 ∈ {𝐼} ↦ 𝑖)) |
30 | | snex 5057 |
. . . . . . . . 9
⊢ {𝑍} ∈ V |
31 | | lmod1zr.r |
. . . . . . . . . 10
⊢ 𝑅 = {〈(Base‘ndx),
{𝑍}〉,
〈(+g‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉,
〈(.r‘ndx), {〈〈𝑍, 𝑍〉, 𝑍〉}〉} |
32 | 31 | rngbase 16203 |
. . . . . . . . 9
⊢ ({𝑍} ∈ V → {𝑍} = (Base‘𝑅)) |
33 | 30, 32 | mp1i 13 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {𝑍} = (Base‘𝑅)) |
34 | | eqidd 2761 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {𝐼} = {𝐼}) |
35 | | mpt2eq12 6880 |
. . . . . . . 8
⊢ (({𝑍} = (Base‘𝑅) ∧ {𝐼} = {𝐼}) → (𝑧 ∈ {𝑍}, 𝑖 ∈ {𝐼} ↦ 𝑖) = (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)) |
36 | 33, 34, 35 | syl2anc 696 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑧 ∈ {𝑍}, 𝑖 ∈ {𝐼} ↦ 𝑖) = (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)) |
37 | 24, 29, 36 | 3eqtrd 2798 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {〈〈𝑍, 𝐼〉, 𝐼〉} = (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)) |
38 | 37 | opeq2d 4560 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 〈(
·𝑠 ‘ndx), {〈〈𝑍, 𝐼〉, 𝐼〉}〉 = 〈(
·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)〉) |
39 | 38 | sneqd 4333 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {〈(
·𝑠 ‘ndx), {〈〈𝑍, 𝐼〉, 𝐼〉}〉} = {〈(
·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)〉}) |
40 | 39 | uneq2d 3910 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ({〈(Base‘ndx), {𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), {〈〈𝑍, 𝐼〉, 𝐼〉}〉}) = ({〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)〉})) |
41 | 1, 40 | syl5eq 2806 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 = ({〈(Base‘ndx), {𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)〉})) |
42 | 31 | ring1 18802 |
. . 3
⊢ (𝑍 ∈ 𝑊 → 𝑅 ∈ Ring) |
43 | | eqidd 2761 |
. . . . . . . 8
⊢ (𝑧 = 𝑎 → 𝑖 = 𝑖) |
44 | | id 22 |
. . . . . . . 8
⊢ (𝑖 = 𝑏 → 𝑖 = 𝑏) |
45 | 43, 44 | cbvmpt2v 6900 |
. . . . . . 7
⊢ (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖) = (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ {𝐼} ↦ 𝑏) |
46 | 45 | opeq2i 4557 |
. . . . . 6
⊢ 〈(
·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)〉 = 〈(
·𝑠 ‘ndx), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ {𝐼} ↦ 𝑏)〉 |
47 | 46 | sneqi 4332 |
. . . . 5
⊢ {〈(
·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)〉} = {〈(
·𝑠 ‘ndx), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ {𝐼} ↦ 𝑏)〉} |
48 | 47 | uneq2i 3907 |
. . . 4
⊢
({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)〉}) = ({〈(Base‘ndx), {𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ {𝐼} ↦ 𝑏)〉}) |
49 | 48 | lmod1 42791 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) →
({〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx),
{〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)〉}) ∈ LMod) |
50 | 42, 49 | sylan2 492 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ({〈(Base‘ndx), {𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉, 〈(Scalar‘ndx),
𝑅〉} ∪ {〈(
·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)〉}) ∈ LMod) |
51 | 41, 50 | eqeltrd 2839 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∈ LMod) |