| Step | Hyp | Ref
| Expression |
| 1 | | m2detleib.d |
. . . 4
⊢ 𝐷 = (𝑁 maDet 𝑅) |
| 2 | | m2detleib.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 3 | | m2detleib.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
| 4 | | eqid 2737 |
. . . 4
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁)) |
| 5 | | eqid 2737 |
. . . 4
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
| 6 | | eqid 2737 |
. . . 4
⊢
(pmSgn‘𝑁) =
(pmSgn‘𝑁) |
| 7 | | m2detleib.t |
. . . 4
⊢ · =
(.r‘𝑅) |
| 8 | | eqid 2737 |
. . . 4
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetleib1 22597 |
. . 3
⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑘 ∈
(Base‘(SymGrp‘𝑁)) ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))))))) |
| 10 | 9 | adantl 481 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑘 ∈
(Base‘(SymGrp‘𝑁)) ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))))))) |
| 11 | | eqid 2737 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 12 | | eqid 2737 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 13 | | ringcmn 20279 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd) |
| 14 | 13 | adantr 480 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ CMnd) |
| 15 | | m2detleib.n |
. . . . . 6
⊢ 𝑁 = {1, 2} |
| 16 | | prfi 9363 |
. . . . . 6
⊢ {1, 2}
∈ Fin |
| 17 | 15, 16 | eqeltri 2837 |
. . . . 5
⊢ 𝑁 ∈ Fin |
| 18 | | eqid 2737 |
. . . . . 6
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
| 19 | 18, 4 | symgbasfi 19396 |
. . . . 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 482 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
| 23 | 22 | adantr 480 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring) |
| 24 | 4, 6, 5 | zrhpsgnelbas 21612 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑘 ∈
(Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅)) |
| 25 | 17, 24 | mp3an2 1451 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈
(Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅)) |
| 26 | 25 | adantlr 715 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) →
((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅)) |
| 27 | | simpr 484 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑘 ∈ (Base‘(SymGrp‘𝑁))) |
| 28 | | simpr 484 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵) |
| 29 | 28 | adantr 480 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → 𝑀 ∈ 𝐵) |
| 30 | 15, 4, 2, 3, 8 | m2detleiblem2 22634 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈
(Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
| 31 | 23, 27, 29, 30 | syl3anc 1373 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg
(𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
| 32 | 11, 7 | ringcl 20247 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ∈ (Base‘𝑅) ∧ ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) |
| 33 | 23, 26, 31, 32 | syl3anc 1373 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ (Base‘(SymGrp‘𝑁))) →
(((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) |
| 34 | | opex 5469 |
. . . . . . . 8
⊢ 〈1,
1〉 ∈ V |
| 35 | | opex 5469 |
. . . . . . . 8
⊢ 〈2,
2〉 ∈ V |
| 36 | 34, 35 | pm3.2i 470 |
. . . . . . 7
⊢ (〈1,
1〉 ∈ V ∧ 〈2, 2〉 ∈ V) |
| 37 | | opex 5469 |
. . . . . . . 8
⊢ 〈1,
2〉 ∈ V |
| 38 | | opex 5469 |
. . . . . . . 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 12474 |
. . . . . . . . . 10
⊢ 1 ≠
2 |
| 42 | 41 | olci 867 |
. . . . . . . . 9
⊢ (1 ≠ 1
∨ 1 ≠ 2) |
| 43 | | 1ex 11257 |
. . . . . . . . . 10
⊢ 1 ∈
V |
| 44 | 43, 43 | opthne 5487 |
. . . . . . . . 9
⊢ (〈1,
1〉 ≠ 〈1, 2〉 ↔ (1 ≠ 1 ∨ 1 ≠ 2)) |
| 45 | 42, 44 | mpbir 231 |
. . . . . . . 8
⊢ 〈1,
1〉 ≠ 〈1, 2〉 |
| 46 | 41 | orci 866 |
. . . . . . . . 9
⊢ (1 ≠ 2
∨ 1 ≠ 1) |
| 47 | 43, 43 | opthne 5487 |
. . . . . . . . 9
⊢ (〈1,
1〉 ≠ 〈2, 1〉 ↔ (1 ≠ 2 ∨ 1 ≠ 1)) |
| 48 | 46, 47 | mpbir 231 |
. . . . . . . 8
⊢ 〈1,
1〉 ≠ 〈2, 1〉 |
| 49 | 45, 48 | pm3.2i 470 |
. . . . . . 7
⊢ (〈1,
1〉 ≠ 〈1, 2〉 ∧ 〈1, 1〉 ≠ 〈2,
1〉) |
| 50 | 49 | orci 866 |
. . . . . 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 4854 |
. . . . 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 406 |
. . . 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 4712 |
. . . 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 12339 |
. . . . . 6
⊢ 2 ∈
ℕ |
| 58 | 18, 4, 15 | symg2bas 19410 |
. . . . . 6
⊢ ((1
∈ V ∧ 2 ∈ ℕ) → (Base‘(SymGrp‘𝑁)) = {{〈1, 1〉,
〈2, 2〉}, {〈1, 2〉, 〈2, 1〉}}) |
| 59 | 43, 57, 58 | mp2an 692 |
. . . . 5
⊢
(Base‘(SymGrp‘𝑁)) = {{〈1, 1〉, 〈2, 2〉},
{〈1, 2〉, 〈2, 1〉}} |
| 60 | | df-pr 4629 |
. . . . 5
⊢
{{〈1, 1〉, 〈2, 2〉}, {〈1, 2〉, 〈2,
1〉}} = ({{〈1, 1〉, 〈2, 2〉}} ∪ {{〈1, 2〉,
〈2, 1〉}}) |
| 61 | 59, 60 | eqtri 2765 |
. . . 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 19948 |
. 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 20240 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
| 65 | 64 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Mnd) |
| 66 | | prex 5437 |
. . . . . 6
⊢ {〈1,
1〉, 〈2, 2〉} ∈ V |
| 67 | 66 | a1i 11 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {〈1, 1〉, 〈2,
2〉} ∈ V) |
| 68 | 66 | prid1 4762 |
. . . . . . . . 9
⊢ {〈1,
1〉, 〈2, 2〉} ∈ {{〈1, 1〉, 〈2, 2〉},
{〈1, 2〉, 〈2, 1〉}} |
| 69 | 68, 59 | eleqtrri 2840 |
. . . . . . . 8
⊢ {〈1,
1〉, 〈2, 2〉} ∈ (Base‘(SymGrp‘𝑁)) |
| 70 | 69 | a1i 11 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → {〈1, 1〉, 〈2, 2〉}
∈ (Base‘(SymGrp‘𝑁))) |
| 71 | 4, 6, 5 | zrhpsgnelbas 21612 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ {〈1,
1〉, 〈2, 2〉} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ∈ (Base‘𝑅)) |
| 72 | 17, 71 | mp3an2 1451 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
1〉, 〈2, 2〉} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ∈ (Base‘𝑅)) |
| 73 | 70, 72 | sylan2 593 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ∈ (Base‘𝑅)) |
| 74 | 15, 4, 2, 3, 8 | m2detleiblem2 22634 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
1〉, 〈2, 2〉} ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
| 75 | 69, 74 | mp3an2 1451 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
| 76 | 11, 7 | ringcl 20247 |
. . . . . 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 1373 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) |
| 78 | | 2fveq3 6911 |
. . . . . . 7
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉, 〈2,
2〉}))) |
| 79 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → (𝑘‘𝑛) = ({〈1, 1〉, 〈2,
2〉}‘𝑛)) |
| 80 | 79 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → ((𝑘‘𝑛)𝑀𝑛) = (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)) |
| 81 | 80 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → (𝑛 ∈
𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)) = (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) |
| 82 | 81 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) = ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)))) |
| 83 | 78, 82 | oveq12d 7449 |
. . . . . 6
⊢ (𝑘 = {〈1, 1〉, 〈2,
2〉} → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉, 〈2,
2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))))) |
| 84 | 11, 83 | gsumsn 19972 |
. . . . 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〉}‘𝑛)𝑀𝑛))))) |
| 85 | 65, 67, 77, 84 | syl3anc 1373 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑘 ∈ {{〈1, 1〉,
〈2, 2〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))))) |
| 86 | | prex 5437 |
. . . . . 6
⊢ {〈1,
2〉, 〈2, 1〉} ∈ V |
| 87 | 86 | a1i 11 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {〈1, 2〉, 〈2,
1〉} ∈ V) |
| 88 | 86 | prid2 4763 |
. . . . . . . . 9
⊢ {〈1,
2〉, 〈2, 1〉} ∈ {{〈1, 1〉, 〈2, 2〉},
{〈1, 2〉, 〈2, 1〉}} |
| 89 | 88, 59 | eleqtrri 2840 |
. . . . . . . 8
⊢ {〈1,
2〉, 〈2, 1〉} ∈ (Base‘(SymGrp‘𝑁)) |
| 90 | 89 | a1i 11 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → {〈1, 2〉, 〈2, 1〉}
∈ (Base‘(SymGrp‘𝑁))) |
| 91 | 4, 6, 5 | zrhpsgnelbas 21612 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ {〈1,
2〉, 〈2, 1〉} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ∈ (Base‘𝑅)) |
| 92 | 17, 91 | mp3an2 1451 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
2〉, 〈2, 1〉} ∈ (Base‘(SymGrp‘𝑁))) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ∈ (Base‘𝑅)) |
| 93 | 90, 92 | sylan2 593 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ∈ (Base‘𝑅)) |
| 94 | 15, 4, 2, 3, 8 | m2detleiblem2 22634 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
2〉, 〈2, 1〉} ∈ (Base‘(SymGrp‘𝑁)) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
| 95 | 89, 94 | mp3an2 1451 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) |
| 96 | 11, 7 | ringcl 20247 |
. . . . . 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‘𝑅)) |
| 97 | 22, 93, 95, 96 | syl3anc 1373 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅)) |
| 98 | | 2fveq3 6911 |
. . . . . . 7
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉, 〈2,
1〉}))) |
| 99 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → (𝑘‘𝑛) = ({〈1, 2〉, 〈2,
1〉}‘𝑛)) |
| 100 | 99 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → ((𝑘‘𝑛)𝑀𝑛) = (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)) |
| 101 | 100 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → (𝑛 ∈
𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)) = (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) |
| 102 | 101 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛))) = ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)))) |
| 103 | 98, 102 | oveq12d 7449 |
. . . . . 6
⊢ (𝑘 = {〈1, 2〉, 〈2,
1〉} → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉, 〈2,
1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))))) |
| 104 | 11, 103 | gsumsn 19972 |
. . . . 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〉}‘𝑛)𝑀𝑛))))) |
| 105 | 65, 87, 97, 104 | syl3anc 1373 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑘 ∈ {{〈1, 2〉,
〈2, 1〉}} ↦ (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘𝑘)) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ ((𝑘‘𝑛)𝑀𝑛)))))) = (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))))) |
| 106 | 85, 105 | oveq12d 7449 |
. . 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〉}‘𝑛)𝑀𝑛)))))) |
| 107 | | eqidd 2738 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → {〈1, 1〉, 〈2, 2〉}
= {〈1, 1〉, 〈2, 2〉}) |
| 108 | | eqid 2737 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 109 | 15, 4, 5, 6, 108 | m2detleiblem5 22631 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
1〉, 〈2, 2〉} = {〈1, 1〉, 〈2, 2〉}) →
((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉, 〈2,
2〉})) = (1r‘𝑅)) |
| 110 | 107, 109 | sylan2 593 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) = (1r‘𝑅)) |
| 111 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {〈1, 1〉, 〈2,
2〉} = {〈1, 1〉, 〈2, 2〉}) |
| 112 | 8, 7 | mgpplusg 20141 |
. . . . . . . 8
⊢ · =
(+g‘(mulGrp‘𝑅)) |
| 113 | 15, 4, 2, 3, 8, 112 | m2detleiblem3 22635 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ {〈1,
1〉, 〈2, 2〉} = {〈1, 1〉, 〈2, 2〉} ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2))) |
| 114 | 22, 111, 28, 113 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2))) |
| 115 | 110, 114 | oveq12d 7449 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)))) = ((1r‘𝑅) · ((1𝑀1) · (2𝑀2)))) |
| 116 | 43 | prid1 4762 |
. . . . . . . . . 10
⊢ 1 ∈
{1, 2} |
| 117 | 116, 15 | eleqtrri 2840 |
. . . . . . . . 9
⊢ 1 ∈
𝑁 |
| 118 | 117 | a1i 11 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 1 ∈ 𝑁) |
| 119 | 3 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘𝐴)) |
| 120 | 119 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (Base‘𝐴)) |
| 121 | 120 | adantl 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ (Base‘𝐴)) |
| 122 | 2, 11 | matecl 22431 |
. . . . . . . 8
⊢ ((1
∈ 𝑁 ∧ 1 ∈
𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (1𝑀1) ∈ (Base‘𝑅)) |
| 123 | 118, 118,
121, 122 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (1𝑀1) ∈ (Base‘𝑅)) |
| 124 | | prid2g 4761 |
. . . . . . . . . . 11
⊢ (2 ∈
ℕ → 2 ∈ {1, 2}) |
| 125 | 57, 124 | ax-mp 5 |
. . . . . . . . . 10
⊢ 2 ∈
{1, 2} |
| 126 | 125, 15 | eleqtrri 2840 |
. . . . . . . . 9
⊢ 2 ∈
𝑁 |
| 127 | 126 | a1i 11 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 2 ∈ 𝑁) |
| 128 | 2, 11 | matecl 22431 |
. . . . . . . 8
⊢ ((2
∈ 𝑁 ∧ 2 ∈
𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (2𝑀2) ∈ (Base‘𝑅)) |
| 129 | 127, 127,
121, 128 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (2𝑀2) ∈ (Base‘𝑅)) |
| 130 | 11, 7 | ringcl 20247 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (1𝑀1) ∈ (Base‘𝑅) ∧ (2𝑀2) ∈ (Base‘𝑅)) → ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅)) |
| 131 | 22, 123, 129, 130 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅)) |
| 132 | 11, 7, 108 | ringlidm 20266 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ ((1𝑀1) · (2𝑀2)) ∈ (Base‘𝑅)) → ((1r‘𝑅) · ((1𝑀1) · (2𝑀2))) = ((1𝑀1) · (2𝑀2))) |
| 133 | 131, 132 | syldan 591 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((1r‘𝑅) · ((1𝑀1) · (2𝑀2))) = ((1𝑀1) · (2𝑀2))) |
| 134 | 115, 133 | eqtrd 2777 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 1〉,
〈2, 2〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 1〉, 〈2,
2〉}‘𝑛)𝑀𝑛)))) = ((1𝑀1) · (2𝑀2))) |
| 135 | | eqidd 2738 |
. . . . . 6
⊢ (𝑀 ∈ 𝐵 → {〈1, 2〉, 〈2, 1〉}
= {〈1, 2〉, 〈2, 1〉}) |
| 136 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 137 | 15, 4, 5, 6, 108, 136 | m2detleiblem6 22632 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ {〈1,
2〉, 〈2, 1〉} = {〈1, 2〉, 〈2, 1〉}) →
((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉, 〈2,
1〉})) = ((invg‘𝑅)‘(1r‘𝑅))) |
| 138 | 135, 137 | sylan2 593 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) = ((invg‘𝑅)‘(1r‘𝑅))) |
| 139 | | eqidd 2738 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {〈1, 2〉, 〈2,
1〉} = {〈1, 2〉, 〈2, 1〉}) |
| 140 | 15, 4, 2, 3, 8, 112 | m2detleiblem4 22636 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ {〈1,
2〉, 〈2, 1〉} = {〈1, 2〉, 〈2, 1〉} ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2))) |
| 141 | 22, 139, 28, 140 | syl3anc 1373 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2))) |
| 142 | 138, 141 | oveq12d 7449 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈1, 2〉,
〈2, 1〉})) ·
((mulGrp‘𝑅)
Σg (𝑛 ∈ 𝑁 ↦ (({〈1, 2〉, 〈2,
1〉}‘𝑛)𝑀𝑛)))) = (((invg‘𝑅)‘(1r‘𝑅)) · ((2𝑀1) · (1𝑀2)))) |
| 143 | 134, 142 | oveq12d 7449 |
. . 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))))) |
| 144 | 2, 11 | matecl 22431 |
. . . . . 6
⊢ ((2
∈ 𝑁 ∧ 1 ∈
𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (2𝑀1) ∈ (Base‘𝑅)) |
| 145 | 127, 118,
121, 144 | syl3anc 1373 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (2𝑀1) ∈ (Base‘𝑅)) |
| 146 | 2, 11 | matecl 22431 |
. . . . . 6
⊢ ((1
∈ 𝑁 ∧ 2 ∈
𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (1𝑀2) ∈ (Base‘𝑅)) |
| 147 | 118, 127,
121, 146 | syl3anc 1373 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (1𝑀2) ∈ (Base‘𝑅)) |
| 148 | 11, 7 | ringcl 20247 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (2𝑀1) ∈ (Base‘𝑅) ∧ (1𝑀2) ∈ (Base‘𝑅)) → ((2𝑀1) · (1𝑀2)) ∈ (Base‘𝑅)) |
| 149 | 22, 145, 147, 148 | syl3anc 1373 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((2𝑀1) · (1𝑀2)) ∈ (Base‘𝑅)) |
| 150 | | m2detleib.m |
. . . . 5
⊢ − =
(-g‘𝑅) |
| 151 | 15, 4, 5, 6, 108, 136, 7, 150 | m2detleiblem7 22633 |
. . . 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)))) |
| 152 | 22, 131, 149, 151 | syl3anc 1373 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (((1𝑀1) · (2𝑀2))(+g‘𝑅)(((invg‘𝑅)‘(1r‘𝑅)) · ((2𝑀1) · (1𝑀2)))) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2)))) |
| 153 | 106, 143,
152 | 3eqtrd 2781 |
. 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)))) |
| 154 | 10, 63, 153 | 3eqtrd 2781 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2)))) |