Step | Hyp | Ref
| Expression |
1 | | mdetdiag.d |
. . . 4
⊢ 𝐷 = (𝑁 maDet 𝑅) |
2 | | mdetdiag.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | | mdetdiag.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
4 | | eqid 2737 |
. . . 4
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁)) |
5 | | eqid 2737 |
. . . 4
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
6 | | eqid 2737 |
. . . 4
⊢
(pmSgn‘𝑁) =
(pmSgn‘𝑁) |
7 | | eqid 2737 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
8 | | eqid 2737 |
. . . 4
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetleib 21484 |
. . 3
⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))))) |
10 | 9 | 3ad2ant3 1137 |
. 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))))) |
11 | | 2fveq3 6722 |
. . . . . . . 8
⊢ (𝑁 = {𝐼} → (Base‘(SymGrp‘𝑁)) =
(Base‘(SymGrp‘{𝐼}))) |
12 | 11 | adantr 484 |
. . . . . . 7
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (Base‘(SymGrp‘𝑁)) =
(Base‘(SymGrp‘{𝐼}))) |
13 | 12 | 3ad2ant2 1136 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) =
(Base‘(SymGrp‘{𝐼}))) |
14 | | simp2r 1202 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝐼 ∈ 𝑉) |
15 | | eqid 2737 |
. . . . . . . 8
⊢
(SymGrp‘{𝐼}) =
(SymGrp‘{𝐼}) |
16 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(SymGrp‘{𝐼})) = (Base‘(SymGrp‘{𝐼})) |
17 | | eqid 2737 |
. . . . . . . 8
⊢ {𝐼} = {𝐼} |
18 | 15, 16, 17 | symg1bas 18783 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (Base‘(SymGrp‘{𝐼})) = {{〈𝐼, 𝐼〉}}) |
19 | 14, 18 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘{𝐼})) = {{〈𝐼, 𝐼〉}}) |
20 | 13, 19 | eqtrd 2777 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}}) |
21 | 20 | mpteq1d 5144 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))) |
22 | | snex 5324 |
. . . . . 6
⊢
{〈𝐼, 𝐼〉} ∈
V |
23 | 22 | a1i 11 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈𝐼, 𝐼〉} ∈ V) |
24 | | ovex 7246 |
. . . . 5
⊢
((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) ∈ V |
25 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑝 = {〈𝐼, 𝐼〉} → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})) |
26 | | fveq1 6716 |
. . . . . . . . . . 11
⊢ (𝑝 = {〈𝐼, 𝐼〉} → (𝑝‘𝑥) = ({〈𝐼, 𝐼〉}‘𝑥)) |
27 | 26 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (𝑝 = {〈𝐼, 𝐼〉} → ((𝑝‘𝑥)𝑀𝑥) = (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)) |
28 | 27 | mpteq2dv 5151 |
. . . . . . . . 9
⊢ (𝑝 = {〈𝐼, 𝐼〉} → (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)) = (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) |
29 | 28 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝑝 = {〈𝐼, 𝐼〉} → ((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) |
30 | 25, 29 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑝 = {〈𝐼, 𝐼〉} → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))) |
31 | 30 | fmptsng 6983 |
. . . . . 6
⊢
(({〈𝐼, 𝐼〉} ∈ V ∧
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) ∈ V) → {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉} = (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))) |
32 | 31 | eqcomd 2743 |
. . . . 5
⊢
(({〈𝐼, 𝐼〉} ∈ V ∧
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) ∈ V) → (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉}) |
33 | 23, 24, 32 | sylancl 589 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉}) |
34 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
35 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ {𝑏 ∈
(Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} = {𝑏 ∈
(Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} |
36 | 34, 4, 35, 6 | psgnfn 18893 |
. . . . . . . . . . . 12
⊢
(pmSgn‘𝑁) Fn
{𝑏 ∈
(Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} |
37 | 18 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (Base‘(SymGrp‘{𝐼})) = {{〈𝐼, 𝐼〉}}) |
38 | 12, 37 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}}) |
39 | 38 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}}) |
40 | | rabeq 3394 |
. . . . . . . . . . . . . . 15
⊢
((Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}} → {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} =
{𝑏 ∈ {{〈𝐼, 𝐼〉}} ∣ dom (𝑏 ∖ I ) ∈ Fin}) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} =
{𝑏 ∈ {{〈𝐼, 𝐼〉}} ∣ dom (𝑏 ∖ I ) ∈ Fin}) |
42 | | difeq1 4030 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = {〈𝐼, 𝐼〉} → (𝑏 ∖ I ) = ({〈𝐼, 𝐼〉} ∖ I )) |
43 | 42 | dmeqd 5774 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = {〈𝐼, 𝐼〉} → dom (𝑏 ∖ I ) = dom ({〈𝐼, 𝐼〉} ∖ I )) |
44 | 43 | eleq1d 2822 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = {〈𝐼, 𝐼〉} → (dom (𝑏 ∖ I ) ∈ Fin ↔ dom
({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin)) |
45 | 44 | rabsnif 4639 |
. . . . . . . . . . . . . . 15
⊢ {𝑏 ∈ {{〈𝐼, 𝐼〉}} ∣ dom (𝑏 ∖ I ) ∈ Fin} = if(dom
({〈𝐼, 𝐼〉} ∖ I ) ∈ Fin,
{{〈𝐼, 𝐼〉}},
∅) |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {𝑏 ∈ {{〈𝐼, 𝐼〉}} ∣ dom (𝑏 ∖ I ) ∈ Fin} = if(dom
({〈𝐼, 𝐼〉} ∖ I ) ∈ Fin,
{{〈𝐼, 𝐼〉}},
∅)) |
47 | | restidsing 5922 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( I
↾ {𝐼}) = ({𝐼} × {𝐼}) |
48 | | xpsng 6954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → ({𝐼} × {𝐼}) = {〈𝐼, 𝐼〉}) |
49 | 48 | anidms 570 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ 𝑉 → ({𝐼} × {𝐼}) = {〈𝐼, 𝐼〉}) |
50 | 47, 49 | eqtr2id 2791 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} = ( I ↾ {𝐼})) |
51 | | fnsng 6432 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → {〈𝐼, 𝐼〉} Fn {𝐼}) |
52 | 51 | anidms 570 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} Fn {𝐼}) |
53 | | fnnfpeq0 6993 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈𝐼, 𝐼〉} Fn {𝐼} → (dom ({〈𝐼, 𝐼〉} ∖ I ) = ∅ ↔
{〈𝐼, 𝐼〉} = ( I ↾ {𝐼}))) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ 𝑉 → (dom ({〈𝐼, 𝐼〉} ∖ I ) = ∅ ↔
{〈𝐼, 𝐼〉} = ( I ↾ {𝐼}))) |
55 | 50, 54 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ 𝑉 → dom ({〈𝐼, 𝐼〉} ∖ I ) =
∅) |
56 | | 0fin 8849 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ Fin |
57 | 55, 56 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑉 → dom ({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin) |
58 | 57 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → dom ({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin) |
59 | 58 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → dom ({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin) |
60 | 59 | iftrued 4447 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → if(dom ({〈𝐼, 𝐼〉} ∖ I ) ∈ Fin,
{{〈𝐼, 𝐼〉}}, ∅) =
{{〈𝐼, 𝐼〉}}) |
61 | 41, 46, 60 | 3eqtrrd 2782 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {{〈𝐼, 𝐼〉}} = {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈
Fin}) |
62 | 61 | fneq2d 6473 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘𝑁) Fn {{〈𝐼, 𝐼〉}} ↔ (pmSgn‘𝑁) Fn {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈
Fin})) |
63 | 36, 62 | mpbiri 261 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (pmSgn‘𝑁) Fn {{〈𝐼, 𝐼〉}}) |
64 | 22 | snid 4577 |
. . . . . . . . . . 11
⊢
{〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}} |
65 | | fvco2 6808 |
. . . . . . . . . . 11
⊢
(((pmSgn‘𝑁) Fn
{{〈𝐼, 𝐼〉}} ∧ {〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}}) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉}) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}))) |
66 | 63, 64, 65 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉}) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}))) |
67 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = {𝐼} → (pmSgn‘𝑁) = (pmSgn‘{𝐼})) |
68 | 67 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (pmSgn‘𝑁) = (pmSgn‘{𝐼})) |
69 | 68 | 3ad2ant2 1136 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (pmSgn‘𝑁) = (pmSgn‘{𝐼})) |
70 | 69 | fveq1d 6719 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}) = ((pmSgn‘{𝐼})‘{〈𝐼, 𝐼〉})) |
71 | | snidg 4575 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈𝐼, 𝐼〉} ∈ V →
{〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}}) |
72 | 22, 71 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}}) |
73 | 72, 18 | eleqtrrd 2841 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼}))) |
74 | 73 | ancli 552 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ 𝑉 → (𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼})))) |
75 | 74 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼})))) |
76 | 75 | 3ad2ant2 1136 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼})))) |
77 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(pmSgn‘{𝐼}) =
(pmSgn‘{𝐼}) |
78 | 17, 15, 16, 77 | psgnsn 18912 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼}))) → ((pmSgn‘{𝐼})‘{〈𝐼, 𝐼〉}) = 1) |
79 | 76, 78 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘{𝐼})‘{〈𝐼, 𝐼〉}) = 1) |
80 | 70, 79 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}) = 1) |
81 | 80 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉})) = ((ℤRHom‘𝑅)‘1)) |
82 | | crngring 19574 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
83 | 82 | 3ad2ant1 1135 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
84 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) |
85 | 5, 84 | zrh1 20479 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
((ℤRHom‘𝑅)‘1) = (1r‘𝑅)) |
86 | 83, 85 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘1) =
(1r‘𝑅)) |
87 | 66, 81, 86 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉}) = (1r‘𝑅)) |
88 | | simp2l 1201 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑁 = {𝐼}) |
89 | 88 | mpteq1d 5144 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)) = (𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) |
90 | 89 | oveq2d 7229 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) |
91 | 8 | ringmgp 19568 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
92 | 82, 91 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
Mnd) |
93 | 92 | 3ad2ant1 1135 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝑅) ∈ Mnd) |
94 | | snidg 4575 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ {𝐼}) |
95 | 94 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → 𝐼 ∈ {𝐼}) |
96 | | eleq2 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = {𝐼} → (𝐼 ∈ 𝑁 ↔ 𝐼 ∈ {𝐼})) |
97 | 96 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (𝐼 ∈ 𝑁 ↔ 𝐼 ∈ {𝐼})) |
98 | 95, 97 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → 𝐼 ∈ 𝑁) |
99 | 3 | eleq2i 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘𝐴)) |
100 | 99 | biimpi 219 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (Base‘𝐴)) |
101 | | simpl 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → 𝐼 ∈ 𝑁) |
102 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → 𝑀 ∈ (Base‘𝐴)) |
103 | 101, 101,
102 | 3jca 1130 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) |
104 | 98, 100, 103 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) |
105 | 104 | 3adant1 1132 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) |
106 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑅) =
(Base‘𝑅) |
107 | 2, 106 | matecl 21322 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) |
108 | 105, 107 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) |
109 | 8, 106 | mgpbas 19510 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
110 | 108, 109 | eleqtrdi 2848 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼𝑀𝐼) ∈ (Base‘(mulGrp‘𝑅))) |
111 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅)) |
112 | | fveq2 6717 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐼 → ({〈𝐼, 𝐼〉}‘𝑥) = ({〈𝐼, 𝐼〉}‘𝐼)) |
113 | | eqvisset 3425 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐼 → 𝐼 ∈ V) |
114 | | fvsng 6995 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ V ∧ 𝐼 ∈ V) → ({〈𝐼, 𝐼〉}‘𝐼) = 𝐼) |
115 | 113, 113,
114 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐼 → ({〈𝐼, 𝐼〉}‘𝐼) = 𝐼) |
116 | 112, 115 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐼 → ({〈𝐼, 𝐼〉}‘𝑥) = 𝐼) |
117 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐼 → 𝑥 = 𝐼) |
118 | 116, 117 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐼 → (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥) = (𝐼𝑀𝐼)) |
119 | 111, 118 | gsumsn 19339 |
. . . . . . . . . . 11
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑉 ∧ (𝐼𝑀𝐼) ∈ (Base‘(mulGrp‘𝑅))) → ((mulGrp‘𝑅) Σg
(𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼)) |
120 | 93, 14, 110, 119 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼)) |
121 | 90, 120 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼)) |
122 | 87, 121 | oveq12d 7231 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) = ((1r‘𝑅)(.r‘𝑅)(𝐼𝑀𝐼))) |
123 | 98 | 3ad2ant2 1136 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝐼 ∈ 𝑁) |
124 | 100 | 3ad2ant3 1137 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ (Base‘𝐴)) |
125 | 123, 123,
124, 107 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) |
126 | 106, 7, 84 | ringlidm 19589 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝐼𝑀𝐼) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)(𝐼𝑀𝐼)) = (𝐼𝑀𝐼)) |
127 | 83, 125, 126 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((1r‘𝑅)(.r‘𝑅)(𝐼𝑀𝐼)) = (𝐼𝑀𝐼)) |
128 | 122, 127 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) = (𝐼𝑀𝐼)) |
129 | 128 | opeq2d 4791 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉 = 〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉) |
130 | 129 | sneqd 4553 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉} = {〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉}) |
131 | | ovex 7246 |
. . . . . 6
⊢ (𝐼𝑀𝐼) ∈ V |
132 | | eqidd 2738 |
. . . . . . 7
⊢ (𝑦 = {〈𝐼, 𝐼〉} → (𝐼𝑀𝐼) = (𝐼𝑀𝐼)) |
133 | 132 | fmptsng 6983 |
. . . . . 6
⊢
(({〈𝐼, 𝐼〉} ∈ V ∧ (𝐼𝑀𝐼) ∈ V) → {〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉} = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) |
134 | 23, 131, 133 | sylancl 589 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉} = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) |
135 | 130, 134 | eqtrd 2777 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉} = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) |
136 | 21, 33, 135 | 3eqtrd 2781 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) |
137 | 136 | oveq2d 7229 |
. 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))) = (𝑅 Σg (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼)))) |
138 | | ringmnd 19572 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
139 | 82, 138 | syl 17 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Mnd) |
140 | 139 | 3ad2ant1 1135 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Mnd) |
141 | 106, 132 | gsumsn 19339 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ {〈𝐼, 𝐼〉} ∈ V ∧ (𝐼𝑀𝐼) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) = (𝐼𝑀𝐼)) |
142 | 140, 23, 125, 141 | syl3anc 1373 |
. 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) = (𝐼𝑀𝐼)) |
143 | 10, 137, 142 | 3eqtrd 2781 |
1
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝐼𝑀𝐼)) |