Step | Hyp | Ref
| Expression |
1 | | m2detleib.d |
. . . 4
⊢ 𝐷 = (𝑁 maDet 𝑅) |
2 | | m2detleib.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | | m2detleib.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
4 | | eqid 2610 |
. . . 4
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁)) |
5 | | eqid 2610 |
. . . 4
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
6 | | eqid 2610 |
. . . 4
⊢
(pmSgn‘𝑁) =
(pmSgn‘𝑁) |
7 | | m2detleib.t |
. . . 4
⊢ · =
(.r‘𝑅) |
8 | | eqid 2610 |
. . . 4
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetleib1 20216 |
. . 3
⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑘 ∈
(Base‘(SymGrp‘𝑁)) ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))))))) |
10 | 9 | adantl 481 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑘 ∈
(Base‘(SymGrp‘𝑁)) ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))))))) |
11 | | eqid 2610 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
12 | | eqid 2610 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
13 | | ringcmn 18404 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
14 | 13 | adantr 480 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ CMnd) |
15 | | m2detleib.n |
. . . . . 6
⊢ 𝑁 = {1, 2} |
16 | | prfi 8120 |
. . . . . 6
⊢ {1, 2}
∈ Fin |
17 | 15, 16 | eqeltri 2684 |
. . . . 5
⊢ 𝑁 ∈ Fin |
18 | | eqid 2610 |
. . . . . 6
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
19 | 18, 4 | symgbasfi 17629 |
. . . . 5
⊢ (𝑁 ∈ Fin →
(Base‘(SymGrp‘𝑁)) ∈ Fin) |
20 | 17, 19 | ax-mp 5 |
. . . 4
⊢
(Base‘(SymGrp‘𝑁)) ∈ Fin |
21 | 20 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) ∈ Fin) |
22 | | simpl 472 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
23 | 22 | adantr 480 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring) |
24 | 4, 6, 5 | zrhpsgnelbas 19759 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑘 ∈
(Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅)) |
25 | 17, 24 | mp3an2 1404 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈
(Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅)) |
26 | 25 | adantlr 747 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) →
((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅)) |
27 | | simpr 476 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑘 ∈ (Base‘(SymGrp‘𝑁))) |
28 | | simpr 476 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵) |
29 | 28 | adantr 480 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑀 ∈ 𝐵) |
30 | 15, 4, 2, 3, 8 | m2detleiblem2 20253 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈
(Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
31 | 23, 27, 29, 30 | syl3anc 1318 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
32 | 11, 7 | ringcl 18384 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) |
33 | 23, 26, 31, 32 | syl3anc 1318 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) →
(((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) |
34 | | opex 4859 |
. . . . . . . 8
⊢ 〈1,
1〉 ∈ V |
35 | | opex 4859 |
. . . . . . . 8
⊢ 〈2,
2〉 ∈ V |
36 | 34, 35 | pm3.2i 470 |
. . . . . . 7
⊢ (〈1,
1〉 ∈ V ∧ 〈2, 2〉 ∈ V) |
37 | | opex 4859 |
. . . . . . . 8
⊢ 〈1,
2〉 ∈ V |
38 | | opex 4859 |
. . . . . . . 8
⊢ 〈2,
1〉 ∈ V |
39 | 37, 38 | pm3.2i 470 |
. . . . . . 7
⊢ (〈1,
2〉 ∈ V ∧ 〈2, 1〉 ∈ V) |
40 | 36, 39 | pm3.2i 470 |
. . . . . 6
⊢
((〈1, 1〉 ∈ V ∧ 〈2, 2〉 ∈ V) ∧
(〈1, 2〉 ∈ V ∧ 〈2, 1〉 ∈ V)) |
41 | | 1ne2 11117 |
. . . . . . . . . 10
⊢ 1 ≠
2 |
42 | 41 | olci 405 |
. . . . . . . . 9
⊢ (1 ≠ 1
∨ 1 ≠ 2) |
43 | | 1ex 9914 |
. . . . . . . . . 10
⊢ 1 ∈
V |
44 | 43, 43 | opthne 4877 |
. . . . . . . . 9
⊢ (〈1,
1〉 ≠ 〈1, 2〉 ↔ (1 ≠ 1 ∨ 1 ≠ 2)) |
45 | 42, 44 | mpbir 220 |
. . . . . . . 8
⊢ 〈1,
1〉 ≠ 〈1, 2〉 |
46 | 41 | orci 404 |
. . . . . . . . 9
⊢ (1 ≠ 2
∨ 1 ≠ 1) |
47 | 43, 43 | opthne 4877 |
. . . . . . . . 9
⊢ (〈1,
1〉 ≠ 〈2, 1〉 ↔ (1 ≠ 2 ∨ 1 ≠ 1)) |
48 | 46, 47 | mpbir 220 |
. . . . . . . 8
⊢ 〈1,
1〉 ≠ 〈2, 1〉 |
49 | 45, 48 | pm3.2i 470 |
. . . . . . 7
⊢ (〈1,
1〉 ≠ 〈1, 2〉 ∧ 〈1, 1〉 ≠ 〈2,
1〉) |
50 | 49 | orci 404 |
. . . . . 6
⊢
((〈1, 1〉 ≠ 〈1, 2〉 ∧ 〈1, 1〉 ≠
〈2, 1〉) ∨ (〈2, 2〉 ≠ 〈1, 2〉 ∧ 〈2,
2〉 ≠ 〈2, 1〉)) |
51 | 40, 50 | pm3.2i 470 |
. . . . 5
⊢
(((〈1, 1〉 ∈ V ∧ 〈2, 2〉 ∈ V) ∧
(〈1, 2〉 ∈ V ∧ 〈2, 1〉 ∈ V)) ∧ ((〈1,
1〉 ≠ 〈1, 2〉 ∧ 〈1, 1〉 ≠ 〈2, 1〉)
∨ (〈2, 2〉 ≠ 〈1, 2〉 ∧ 〈2, 2〉 ≠
〈2, 1〉))) |
52 | 51 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((〈1, 1〉 ∈ V ∧
〈2, 2〉 ∈ V) ∧ (〈1, 2〉 ∈ V ∧ 〈2,
1〉 ∈ V)) ∧ ((〈1, 1〉 ≠ 〈1, 2〉 ∧
〈1, 1〉 ≠ 〈2, 1〉) ∨ (〈2, 2〉 ≠ 〈1,
2〉 ∧ 〈2, 2〉 ≠ 〈2, 1〉)))) |
53 | | prneimg 4328 |
. . . . 5
⊢
(((〈1, 1〉 ∈ V ∧ 〈2, 2〉 ∈ V) ∧
(〈1, 2〉 ∈ V ∧ 〈2, 1〉 ∈ V)) → (((〈1,
1〉 ≠ 〈1, 2〉 ∧ 〈1, 1〉 ≠ 〈2, 1〉)
∨ (〈2, 2〉 ≠ 〈1, 2〉 ∧ 〈2, 2〉 ≠
〈2, 1〉)) → {〈1, 1〉, 〈2, 2〉} ≠ {〈1,
2〉, 〈2, 1〉})) |
54 | 53 | imp 444 |
. . . 4
⊢
((((〈1, 1〉 ∈ V ∧ 〈2, 2〉 ∈ V) ∧
(〈1, 2〉 ∈ V ∧ 〈2, 1〉 ∈ V)) ∧ ((〈1,
1〉 ≠ 〈1, 2〉 ∧ 〈1, 1〉 ≠ 〈2, 1〉)
∨ (〈2, 2〉 ≠ 〈1, 2〉 ∧ 〈2, 2〉 ≠
〈2, 1〉))) → {〈1, 1〉, 〈2, 2〉} ≠ {〈1,
2〉, 〈2, 1〉}) |
55 | | disjsn2 4193 |
. . . 4
⊢
({〈1, 1〉, 〈2, 2〉} ≠ {〈1, 2〉, 〈2,
1〉} → ({{〈1, 1〉, 〈2, 2〉}} ∩ {{〈1,
2〉, 〈2, 1〉}}) = ∅) |
56 | 52, 54, 55 | 3syl 18 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ({{〈1, 1〉, 〈2,
2〉}} ∩ {{〈1, 2〉, 〈2, 1〉}}) =
∅) |
57 | | 2nn 11062 |
. . . . . 6
⊢ 2 ∈
ℕ |
58 | 18, 4, 15 | symg2bas 17641 |
. . . . . 6
⊢ ((1
∈ V ∧ 2 ∈ ℕ) → (Base‘(SymGrp‘𝑁)) = {{〈1, 1〉,
〈2, 2〉}, {〈1, 2〉, 〈2, 1〉}}) |
59 | 43, 57, 58 | mp2an 704 |
. . . . 5
⊢
(Base‘(SymGrp‘𝑁)) = {{〈1, 1〉, 〈2, 2〉},
{〈1, 2〉, 〈2, 1〉}} |
60 | | df-pr 4128 |
. . . . 5
⊢
{{〈1, 1〉, 〈2, 2〉}, {〈1, 2〉, 〈2,
1〉}} = ({{〈1, 1〉, 〈2, 2〉}} ∪ {{〈1, 2〉,
〈2, 1〉}}) |
61 | 59, 60 | eqtri 2632 |
. . . 4
⊢
(Base‘(SymGrp‘𝑁)) = ({{〈1, 1〉, 〈2, 2〉}}
∪ {{〈1, 2〉, 〈2, 1〉}}) |
62 | 61 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) = ({{〈1, 1〉,
〈2, 2〉}} ∪ {{〈1, 2〉, 〈2,
1〉}})) |
63 | 11, 12, 14, 21, 33, 56, 62 | gsummptfidmsplit 18153 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑘 ∈
(Base‘(SymGrp‘𝑁)) ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))) = ((𝑅 Σg (𝑘 ∈ {{〈1, 1〉,
〈2, 2〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))))))(+g‘𝑅)(𝑅 Σg (𝑘 ∈ {{〈1, 2〉,
〈2, 1〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))))) |
64 | | ringmnd 18379 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
65 | 64 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Mnd) |
66 | | prex 4836 |
. . . . . 6
⊢ {〈1,
1〉, 〈2, 2〉} ∈ V |
67 | 66 | a1i 11 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {〈1, 1〉, 〈2,
2〉} ∈ V) |
68 | 66 | prid1 4241 |
. . . . . . . . 9
⊢ {〈1,
1〉, 〈2, 2〉} ∈ {{〈1, 1〉, 〈2, 2〉},
{〈1, 2〉, 〈2, 1〉}} |
69 | 68, 59 | eleqtrri 2687 |
. . . . . . . 8
⊢ {〈1,
1〉, 〈2, 2〉} ∈ (Base‘(SymGrp‘𝑁)) |
70 | 69 | a1i 11 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → {〈1, 1〉, 〈2, 2〉}
∈ (Base‘(SymGrp‘𝑁))) |
71 | 4, 6, 5 | zrhpsgnelbas 19759 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ {〈1,
1〉, 〈2, 2〉} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ∈ (Base‘𝑅)) |
72 | 17, 71 | mp3an2 1404 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
1〉, 〈2, 2〉} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ∈ (Base‘𝑅)) |
73 | 70, 72 | sylan2 490 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ∈ (Base‘𝑅)) |
74 | 15, 4, 2, 3, 8 | m2detleiblem2 20253 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
1〉, 〈2, 2〉} ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
75 | 69, 74 | mp3an2 1404 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
76 | 11, 7 | ringcl 18384 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉, 〈2,
2〉})) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) |
77 | 22, 73, 75, 76 | syl3anc 1318 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) |
78 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → ((pmSgn‘𝑁)‘𝑘) = ((pmSgn‘𝑁)‘{〈1, 1〉, 〈2,
2〉})) |
79 | 78 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉, 〈2,
2〉}))) |
80 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → (𝑘‘𝑛) = ({〈1, 1〉, 〈2,
2〉}‘𝑛)) |
81 | 80 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → ((𝑘‘𝑛)𝑀𝑛) = (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)) |
82 | 81 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → (𝑛 ∈
𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)) = (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) |
83 | 82 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) = ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)))) |
84 | 79, 83 | oveq12d 6567 |
. . . . . 6
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉, 〈2,
2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))))) |
85 | 11, 84 | gsumsn 18177 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ {〈1,
1〉, 〈2, 2〉} ∈ V ∧ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑘 ∈ {{〈1, 1〉,
〈2, 2〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))))) |
86 | 65, 67, 77, 85 | syl3anc 1318 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑘 ∈ {{〈1, 1〉,
〈2, 2〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))))) |
87 | | prex 4836 |
. . . . . 6
⊢ {〈1,
2〉, 〈2, 1〉} ∈ V |
88 | 87 | a1i 11 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {〈1, 2〉, 〈2,
1〉} ∈ V) |
89 | 87 | prid2 4242 |
. . . . . . . . 9
⊢ {〈1,
2〉, 〈2, 1〉} ∈ {{〈1, 1〉, 〈2, 2〉},
{〈1, 2〉, 〈2, 1〉}} |
90 | 89, 59 | eleqtrri 2687 |
. . . . . . . 8
⊢ {〈1,
2〉, 〈2, 1〉} ∈ (Base‘(SymGrp‘𝑁)) |
91 | 90 | a1i 11 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → {〈1, 2〉, 〈2, 1〉}
∈ (Base‘(SymGrp‘𝑁))) |
92 | 4, 6, 5 | zrhpsgnelbas 19759 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ {〈1,
2〉, 〈2, 1〉} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ∈ (Base‘𝑅)) |
93 | 17, 92 | mp3an2 1404 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
2〉, 〈2, 1〉} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ∈ (Base‘𝑅)) |
94 | 91, 93 | sylan2 490 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ∈ (Base‘𝑅)) |
95 | 15, 4, 2, 3, 8 | m2detleiblem2 20253 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
2〉, 〈2, 1〉} ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
96 | 90, 95 | mp3an2 1404 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
97 | 11, 7 | ringcl 18384 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉, 〈2,
1〉})) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) |
98 | 22, 94, 96, 97 | syl3anc 1318 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) |
99 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → ((pmSgn‘𝑁)‘𝑘) = ((pmSgn‘𝑁)‘{〈1, 2〉, 〈2,
1〉})) |
100 | 99 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉, 〈2,
1〉}))) |
101 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → (𝑘‘𝑛) = ({〈1, 2〉, 〈2,
1〉}‘𝑛)) |
102 | 101 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → ((𝑘‘𝑛)𝑀𝑛) = (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)) |
103 | 102 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → (𝑛 ∈
𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)) = (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) |
104 | 103 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) = ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)))) |
105 | 100, 104 | oveq12d 6567 |
. . . . . 6
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉, 〈2,
1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))))) |
106 | 11, 105 | gsumsn 18177 |
. . . . 5
⊢ ((𝑅 ∈ Mnd ∧ {〈1,
2〉, 〈2, 1〉} ∈ V ∧ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑘 ∈ {{〈1, 2〉,
〈2, 1〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))))) |
107 | 65, 88, 98, 106 | syl3anc 1318 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑘 ∈ {{〈1, 2〉,
〈2, 1〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))))) |
108 | 86, 107 | oveq12d 6567 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑅 Σg (𝑘 ∈ {{〈1, 1〉,
〈2, 2〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))))))(+g‘𝑅)(𝑅 Σg (𝑘 ∈ {{〈1, 2〉,
〈2, 1〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))))))) = ((((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))))(+g‘𝑅)(((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉, 〈2,
1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)))))) |
109 | | eqidd 2611 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → {〈1, 1〉, 〈2, 2〉}
= {〈1, 1〉, 〈2, 2〉}) |
110 | | eqid 2610 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
111 | 15, 4, 5, 6, 110 | m2detleiblem5 20250 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
1〉, 〈2, 2〉} = {〈1, 1〉, 〈2, 2〉}) →
((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉, 〈2,
2〉})) = (1r‘𝑅)) |
112 | 109, 111 | sylan2 490 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) = (1r‘𝑅)) |
113 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {〈1, 1〉, 〈2,
2〉} = {〈1, 1〉, 〈2, 2〉}) |
114 | 8, 7 | mgpplusg 18316 |
. . . . . . . 8
⊢ · =
(+g‘(mulGrp‘𝑅)) |
115 | 15, 4, 2, 3, 8, 114 | m2detleiblem3 20254 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
1〉, 〈2, 2〉} = {〈1, 1〉, 〈2, 2〉} ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2))) |
116 | 22, 113, 28, 115 | syl3anc 1318 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2))) |
117 | 112, 116 | oveq12d 6567 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)))) = ((1r‘𝑅) · ((1𝑀1) · (2𝑀2)))) |
118 | 43 | prid1 4241 |
. . . . . . . . . 10
⊢ 1 ∈
{1, 2} |
119 | 118, 15 | eleqtrri 2687 |
. . . . . . . . 9
⊢ 1 ∈
𝑁 |
120 | 119 | a1i 11 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 1 ∈ 𝑁) |
121 | 3 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘𝐴)) |
122 | 121 | biimpi 205 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (Base‘𝐴)) |
123 | 122 | adantl 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ (Base‘𝐴)) |
124 | 2, 11 | matecl 20050 |
. . . . . . . 8
⊢ ((1
∈ 𝑁 ∧ 1 ∈
𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (1𝑀1) ∈ (Base‘𝑅)) |
125 | 120, 120,
123, 124 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (1𝑀1) ∈ (Base‘𝑅)) |
126 | | prid2g 4240 |
. . . . . . . . . . 11
⊢ (2 ∈
ℕ → 2 ∈ {1, 2}) |
127 | 57, 126 | ax-mp 5 |
. . . . . . . . . 10
⊢ 2 ∈
{1, 2} |
128 | 127, 15 | eleqtrri 2687 |
. . . . . . . . 9
⊢ 2 ∈
𝑁 |
129 | 128 | a1i 11 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 2 ∈ 𝑁) |
130 | 2, 11 | matecl 20050 |
. . . . . . . 8
⊢ ((2
∈ 𝑁 ∧ 2 ∈
𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (2𝑀2) ∈ (Base‘𝑅)) |
131 | 129, 129,
123, 130 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (2𝑀2) ∈ (Base‘𝑅)) |
132 | 11, 7 | ringcl 18384 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (1𝑀1) ∈ (Base‘𝑅) ∧ (2𝑀2) ∈ (Base‘𝑅)) → ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅)) |
133 | 22, 125, 131, 132 | syl3anc 1318 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅)) |
134 | 11, 7, 110 | ringlidm 18394 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅)) → ((1r‘𝑅) · ((1𝑀1) · (2𝑀2))) = ((1𝑀1) · (2𝑀2))) |
135 | 133, 134 | syldan 486 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((1r‘𝑅) · ((1𝑀1) · (2𝑀2))) = ((1𝑀1) · (2𝑀2))) |
136 | 117, 135 | eqtrd 2644 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)))) = ((1𝑀1) · (2𝑀2))) |
137 | | eqidd 2611 |
. . . . . 6
⊢ (𝑀 ∈ 𝐵 → {〈1, 2〉, 〈2, 1〉}
= {〈1, 2〉, 〈2, 1〉}) |
138 | | eqid 2610 |
. . . . . . 7
⊢
(invg‘𝑅) = (invg‘𝑅) |
139 | 15, 4, 5, 6, 110, 138 | m2detleiblem6 20251 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ {〈1,
2〉, 〈2, 1〉} = {〈1, 2〉, 〈2, 1〉}) →
((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉, 〈2,
1〉})) = ((invg‘𝑅)‘(1r‘𝑅))) |
140 | 137, 139 | sylan2 490 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) = ((invg‘𝑅)‘(1r‘𝑅))) |
141 | | eqidd 2611 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {〈1, 2〉, 〈2,
1〉} = {〈1, 2〉, 〈2, 1〉}) |
142 | 15, 4, 2, 3, 8, 114 | m2detleiblem4 20255 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ {〈1,
2〉, 〈2, 1〉} = {〈1, 2〉, 〈2, 1〉} ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2))) |
143 | 22, 141, 28, 142 | syl3anc 1318 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2))) |
144 | 140, 143 | oveq12d 6567 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)))) = (((invg‘𝑅)‘(1r‘𝑅)) · ((2𝑀1) · (1𝑀2)))) |
145 | 136, 144 | oveq12d 6567 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))))(+g‘𝑅)(((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉, 〈2,
1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))))) = (((1𝑀1) · (2𝑀2))(+g‘𝑅)(((invg‘𝑅)‘(1r‘𝑅)) · ((2𝑀1) · (1𝑀2))))) |
146 | 2, 11 | matecl 20050 |
. . . . . 6
⊢ ((2
∈ 𝑁 ∧ 1 ∈
𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (2𝑀1) ∈ (Base‘𝑅)) |
147 | 129, 120,
123, 146 | syl3anc 1318 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (2𝑀1) ∈ (Base‘𝑅)) |
148 | 2, 11 | matecl 20050 |
. . . . . 6
⊢ ((1
∈ 𝑁 ∧ 2 ∈
𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (1𝑀2) ∈ (Base‘𝑅)) |
149 | 120, 129,
123, 148 | syl3anc 1318 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (1𝑀2) ∈ (Base‘𝑅)) |
150 | 11, 7 | ringcl 18384 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (2𝑀1) ∈ (Base‘𝑅) ∧ (1𝑀2) ∈ (Base‘𝑅)) → ((2𝑀1) · (1𝑀2)) ∈ (Base‘𝑅)) |
151 | 22, 147, 149, 150 | syl3anc 1318 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((2𝑀1) · (1𝑀2)) ∈ (Base‘𝑅)) |
152 | | m2detleib.m |
. . . . 5
⊢ − =
(-g‘𝑅) |
153 | 15, 4, 5, 6, 110, 138, 7, 152 | m2detleiblem7 20252 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅) ∧ ((2𝑀1) · (1𝑀2)) ∈ (Base‘𝑅)) → (((1𝑀1) · (2𝑀2))(+g‘𝑅)(((invg‘𝑅)‘(1r‘𝑅)) · ((2𝑀1) · (1𝑀2)))) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2)))) |
154 | 22, 133, 151, 153 | syl3anc 1318 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((1𝑀1) · (2𝑀2))(+g‘𝑅)(((invg‘𝑅)‘(1r‘𝑅)) · ((2𝑀1) · (1𝑀2)))) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2)))) |
155 | 108, 145,
154 | 3eqtrd 2648 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑅 Σg (𝑘 ∈ {{〈1, 1〉,
〈2, 2〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))))))(+g‘𝑅)(𝑅 Σg (𝑘 ∈ {{〈1, 2〉,
〈2, 1〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))))))) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2)))) |
156 | 10, 63, 155 | 3eqtrd 2648 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2)))) |