Step | Hyp | Ref
| Expression |
1 | | mdetdiag.d |
. . . 4
⊢ 𝐷 = (𝑁 maDet 𝑅) |
2 | | mdetdiag.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | | mdetdiag.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
4 | | eqid 2610 |
. . . 4
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁)) |
5 | | eqid 2610 |
. . . 4
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
6 | | eqid 2610 |
. . . 4
⊢
(pmSgn‘𝑁) =
(pmSgn‘𝑁) |
7 | | eqid 2610 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
8 | | eqid 2610 |
. . . 4
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetleib 20212 |
. . 3
⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))))) |
10 | 9 | 3ad2ant3 1077 |
. 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))))) |
11 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑁 = {𝐼} → (SymGrp‘𝑁) = (SymGrp‘{𝐼})) |
12 | 11 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑁 = {𝐼} → (Base‘(SymGrp‘𝑁)) =
(Base‘(SymGrp‘{𝐼}))) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (Base‘(SymGrp‘𝑁)) =
(Base‘(SymGrp‘{𝐼}))) |
14 | 13 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) =
(Base‘(SymGrp‘{𝐼}))) |
15 | | simp2r 1081 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝐼 ∈ 𝑉) |
16 | | eqid 2610 |
. . . . . . . 8
⊢
(SymGrp‘{𝐼}) =
(SymGrp‘{𝐼}) |
17 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(SymGrp‘{𝐼})) = (Base‘(SymGrp‘{𝐼})) |
18 | | eqid 2610 |
. . . . . . . 8
⊢ {𝐼} = {𝐼} |
19 | 16, 17, 18 | symg1bas 17639 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (Base‘(SymGrp‘{𝐼})) = {{〈𝐼, 𝐼〉}}) |
20 | 15, 19 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘{𝐼})) = {{〈𝐼, 𝐼〉}}) |
21 | 14, 20 | eqtrd 2644 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}}) |
22 | 21 | mpteq1d 4666 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))) |
23 | | snex 4835 |
. . . . . 6
⊢
{〈𝐼, 𝐼〉} ∈
V |
24 | 23 | a1i 11 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈𝐼, 𝐼〉} ∈ V) |
25 | | ovex 6577 |
. . . . 5
⊢
((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) ∈ V |
26 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑝 = {〈𝐼, 𝐼〉} → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})) |
27 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ (𝑝 = {〈𝐼, 𝐼〉} → (𝑝‘𝑥) = ({〈𝐼, 𝐼〉}‘𝑥)) |
28 | 27 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑝 = {〈𝐼, 𝐼〉} → ((𝑝‘𝑥)𝑀𝑥) = (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)) |
29 | 28 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝑝 = {〈𝐼, 𝐼〉} → (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)) = (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) |
30 | 29 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑝 = {〈𝐼, 𝐼〉} → ((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) |
31 | 26, 30 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑝 = {〈𝐼, 𝐼〉} → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))) |
32 | 31 | fmptsng 6339 |
. . . . . 6
⊢
(({〈𝐼, 𝐼〉} ∈ V ∧
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) ∈ V) → {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉} = (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))) |
33 | 32 | eqcomd 2616 |
. . . . 5
⊢
(({〈𝐼, 𝐼〉} ∈ V ∧
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) ∈ V) → (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉}) |
34 | 24, 25, 33 | sylancl 693 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉}) |
35 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) |
36 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ {𝑏 ∈
(Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} = {𝑏 ∈
(Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} |
37 | 35, 4, 36, 6 | psgnfn 17744 |
. . . . . . . . . . . 12
⊢
(pmSgn‘𝑁) Fn
{𝑏 ∈
(Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} |
38 | 19 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (Base‘(SymGrp‘{𝐼})) = {{〈𝐼, 𝐼〉}}) |
39 | 13, 38 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}}) |
40 | 39 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}}) |
41 | | rabeq 3166 |
. . . . . . . . . . . . . . 15
⊢
((Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}} → {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} =
{𝑏 ∈ {{〈𝐼, 𝐼〉}} ∣ dom (𝑏 ∖ I ) ∈ Fin}) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} =
{𝑏 ∈ {{〈𝐼, 𝐼〉}} ∣ dom (𝑏 ∖ I ) ∈ Fin}) |
43 | | difeq1 3683 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = {〈𝐼, 𝐼〉} → (𝑏 ∖ I ) = ({〈𝐼, 𝐼〉} ∖ I )) |
44 | 43 | dmeqd 5248 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = {〈𝐼, 𝐼〉} → dom (𝑏 ∖ I ) = dom ({〈𝐼, 𝐼〉} ∖ I )) |
45 | 44 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = {〈𝐼, 𝐼〉} → (dom (𝑏 ∖ I ) ∈ Fin ↔ dom
({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin)) |
46 | 45 | rabsnif 4202 |
. . . . . . . . . . . . . . 15
⊢ {𝑏 ∈ {{〈𝐼, 𝐼〉}} ∣ dom (𝑏 ∖ I ) ∈ Fin} = if(dom
({〈𝐼, 𝐼〉} ∖ I ) ∈ Fin,
{{〈𝐼, 𝐼〉}},
∅) |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {𝑏 ∈ {{〈𝐼, 𝐼〉}} ∣ dom (𝑏 ∖ I ) ∈ Fin} = if(dom
({〈𝐼, 𝐼〉} ∖ I ) ∈ Fin,
{{〈𝐼, 𝐼〉}},
∅)) |
48 | | restidsing 5377 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( I
↾ {𝐼}) = ({𝐼} × {𝐼}) |
49 | | xpsng 6312 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → ({𝐼} × {𝐼}) = {〈𝐼, 𝐼〉}) |
50 | 49 | anidms 675 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ 𝑉 → ({𝐼} × {𝐼}) = {〈𝐼, 𝐼〉}) |
51 | 48, 50 | syl5req 2657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} = ( I ↾ {𝐼})) |
52 | | fnsng 5852 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → {〈𝐼, 𝐼〉} Fn {𝐼}) |
53 | 52 | anidms 675 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} Fn {𝐼}) |
54 | | fnnfpeq0 6349 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈𝐼, 𝐼〉} Fn {𝐼} → (dom ({〈𝐼, 𝐼〉} ∖ I ) = ∅ ↔
{〈𝐼, 𝐼〉} = ( I ↾ {𝐼}))) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ 𝑉 → (dom ({〈𝐼, 𝐼〉} ∖ I ) = ∅ ↔
{〈𝐼, 𝐼〉} = ( I ↾ {𝐼}))) |
56 | 51, 55 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ 𝑉 → dom ({〈𝐼, 𝐼〉} ∖ I ) =
∅) |
57 | | 0fin 8073 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ Fin |
58 | 56, 57 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑉 → dom ({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin) |
59 | 58 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → dom ({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin) |
60 | 59 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → dom ({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin) |
61 | 60 | iftrued 4044 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → if(dom ({〈𝐼, 𝐼〉} ∖ I ) ∈ Fin,
{{〈𝐼, 𝐼〉}}, ∅) =
{{〈𝐼, 𝐼〉}}) |
62 | 42, 47, 61 | 3eqtrrd 2649 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {{〈𝐼, 𝐼〉}} = {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈
Fin}) |
63 | 62 | fneq2d 5896 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘𝑁) Fn {{〈𝐼, 𝐼〉}} ↔ (pmSgn‘𝑁) Fn {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈
Fin})) |
64 | 37, 63 | mpbiri 247 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (pmSgn‘𝑁) Fn {{〈𝐼, 𝐼〉}}) |
65 | 23 | snid 4155 |
. . . . . . . . . . 11
⊢
{〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}} |
66 | | fvco2 6183 |
. . . . . . . . . . 11
⊢
(((pmSgn‘𝑁) Fn
{{〈𝐼, 𝐼〉}} ∧ {〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}}) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉}) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}))) |
67 | 64, 65, 66 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉}) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}))) |
68 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = {𝐼} → (pmSgn‘𝑁) = (pmSgn‘{𝐼})) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (pmSgn‘𝑁) = (pmSgn‘{𝐼})) |
70 | 69 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (pmSgn‘𝑁) = (pmSgn‘{𝐼})) |
71 | 70 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}) = ((pmSgn‘{𝐼})‘{〈𝐼, 𝐼〉})) |
72 | | snidg 4153 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈𝐼, 𝐼〉} ∈ V →
{〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}}) |
73 | 23, 72 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}}) |
74 | 73, 19 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼}))) |
75 | 74 | ancli 572 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ 𝑉 → (𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼})))) |
76 | 75 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼})))) |
77 | 76 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼})))) |
78 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(pmSgn‘{𝐼}) =
(pmSgn‘{𝐼}) |
79 | 18, 16, 17, 78 | psgnsn 17763 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼}))) → ((pmSgn‘{𝐼})‘{〈𝐼, 𝐼〉}) = 1) |
80 | 77, 79 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘{𝐼})‘{〈𝐼, 𝐼〉}) = 1) |
81 | 71, 80 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}) = 1) |
82 | 81 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉})) = ((ℤRHom‘𝑅)‘1)) |
83 | | crngring 18381 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
84 | 83 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
85 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) |
86 | 5, 85 | zrh1 19680 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
((ℤRHom‘𝑅)‘1) = (1r‘𝑅)) |
87 | 84, 86 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘1) =
(1r‘𝑅)) |
88 | 67, 82, 87 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉}) = (1r‘𝑅)) |
89 | | simp2l 1080 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑁 = {𝐼}) |
90 | 89 | mpteq1d 4666 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)) = (𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) |
91 | 90 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) |
92 | 8 | ringmgp 18376 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
93 | 83, 92 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
Mnd) |
94 | 93 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝑅) ∈ Mnd) |
95 | | snidg 4153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ {𝐼}) |
96 | 95 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → 𝐼 ∈ {𝐼}) |
97 | | eleq2 2677 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = {𝐼} → (𝐼 ∈ 𝑁 ↔ 𝐼 ∈ {𝐼})) |
98 | 97 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (𝐼 ∈ 𝑁 ↔ 𝐼 ∈ {𝐼})) |
99 | 96, 98 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → 𝐼 ∈ 𝑁) |
100 | 3 | eleq2i 2680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘𝐴)) |
101 | 100 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (Base‘𝐴)) |
102 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → 𝐼 ∈ 𝑁) |
103 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → 𝑀 ∈ (Base‘𝐴)) |
104 | 102, 102,
103 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) |
105 | 99, 101, 104 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) |
106 | 105 | 3adant1 1072 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) |
107 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑅) =
(Base‘𝑅) |
108 | 2, 107 | matecl 20050 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) |
109 | 106, 108 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) |
110 | 8, 107 | mgpbas 18318 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
111 | 109, 110 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼𝑀𝐼) ∈ (Base‘(mulGrp‘𝑅))) |
112 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅)) |
113 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐼 → ({〈𝐼, 𝐼〉}‘𝑥) = ({〈𝐼, 𝐼〉}‘𝐼)) |
114 | | eqvisset 3184 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐼 → 𝐼 ∈ V) |
115 | | fvsng 6352 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ V ∧ 𝐼 ∈ V) → ({〈𝐼, 𝐼〉}‘𝐼) = 𝐼) |
116 | 114, 114,
115 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐼 → ({〈𝐼, 𝐼〉}‘𝐼) = 𝐼) |
117 | 113, 116 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐼 → ({〈𝐼, 𝐼〉}‘𝑥) = 𝐼) |
118 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐼 → 𝑥 = 𝐼) |
119 | 117, 118 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐼 → (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥) = (𝐼𝑀𝐼)) |
120 | 112, 119 | gsumsn 18177 |
. . . . . . . . . . 11
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑉 ∧ (𝐼𝑀𝐼) ∈ (Base‘(mulGrp‘𝑅))) → ((mulGrp‘𝑅) Σg
(𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼)) |
121 | 94, 15, 111, 120 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼)) |
122 | 91, 121 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼)) |
123 | 88, 122 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) = ((1r‘𝑅)(.r‘𝑅)(𝐼𝑀𝐼))) |
124 | 99 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝐼 ∈ 𝑁) |
125 | 101 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ (Base‘𝐴)) |
126 | 124, 124,
125, 108 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) |
127 | 107, 7, 85 | ringlidm 18394 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝐼𝑀𝐼) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)(𝐼𝑀𝐼)) = (𝐼𝑀𝐼)) |
128 | 84, 126, 127 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((1r‘𝑅)(.r‘𝑅)(𝐼𝑀𝐼)) = (𝐼𝑀𝐼)) |
129 | 123, 128 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) = (𝐼𝑀𝐼)) |
130 | 129 | opeq2d 4347 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉 = 〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉) |
131 | 130 | sneqd 4137 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉} = {〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉}) |
132 | | ovex 6577 |
. . . . . 6
⊢ (𝐼𝑀𝐼) ∈ V |
133 | | eqidd 2611 |
. . . . . . 7
⊢ (𝑦 = {〈𝐼, 𝐼〉} → (𝐼𝑀𝐼) = (𝐼𝑀𝐼)) |
134 | 133 | fmptsng 6339 |
. . . . . 6
⊢
(({〈𝐼, 𝐼〉} ∈ V ∧ (𝐼𝑀𝐼) ∈ V) → {〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉} = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) |
135 | 24, 132, 134 | sylancl 693 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉} = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) |
136 | 131, 135 | eqtrd 2644 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉} = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) |
137 | 22, 34, 136 | 3eqtrd 2648 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) |
138 | 137 | oveq2d 6565 |
. 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))) = (𝑅 Σg (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼)))) |
139 | | ringmnd 18379 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
140 | 83, 139 | syl 17 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Mnd) |
141 | 140 | 3ad2ant1 1075 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Mnd) |
142 | 107, 133 | gsumsn 18177 |
. . 3
⊢ ((𝑅 ∈ Mnd ∧ {〈𝐼, 𝐼〉} ∈ V ∧ (𝐼𝑀𝐼) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) = (𝐼𝑀𝐼)) |
143 | 141, 24, 126, 142 | syl3anc 1318 |
. 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) = (𝐼𝑀𝐼)) |
144 | 10, 138, 143 | 3eqtrd 2648 |
1
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝐼𝑀𝐼)) |