Proof of Theorem m2detleiblem4
Step | Hyp | Ref
| Expression |
1 | | m2detleiblem2.g |
. . . 4
⊢ 𝐺 = (mulGrp‘𝑅) |
2 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | 1, 2 | mgpbas 18318 |
. . 3
⊢
(Base‘𝑅) =
(Base‘𝐺) |
4 | | m2detleiblem3.m |
. . 3
⊢ · =
(+g‘𝐺) |
5 | | fvex 6113 |
. . . . 5
⊢
(mulGrp‘𝑅)
∈ V |
6 | 1, 5 | eqeltri 2684 |
. . . 4
⊢ 𝐺 ∈ V |
7 | 6 | a1i 11 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → 𝐺 ∈ V) |
8 | | 1ex 9914 |
. . . . . . 7
⊢ 1 ∈
V |
9 | | 2nn 11062 |
. . . . . . 7
⊢ 2 ∈
ℕ |
10 | | prex 4836 |
. . . . . . . . 9
⊢ {〈1,
2〉, 〈2, 1〉} ∈ V |
11 | 10 | prid2 4242 |
. . . . . . . 8
⊢ {〈1,
2〉, 〈2, 1〉} ∈ {{〈1, 1〉, 〈2, 2〉},
{〈1, 2〉, 〈2, 1〉}} |
12 | | eqid 2610 |
. . . . . . . . 9
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
13 | | m2detleiblem2.p |
. . . . . . . . 9
⊢ 𝑃 =
(Base‘(SymGrp‘𝑁)) |
14 | | m2detleiblem2.n |
. . . . . . . . 9
⊢ 𝑁 = {1, 2} |
15 | 12, 13, 14 | symg2bas 17641 |
. . . . . . . 8
⊢ ((1
∈ V ∧ 2 ∈ ℕ) → 𝑃 = {{〈1, 1〉, 〈2, 2〉},
{〈1, 2〉, 〈2, 1〉}}) |
16 | 11, 15 | syl5eleqr 2695 |
. . . . . . 7
⊢ ((1
∈ V ∧ 2 ∈ ℕ) → {〈1, 2〉, 〈2, 1〉}
∈ 𝑃) |
17 | 8, 9, 16 | mp2an 704 |
. . . . . 6
⊢ {〈1,
2〉, 〈2, 1〉} ∈ 𝑃 |
18 | | eleq1 2676 |
. . . . . 6
⊢ (𝑄 = {〈1, 2〉, 〈2,
1〉} → (𝑄 ∈
𝑃 ↔ {〈1, 2〉,
〈2, 1〉} ∈ 𝑃)) |
19 | 17, 18 | mpbiri 247 |
. . . . 5
⊢ (𝑄 = {〈1, 2〉, 〈2,
1〉} → 𝑄 ∈
𝑃) |
20 | | m2detleiblem2.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
21 | 14 | oveq1i 6559 |
. . . . . . 7
⊢ (𝑁 Mat 𝑅) = ({1, 2} Mat 𝑅) |
22 | 20, 21 | eqtri 2632 |
. . . . . 6
⊢ 𝐴 = ({1, 2} Mat 𝑅) |
23 | | m2detleiblem2.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐴) |
24 | 14 | fveq2i 6106 |
. . . . . . . 8
⊢
(SymGrp‘𝑁) =
(SymGrp‘{1, 2}) |
25 | 24 | fveq2i 6106 |
. . . . . . 7
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘{1,
2})) |
26 | 13, 25 | eqtri 2632 |
. . . . . 6
⊢ 𝑃 = (Base‘(SymGrp‘{1,
2})) |
27 | 22, 23, 26 | matepmcl 20087 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ {1, 2} ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅)) |
28 | 19, 27 | syl3an2 1352 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → ∀𝑛 ∈ {1, 2} ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅)) |
29 | | mpteq1 4665 |
. . . . . 6
⊢ (𝑁 = {1, 2} → (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)) = (𝑛 ∈ {1, 2} ↦ ((𝑄‘𝑛)𝑀𝑛))) |
30 | 14, 29 | ax-mp 5 |
. . . . 5
⊢ (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)) = (𝑛 ∈ {1, 2} ↦ ((𝑄‘𝑛)𝑀𝑛)) |
31 | 30 | fmpt 6289 |
. . . 4
⊢
(∀𝑛 ∈
{1, 2} ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅) ↔ (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)):{1, 2}⟶(Base‘𝑅)) |
32 | 28, 31 | sylib 207 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)):{1, 2}⟶(Base‘𝑅)) |
33 | 3, 4, 7, 32 | gsumpr12val 17105 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → (𝐺 Σg
(𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) = (((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘1) · ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘2))) |
34 | 8 | prid1 4241 |
. . . . . 6
⊢ 1 ∈
{1, 2} |
35 | 34, 14 | eleqtrri 2687 |
. . . . 5
⊢ 1 ∈
𝑁 |
36 | 20, 23, 13 | matepmcl 20087 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ 𝑁 ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅)) |
37 | 19, 36 | syl3an2 1352 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → ∀𝑛 ∈ 𝑁 ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅)) |
38 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (𝑄‘𝑛) = (𝑄‘1)) |
39 | | id 22 |
. . . . . . . . 9
⊢ (𝑛 = 1 → 𝑛 = 1) |
40 | 38, 39 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑛 = 1 → ((𝑄‘𝑛)𝑀𝑛) = ((𝑄‘1)𝑀1)) |
41 | 40 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑛 = 1 → (((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅) ↔ ((𝑄‘1)𝑀1) ∈ (Base‘𝑅))) |
42 | 41 | rspcva 3280 |
. . . . . 6
⊢ ((1
∈ 𝑁 ∧
∀𝑛 ∈ 𝑁 ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅)) → ((𝑄‘1)𝑀1) ∈ (Base‘𝑅)) |
43 | 35, 37, 42 | sylancr 694 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → ((𝑄‘1)𝑀1) ∈ (Base‘𝑅)) |
44 | | eqid 2610 |
. . . . . 6
⊢ (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)) = (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)) |
45 | 40, 44 | fvmptg 6189 |
. . . . 5
⊢ ((1
∈ 𝑁 ∧ ((𝑄‘1)𝑀1) ∈ (Base‘𝑅)) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘1) = ((𝑄‘1)𝑀1)) |
46 | 35, 43, 45 | sylancr 694 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘1) = ((𝑄‘1)𝑀1)) |
47 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑄 = {〈1, 2〉, 〈2,
1〉} → (𝑄‘1)
= ({〈1, 2〉, 〈2, 1〉}‘1)) |
48 | | 1ne2 11117 |
. . . . . . . 8
⊢ 1 ≠
2 |
49 | | 2ex 10969 |
. . . . . . . . 9
⊢ 2 ∈
V |
50 | 8, 49 | fvpr1 6361 |
. . . . . . . 8
⊢ (1 ≠ 2
→ ({〈1, 2〉, 〈2, 1〉}‘1) = 2) |
51 | 48, 50 | ax-mp 5 |
. . . . . . 7
⊢
({〈1, 2〉, 〈2, 1〉}‘1) = 2 |
52 | 47, 51 | syl6eq 2660 |
. . . . . 6
⊢ (𝑄 = {〈1, 2〉, 〈2,
1〉} → (𝑄‘1)
= 2) |
53 | 52 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → (𝑄‘1) = 2) |
54 | 53 | oveq1d 6564 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → ((𝑄‘1)𝑀1) = (2𝑀1)) |
55 | 46, 54 | eqtrd 2644 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘1) = (2𝑀1)) |
56 | 49 | prid2 4242 |
. . . . . 6
⊢ 2 ∈
{1, 2} |
57 | 56, 14 | eleqtrri 2687 |
. . . . 5
⊢ 2 ∈
𝑁 |
58 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑛 = 2 → (𝑄‘𝑛) = (𝑄‘2)) |
59 | | id 22 |
. . . . . . . . 9
⊢ (𝑛 = 2 → 𝑛 = 2) |
60 | 58, 59 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑛 = 2 → ((𝑄‘𝑛)𝑀𝑛) = ((𝑄‘2)𝑀2)) |
61 | 60 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑛 = 2 → (((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅) ↔ ((𝑄‘2)𝑀2) ∈ (Base‘𝑅))) |
62 | 61 | rspcva 3280 |
. . . . . 6
⊢ ((2
∈ 𝑁 ∧
∀𝑛 ∈ 𝑁 ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅)) → ((𝑄‘2)𝑀2) ∈ (Base‘𝑅)) |
63 | 57, 37, 62 | sylancr 694 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → ((𝑄‘2)𝑀2) ∈ (Base‘𝑅)) |
64 | 60, 44 | fvmptg 6189 |
. . . . 5
⊢ ((2
∈ 𝑁 ∧ ((𝑄‘2)𝑀2) ∈ (Base‘𝑅)) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘2) = ((𝑄‘2)𝑀2)) |
65 | 57, 63, 64 | sylancr 694 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘2) = ((𝑄‘2)𝑀2)) |
66 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑄 = {〈1, 2〉, 〈2,
1〉} → (𝑄‘2)
= ({〈1, 2〉, 〈2, 1〉}‘2)) |
67 | 49, 8 | fvpr2 6362 |
. . . . . . . 8
⊢ (1 ≠ 2
→ ({〈1, 2〉, 〈2, 1〉}‘2) = 1) |
68 | 48, 67 | ax-mp 5 |
. . . . . . 7
⊢
({〈1, 2〉, 〈2, 1〉}‘2) = 1 |
69 | 66, 68 | syl6eq 2660 |
. . . . . 6
⊢ (𝑄 = {〈1, 2〉, 〈2,
1〉} → (𝑄‘2)
= 1) |
70 | 69 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → (𝑄‘2) = 1) |
71 | 70 | oveq1d 6564 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → ((𝑄‘2)𝑀2) = (1𝑀2)) |
72 | 65, 71 | eqtrd 2644 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘2) = (1𝑀2)) |
73 | 55, 72 | oveq12d 6567 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → (((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘1) · ((𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))‘2)) = ((2𝑀1) · (1𝑀2))) |
74 | 33, 73 | eqtrd 2644 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2,
1〉} ∧ 𝑀 ∈
𝐵) → (𝐺 Σg
(𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2))) |