| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mdetdiag.d | . . . 4
⊢ 𝐷 = (𝑁 maDet 𝑅) | 
| 2 |  | mdetdiag.a | . . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 3 |  | mdetdiag.b | . . . 4
⊢ 𝐵 = (Base‘𝐴) | 
| 4 |  | eqid 2736 | . . . 4
⊢
(Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁)) | 
| 5 |  | eqid 2736 | . . . 4
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) | 
| 6 |  | eqid 2736 | . . . 4
⊢
(pmSgn‘𝑁) =
(pmSgn‘𝑁) | 
| 7 |  | eqid 2736 | . . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 8 |  | eqid 2736 | . . . 4
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) | 
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | mdetleib 22594 | . . 3
⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))))) | 
| 10 | 9 | 3ad2ant3 1135 | . 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))))) | 
| 11 |  | 2fveq3 6910 | . . . . . . . 8
⊢ (𝑁 = {𝐼} → (Base‘(SymGrp‘𝑁)) =
(Base‘(SymGrp‘{𝐼}))) | 
| 12 | 11 | adantr 480 | . . . . . . 7
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (Base‘(SymGrp‘𝑁)) =
(Base‘(SymGrp‘{𝐼}))) | 
| 13 | 12 | 3ad2ant2 1134 | . . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) =
(Base‘(SymGrp‘{𝐼}))) | 
| 14 |  | simp2r 1200 | . . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝐼 ∈ 𝑉) | 
| 15 |  | eqid 2736 | . . . . . . . 8
⊢
(SymGrp‘{𝐼}) =
(SymGrp‘{𝐼}) | 
| 16 |  | eqid 2736 | . . . . . . . 8
⊢
(Base‘(SymGrp‘{𝐼})) = (Base‘(SymGrp‘{𝐼})) | 
| 17 |  | eqid 2736 | . . . . . . . 8
⊢ {𝐼} = {𝐼} | 
| 18 | 15, 16, 17 | symg1bas 19409 | . . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (Base‘(SymGrp‘{𝐼})) = {{〈𝐼, 𝐼〉}}) | 
| 19 | 14, 18 | syl 17 | . . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘{𝐼})) = {{〈𝐼, 𝐼〉}}) | 
| 20 | 13, 19 | eqtrd 2776 | . . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}}) | 
| 21 | 20 | mpteq1d 5236 | . . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))) | 
| 22 |  | snex 5435 | . . . . . 6
⊢
{〈𝐼, 𝐼〉} ∈
V | 
| 23 | 22 | a1i 11 | . . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈𝐼, 𝐼〉} ∈ V) | 
| 24 |  | ovex 7465 | . . . . 5
⊢
((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) ∈ V | 
| 25 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑝 = {〈𝐼, 𝐼〉} → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})) | 
| 26 |  | fveq1 6904 | . . . . . . . . . . 11
⊢ (𝑝 = {〈𝐼, 𝐼〉} → (𝑝‘𝑥) = ({〈𝐼, 𝐼〉}‘𝑥)) | 
| 27 | 26 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑝 = {〈𝐼, 𝐼〉} → ((𝑝‘𝑥)𝑀𝑥) = (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)) | 
| 28 | 27 | mpteq2dv 5243 | . . . . . . . . 9
⊢ (𝑝 = {〈𝐼, 𝐼〉} → (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)) = (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) | 
| 29 | 28 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑝 = {〈𝐼, 𝐼〉} → ((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) | 
| 30 | 25, 29 | oveq12d 7450 | . . . . . . 7
⊢ (𝑝 = {〈𝐼, 𝐼〉} → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))) | 
| 31 | 30 | fmptsng 7189 | . . . . . 6
⊢
(({〈𝐼, 𝐼〉} ∈ V ∧
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) ∈ V) → {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉} = (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))) | 
| 32 | 31 | eqcomd 2742 | . . . . 5
⊢
(({〈𝐼, 𝐼〉} ∈ V ∧
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) ∈ V) → (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉}) | 
| 33 | 23, 24, 32 | sylancl 586 | . . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑝 ∈ {{〈𝐼, 𝐼〉}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉}) | 
| 34 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) | 
| 35 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ {𝑏 ∈
(Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} = {𝑏 ∈
(Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} | 
| 36 | 34, 4, 35, 6 | psgnfn 19520 | . . . . . . . . . . . 12
⊢
(pmSgn‘𝑁) Fn
{𝑏 ∈
(Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} | 
| 37 | 18 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (Base‘(SymGrp‘{𝐼})) = {{〈𝐼, 𝐼〉}}) | 
| 38 | 12, 37 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}}) | 
| 39 | 38 | 3ad2ant2 1134 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) = {{〈𝐼, 𝐼〉}}) | 
| 40 |  | rabeq 3450 | . . . . . . . . . . . . . . 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 4118 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = {〈𝐼, 𝐼〉} → (𝑏 ∖ I ) = ({〈𝐼, 𝐼〉} ∖ I )) | 
| 43 | 42 | dmeqd 5915 | . . . . . . . . . . . . . . . . 17
⊢ (𝑏 = {〈𝐼, 𝐼〉} → dom (𝑏 ∖ I ) = dom ({〈𝐼, 𝐼〉} ∖ I )) | 
| 44 | 43 | eleq1d 2825 | . . . . . . . . . . . . . . . 16
⊢ (𝑏 = {〈𝐼, 𝐼〉} → (dom (𝑏 ∖ I ) ∈ Fin ↔ dom
({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin)) | 
| 45 | 44 | rabsnif 4722 | . . . . . . . . . . . . . . 15
⊢ {𝑏 ∈ {{〈𝐼, 𝐼〉}} ∣ dom (𝑏 ∖ I ) ∈ Fin} = if(dom
({〈𝐼, 𝐼〉} ∖ I ) ∈ Fin,
{{〈𝐼, 𝐼〉}},
∅) | 
| 46 | 45 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {𝑏 ∈ {{〈𝐼, 𝐼〉}} ∣ dom (𝑏 ∖ I ) ∈ Fin} = if(dom
({〈𝐼, 𝐼〉} ∖ I ) ∈ Fin,
{{〈𝐼, 𝐼〉}},
∅)) | 
| 47 |  | restidsing 6070 | . . . . . . . . . . . . . . . . . . . 20
⊢ ( I
↾ {𝐼}) = ({𝐼} × {𝐼}) | 
| 48 |  | xpsng 7158 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → ({𝐼} × {𝐼}) = {〈𝐼, 𝐼〉}) | 
| 49 | 48 | anidms 566 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ 𝑉 → ({𝐼} × {𝐼}) = {〈𝐼, 𝐼〉}) | 
| 50 | 47, 49 | eqtr2id 2789 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} = ( I ↾ {𝐼})) | 
| 51 |  | fnsng 6617 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → {〈𝐼, 𝐼〉} Fn {𝐼}) | 
| 52 | 51 | anidms 566 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} Fn {𝐼}) | 
| 53 |  | fnnfpeq0 7199 | . . . . . . . . . . . . . . . . . . . 20
⊢
({〈𝐼, 𝐼〉} Fn {𝐼} → (dom ({〈𝐼, 𝐼〉} ∖ I ) = ∅ ↔
{〈𝐼, 𝐼〉} = ( I ↾ {𝐼}))) | 
| 54 | 52, 53 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ 𝑉 → (dom ({〈𝐼, 𝐼〉} ∖ I ) = ∅ ↔
{〈𝐼, 𝐼〉} = ( I ↾ {𝐼}))) | 
| 55 | 50, 54 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ 𝑉 → dom ({〈𝐼, 𝐼〉} ∖ I ) =
∅) | 
| 56 |  | 0fi 9083 | . . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ Fin | 
| 57 | 55, 56 | eqeltrdi 2848 | . . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑉 → dom ({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin) | 
| 58 | 57 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → dom ({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin) | 
| 59 | 58 | 3ad2ant2 1134 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → dom ({〈𝐼, 𝐼〉} ∖ I ) ∈
Fin) | 
| 60 | 59 | iftrued 4532 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → if(dom ({〈𝐼, 𝐼〉} ∖ I ) ∈ Fin,
{{〈𝐼, 𝐼〉}}, ∅) =
{{〈𝐼, 𝐼〉}}) | 
| 61 | 41, 46, 60 | 3eqtrrd 2781 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {{〈𝐼, 𝐼〉}} = {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈
Fin}) | 
| 62 | 61 | fneq2d 6661 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘𝑁) Fn {{〈𝐼, 𝐼〉}} ↔ (pmSgn‘𝑁) Fn {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈
Fin})) | 
| 63 | 36, 62 | mpbiri 258 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (pmSgn‘𝑁) Fn {{〈𝐼, 𝐼〉}}) | 
| 64 | 22 | snid 4661 | . . . . . . . . . . 11
⊢
{〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}} | 
| 65 |  | fvco2 7005 | . . . . . . . . . . 11
⊢
(((pmSgn‘𝑁) Fn
{{〈𝐼, 𝐼〉}} ∧ {〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}}) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉}) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}))) | 
| 66 | 63, 64, 65 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉}) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}))) | 
| 67 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑁 = {𝐼} → (pmSgn‘𝑁) = (pmSgn‘{𝐼})) | 
| 68 | 67 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (pmSgn‘𝑁) = (pmSgn‘{𝐼})) | 
| 69 | 68 | 3ad2ant2 1134 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (pmSgn‘𝑁) = (pmSgn‘{𝐼})) | 
| 70 | 69 | fveq1d 6907 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}) = ((pmSgn‘{𝐼})‘{〈𝐼, 𝐼〉})) | 
| 71 |  | snidg 4659 | . . . . . . . . . . . . . . . . . 18
⊢
({〈𝐼, 𝐼〉} ∈ V →
{〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}}) | 
| 72 | 22, 71 | mp1i 13 | . . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} ∈ {{〈𝐼, 𝐼〉}}) | 
| 73 | 72, 18 | eleqtrrd 2843 | . . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ 𝑉 → {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼}))) | 
| 74 | 73 | ancli 548 | . . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ 𝑉 → (𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼})))) | 
| 75 | 74 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼})))) | 
| 76 | 75 | 3ad2ant2 1134 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼})))) | 
| 77 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(pmSgn‘{𝐼}) =
(pmSgn‘{𝐼}) | 
| 78 | 17, 15, 16, 77 | psgnsn 19539 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ {〈𝐼, 𝐼〉} ∈
(Base‘(SymGrp‘{𝐼}))) → ((pmSgn‘{𝐼})‘{〈𝐼, 𝐼〉}) = 1) | 
| 79 | 76, 78 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘{𝐼})‘{〈𝐼, 𝐼〉}) = 1) | 
| 80 | 70, 79 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉}) = 1) | 
| 81 | 80 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{〈𝐼, 𝐼〉})) = ((ℤRHom‘𝑅)‘1)) | 
| 82 |  | crngring 20243 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 83 | 82 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) | 
| 84 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 85 | 5, 84 | zrh1 21524 | . . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
((ℤRHom‘𝑅)‘1) = (1r‘𝑅)) | 
| 86 | 83, 85 | syl 17 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((ℤRHom‘𝑅)‘1) =
(1r‘𝑅)) | 
| 87 | 66, 81, 86 | 3eqtrd 2780 | . . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉}) = (1r‘𝑅)) | 
| 88 |  | simp2l 1199 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑁 = {𝐼}) | 
| 89 | 88 | mpteq1d 5236 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)) = (𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) | 
| 90 | 89 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) | 
| 91 | 8 | ringmgp 20237 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) | 
| 92 | 82, 91 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
Mnd) | 
| 93 | 92 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝑅) ∈ Mnd) | 
| 94 |  | snidg 4659 | . . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ {𝐼}) | 
| 95 | 94 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → 𝐼 ∈ {𝐼}) | 
| 96 |  | eleq2 2829 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁 = {𝐼} → (𝐼 ∈ 𝑁 ↔ 𝐼 ∈ {𝐼})) | 
| 97 | 96 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → (𝐼 ∈ 𝑁 ↔ 𝐼 ∈ {𝐼})) | 
| 98 | 95, 97 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → 𝐼 ∈ 𝑁) | 
| 99 | 3 | eleq2i 2832 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘𝐴)) | 
| 100 | 99 | biimpi 216 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (Base‘𝐴)) | 
| 101 |  | simpl 482 | . . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → 𝐼 ∈ 𝑁) | 
| 102 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → 𝑀 ∈ (Base‘𝐴)) | 
| 103 | 101, 101,
102 | 3jca 1128 | . . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) | 
| 104 | 98, 100, 103 | syl2an 596 | . . . . . . . . . . . . . 14
⊢ (((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) | 
| 105 | 104 | 3adant1 1130 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴))) | 
| 106 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 107 | 2, 106 | matecl 22432 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) | 
| 108 | 105, 107 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) | 
| 109 | 8, 106 | mgpbas 20143 | . . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) | 
| 110 | 108, 109 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼𝑀𝐼) ∈ (Base‘(mulGrp‘𝑅))) | 
| 111 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅)) | 
| 112 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐼 → ({〈𝐼, 𝐼〉}‘𝑥) = ({〈𝐼, 𝐼〉}‘𝐼)) | 
| 113 |  | eqvisset 3499 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐼 → 𝐼 ∈ V) | 
| 114 |  | fvsng 7201 | . . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ V ∧ 𝐼 ∈ V) → ({〈𝐼, 𝐼〉}‘𝐼) = 𝐼) | 
| 115 | 113, 113,
114 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐼 → ({〈𝐼, 𝐼〉}‘𝐼) = 𝐼) | 
| 116 | 112, 115 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝐼 → ({〈𝐼, 𝐼〉}‘𝑥) = 𝐼) | 
| 117 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝐼 → 𝑥 = 𝐼) | 
| 118 | 116, 117 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝐼 → (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥) = (𝐼𝑀𝐼)) | 
| 119 | 111, 118 | gsumsn 19973 | . . . . . . . . . . 11
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝐼 ∈
𝑉 ∧ (𝐼𝑀𝐼) ∈ (Base‘(mulGrp‘𝑅))) → ((mulGrp‘𝑅) Σg
(𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼)) | 
| 120 | 93, 14, 110, 119 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑥 ∈ {𝐼} ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼)) | 
| 121 | 90, 120 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼)) | 
| 122 | 87, 121 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) = ((1r‘𝑅)(.r‘𝑅)(𝐼𝑀𝐼))) | 
| 123 | 98 | 3ad2ant2 1134 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝐼 ∈ 𝑁) | 
| 124 | 100 | 3ad2ant3 1135 | . . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ (Base‘𝐴)) | 
| 125 | 123, 123,
124, 107 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) | 
| 126 | 106, 7, 84 | ringlidm 20267 | . . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝐼𝑀𝐼) ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)(𝐼𝑀𝐼)) = (𝐼𝑀𝐼)) | 
| 127 | 83, 125, 126 | syl2anc 584 | . . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((1r‘𝑅)(.r‘𝑅)(𝐼𝑀𝐼)) = (𝐼𝑀𝐼)) | 
| 128 | 122, 127 | eqtrd 2776 | . . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥)))) = (𝐼𝑀𝐼)) | 
| 129 | 128 | opeq2d 4879 | . . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉 = 〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉) | 
| 130 | 129 | sneqd 4637 | . . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉} = {〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉}) | 
| 131 |  | ovex 7465 | . . . . . 6
⊢ (𝐼𝑀𝐼) ∈ V | 
| 132 |  | eqidd 2737 | . . . . . . 7
⊢ (𝑦 = {〈𝐼, 𝐼〉} → (𝐼𝑀𝐼) = (𝐼𝑀𝐼)) | 
| 133 | 132 | fmptsng 7189 | . . . . . 6
⊢
(({〈𝐼, 𝐼〉} ∈ V ∧ (𝐼𝑀𝐼) ∈ V) → {〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉} = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) | 
| 134 | 23, 131, 133 | sylancl 586 | . . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈{〈𝐼, 𝐼〉}, (𝐼𝑀𝐼)〉} = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) | 
| 135 | 130, 134 | eqtrd 2776 | . . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → {〈{〈𝐼, 𝐼〉}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{〈𝐼, 𝐼〉})(.r‘𝑅)((mulGrp‘𝑅) Σg
(𝑥 ∈ 𝑁 ↦ (({〈𝐼, 𝐼〉}‘𝑥)𝑀𝑥))))〉} = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) | 
| 136 | 21, 33, 135 | 3eqtrd 2780 | . . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦
((((ℤRHom‘𝑅)
∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))) = (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) | 
| 137 | 136 | oveq2d 7448 | . 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑝 ∈
(Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))) = (𝑅 Σg (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼)))) | 
| 138 |  | ringmnd 20241 | . . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) | 
| 139 | 82, 138 | syl 17 | . . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Mnd) | 
| 140 | 139 | 3ad2ant1 1133 | . . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Mnd) | 
| 141 | 106, 132 | gsumsn 19973 | . . 3
⊢ ((𝑅 ∈ Mnd ∧ {〈𝐼, 𝐼〉} ∈ V ∧ (𝐼𝑀𝐼) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) = (𝐼𝑀𝐼)) | 
| 142 | 140, 23, 125, 141 | syl3anc 1372 | . 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑅 Σg (𝑦 ∈ {{〈𝐼, 𝐼〉}} ↦ (𝐼𝑀𝐼))) = (𝐼𝑀𝐼)) | 
| 143 | 10, 137, 142 | 3eqtrd 2780 | 1
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝐼𝑀𝐼)) |