Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  m1detdiag Structured version   Visualization version   GIF version

Theorem m1detdiag 21240
 Description: The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019.)
Hypotheses
Ref Expression
mdetdiag.d 𝐷 = (𝑁 maDet 𝑅)
mdetdiag.a 𝐴 = (𝑁 Mat 𝑅)
mdetdiag.b 𝐵 = (Base‘𝐴)
Assertion
Ref Expression
m1detdiag ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝐷𝑀) = (𝐼𝑀𝐼))

Proof of Theorem m1detdiag
Dummy variables 𝑏 𝑝 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetdiag.d . . . 4 𝐷 = (𝑁 maDet 𝑅)
2 mdetdiag.a . . . 4 𝐴 = (𝑁 Mat 𝑅)
3 mdetdiag.b . . . 4 𝐵 = (Base‘𝐴)
4 eqid 2798 . . . 4 (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
5 eqid 2798 . . . 4 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
6 eqid 2798 . . . 4 (pmSgn‘𝑁) = (pmSgn‘𝑁)
7 eqid 2798 . . . 4 (.r𝑅) = (.r𝑅)
8 eqid 2798 . . . 4 (mulGrp‘𝑅) = (mulGrp‘𝑅)
91, 2, 3, 4, 5, 6, 7, 8mdetleib 21230 . . 3 (𝑀𝐵 → (𝐷𝑀) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥)))))))
1093ad2ant3 1132 . 2 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝐷𝑀) = (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥)))))))
11 2fveq3 6657 . . . . . . . 8 (𝑁 = {𝐼} → (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘{𝐼})))
1211adantr 484 . . . . . . 7 ((𝑁 = {𝐼} ∧ 𝐼𝑉) → (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘{𝐼})))
13123ad2ant2 1131 . . . . . 6 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘{𝐼})))
14 simp2r 1197 . . . . . . 7 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → 𝐼𝑉)
15 eqid 2798 . . . . . . . 8 (SymGrp‘{𝐼}) = (SymGrp‘{𝐼})
16 eqid 2798 . . . . . . . 8 (Base‘(SymGrp‘{𝐼})) = (Base‘(SymGrp‘{𝐼}))
17 eqid 2798 . . . . . . . 8 {𝐼} = {𝐼}
1815, 16, 17symg1bas 18529 . . . . . . 7 (𝐼𝑉 → (Base‘(SymGrp‘{𝐼})) = {{⟨𝐼, 𝐼⟩}})
1914, 18syl 17 . . . . . 6 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (Base‘(SymGrp‘{𝐼})) = {{⟨𝐼, 𝐼⟩}})
2013, 19eqtrd 2833 . . . . 5 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (Base‘(SymGrp‘𝑁)) = {{⟨𝐼, 𝐼⟩}})
2120mpteq1d 5122 . . . 4 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥))))) = (𝑝 ∈ {{⟨𝐼, 𝐼⟩}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥))))))
22 snex 5300 . . . . . 6 {⟨𝐼, 𝐼⟩} ∈ V
2322a1i 11 . . . . 5 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → {⟨𝐼, 𝐼⟩} ∈ V)
24 ovex 7175 . . . . 5 ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥)))) ∈ V
25 fveq2 6652 . . . . . . . 8 (𝑝 = {⟨𝐼, 𝐼⟩} → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩}))
26 fveq1 6651 . . . . . . . . . . 11 (𝑝 = {⟨𝐼, 𝐼⟩} → (𝑝𝑥) = ({⟨𝐼, 𝐼⟩}‘𝑥))
2726oveq1d 7157 . . . . . . . . . 10 (𝑝 = {⟨𝐼, 𝐼⟩} → ((𝑝𝑥)𝑀𝑥) = (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))
2827mpteq2dv 5129 . . . . . . . . 9 (𝑝 = {⟨𝐼, 𝐼⟩} → (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥)) = (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥)))
2928oveq2d 7158 . . . . . . . 8 (𝑝 = {⟨𝐼, 𝐼⟩} → ((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))))
3025, 29oveq12d 7160 . . . . . . 7 (𝑝 = {⟨𝐼, 𝐼⟩} → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥)))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥)))))
3130fmptsng 6914 . . . . . 6 (({⟨𝐼, 𝐼⟩} ∈ V ∧ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥)))) ∈ V) → {⟨{⟨𝐼, 𝐼⟩}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))))⟩} = (𝑝 ∈ {{⟨𝐼, 𝐼⟩}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥))))))
3231eqcomd 2804 . . . . 5 (({⟨𝐼, 𝐼⟩} ∈ V ∧ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥)))) ∈ V) → (𝑝 ∈ {{⟨𝐼, 𝐼⟩}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥))))) = {⟨{⟨𝐼, 𝐼⟩}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))))⟩})
3323, 24, 32sylancl 589 . . . 4 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝑝 ∈ {{⟨𝐼, 𝐼⟩}} ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥))))) = {⟨{⟨𝐼, 𝐼⟩}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))))⟩})
34 eqid 2798 . . . . . . . . . . . . 13 (SymGrp‘𝑁) = (SymGrp‘𝑁)
35 eqid 2798 . . . . . . . . . . . . 13 {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} = {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin}
3634, 4, 35, 6psgnfn 18639 . . . . . . . . . . . 12 (pmSgn‘𝑁) Fn {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin}
3718adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑁 = {𝐼} ∧ 𝐼𝑉) → (Base‘(SymGrp‘{𝐼})) = {{⟨𝐼, 𝐼⟩}})
3812, 37eqtrd 2833 . . . . . . . . . . . . . . . 16 ((𝑁 = {𝐼} ∧ 𝐼𝑉) → (Base‘(SymGrp‘𝑁)) = {{⟨𝐼, 𝐼⟩}})
39383ad2ant2 1131 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (Base‘(SymGrp‘𝑁)) = {{⟨𝐼, 𝐼⟩}})
40 rabeq 3431 . . . . . . . . . . . . . . 15 ((Base‘(SymGrp‘𝑁)) = {{⟨𝐼, 𝐼⟩}} → {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} = {𝑏 ∈ {{⟨𝐼, 𝐼⟩}} ∣ dom (𝑏 ∖ I ) ∈ Fin})
4139, 40syl 17 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin} = {𝑏 ∈ {{⟨𝐼, 𝐼⟩}} ∣ dom (𝑏 ∖ I ) ∈ Fin})
42 difeq1 4045 . . . . . . . . . . . . . . . . . 18 (𝑏 = {⟨𝐼, 𝐼⟩} → (𝑏 ∖ I ) = ({⟨𝐼, 𝐼⟩} ∖ I ))
4342dmeqd 5743 . . . . . . . . . . . . . . . . 17 (𝑏 = {⟨𝐼, 𝐼⟩} → dom (𝑏 ∖ I ) = dom ({⟨𝐼, 𝐼⟩} ∖ I ))
4443eleq1d 2874 . . . . . . . . . . . . . . . 16 (𝑏 = {⟨𝐼, 𝐼⟩} → (dom (𝑏 ∖ I ) ∈ Fin ↔ dom ({⟨𝐼, 𝐼⟩} ∖ I ) ∈ Fin))
4544rabsnif 4621 . . . . . . . . . . . . . . 15 {𝑏 ∈ {{⟨𝐼, 𝐼⟩}} ∣ dom (𝑏 ∖ I ) ∈ Fin} = if(dom ({⟨𝐼, 𝐼⟩} ∖ I ) ∈ Fin, {{⟨𝐼, 𝐼⟩}}, ∅)
4645a1i 11 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → {𝑏 ∈ {{⟨𝐼, 𝐼⟩}} ∣ dom (𝑏 ∖ I ) ∈ Fin} = if(dom ({⟨𝐼, 𝐼⟩} ∖ I ) ∈ Fin, {{⟨𝐼, 𝐼⟩}}, ∅))
47 restidsing 5892 . . . . . . . . . . . . . . . . . . . 20 ( I ↾ {𝐼}) = ({𝐼} × {𝐼})
48 xpsng 6885 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼𝑉𝐼𝑉) → ({𝐼} × {𝐼}) = {⟨𝐼, 𝐼⟩})
4948anidms 570 . . . . . . . . . . . . . . . . . . . 20 (𝐼𝑉 → ({𝐼} × {𝐼}) = {⟨𝐼, 𝐼⟩})
5047, 49syl5req 2846 . . . . . . . . . . . . . . . . . . 19 (𝐼𝑉 → {⟨𝐼, 𝐼⟩} = ( I ↾ {𝐼}))
51 fnsng 6381 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼𝑉𝐼𝑉) → {⟨𝐼, 𝐼⟩} Fn {𝐼})
5251anidms 570 . . . . . . . . . . . . . . . . . . . 20 (𝐼𝑉 → {⟨𝐼, 𝐼⟩} Fn {𝐼})
53 fnnfpeq0 6924 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝐼, 𝐼⟩} Fn {𝐼} → (dom ({⟨𝐼, 𝐼⟩} ∖ I ) = ∅ ↔ {⟨𝐼, 𝐼⟩} = ( I ↾ {𝐼})))
5452, 53syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐼𝑉 → (dom ({⟨𝐼, 𝐼⟩} ∖ I ) = ∅ ↔ {⟨𝐼, 𝐼⟩} = ( I ↾ {𝐼})))
5550, 54mpbird 260 . . . . . . . . . . . . . . . . . 18 (𝐼𝑉 → dom ({⟨𝐼, 𝐼⟩} ∖ I ) = ∅)
56 0fin 8745 . . . . . . . . . . . . . . . . . 18 ∅ ∈ Fin
5755, 56eqeltrdi 2898 . . . . . . . . . . . . . . . . 17 (𝐼𝑉 → dom ({⟨𝐼, 𝐼⟩} ∖ I ) ∈ Fin)
5857adantl 485 . . . . . . . . . . . . . . . 16 ((𝑁 = {𝐼} ∧ 𝐼𝑉) → dom ({⟨𝐼, 𝐼⟩} ∖ I ) ∈ Fin)
59583ad2ant2 1131 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → dom ({⟨𝐼, 𝐼⟩} ∖ I ) ∈ Fin)
6059iftrued 4435 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → if(dom ({⟨𝐼, 𝐼⟩} ∖ I ) ∈ Fin, {{⟨𝐼, 𝐼⟩}}, ∅) = {{⟨𝐼, 𝐼⟩}})
6141, 46, 603eqtrrd 2838 . . . . . . . . . . . . 13 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → {{⟨𝐼, 𝐼⟩}} = {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin})
6261fneq2d 6422 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((pmSgn‘𝑁) Fn {{⟨𝐼, 𝐼⟩}} ↔ (pmSgn‘𝑁) Fn {𝑏 ∈ (Base‘(SymGrp‘𝑁)) ∣ dom (𝑏 ∖ I ) ∈ Fin}))
6336, 62mpbiri 261 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (pmSgn‘𝑁) Fn {{⟨𝐼, 𝐼⟩}})
6422snid 4563 . . . . . . . . . . 11 {⟨𝐼, 𝐼⟩} ∈ {{⟨𝐼, 𝐼⟩}}
65 fvco2 6742 . . . . . . . . . . 11 (((pmSgn‘𝑁) Fn {{⟨𝐼, 𝐼⟩}} ∧ {⟨𝐼, 𝐼⟩} ∈ {{⟨𝐼, 𝐼⟩}}) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩}) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨𝐼, 𝐼⟩})))
6663, 64, 65sylancl 589 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩}) = ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨𝐼, 𝐼⟩})))
67 fveq2 6652 . . . . . . . . . . . . . . 15 (𝑁 = {𝐼} → (pmSgn‘𝑁) = (pmSgn‘{𝐼}))
6867adantr 484 . . . . . . . . . . . . . 14 ((𝑁 = {𝐼} ∧ 𝐼𝑉) → (pmSgn‘𝑁) = (pmSgn‘{𝐼}))
69683ad2ant2 1131 . . . . . . . . . . . . 13 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (pmSgn‘𝑁) = (pmSgn‘{𝐼}))
7069fveq1d 6654 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((pmSgn‘𝑁)‘{⟨𝐼, 𝐼⟩}) = ((pmSgn‘{𝐼})‘{⟨𝐼, 𝐼⟩}))
71 snidg 4561 . . . . . . . . . . . . . . . . . 18 ({⟨𝐼, 𝐼⟩} ∈ V → {⟨𝐼, 𝐼⟩} ∈ {{⟨𝐼, 𝐼⟩}})
7222, 71mp1i 13 . . . . . . . . . . . . . . . . 17 (𝐼𝑉 → {⟨𝐼, 𝐼⟩} ∈ {{⟨𝐼, 𝐼⟩}})
7372, 18eleqtrrd 2893 . . . . . . . . . . . . . . . 16 (𝐼𝑉 → {⟨𝐼, 𝐼⟩} ∈ (Base‘(SymGrp‘{𝐼})))
7473ancli 552 . . . . . . . . . . . . . . 15 (𝐼𝑉 → (𝐼𝑉 ∧ {⟨𝐼, 𝐼⟩} ∈ (Base‘(SymGrp‘{𝐼}))))
7574adantl 485 . . . . . . . . . . . . . 14 ((𝑁 = {𝐼} ∧ 𝐼𝑉) → (𝐼𝑉 ∧ {⟨𝐼, 𝐼⟩} ∈ (Base‘(SymGrp‘{𝐼}))))
76753ad2ant2 1131 . . . . . . . . . . . . 13 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝐼𝑉 ∧ {⟨𝐼, 𝐼⟩} ∈ (Base‘(SymGrp‘{𝐼}))))
77 eqid 2798 . . . . . . . . . . . . . 14 (pmSgn‘{𝐼}) = (pmSgn‘{𝐼})
7817, 15, 16, 77psgnsn 18658 . . . . . . . . . . . . 13 ((𝐼𝑉 ∧ {⟨𝐼, 𝐼⟩} ∈ (Base‘(SymGrp‘{𝐼}))) → ((pmSgn‘{𝐼})‘{⟨𝐼, 𝐼⟩}) = 1)
7976, 78syl 17 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((pmSgn‘{𝐼})‘{⟨𝐼, 𝐼⟩}) = 1)
8070, 79eqtrd 2833 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((pmSgn‘𝑁)‘{⟨𝐼, 𝐼⟩}) = 1)
8180fveq2d 6656 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((ℤRHom‘𝑅)‘((pmSgn‘𝑁)‘{⟨𝐼, 𝐼⟩})) = ((ℤRHom‘𝑅)‘1))
82 crngring 19320 . . . . . . . . . . . 12 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
83823ad2ant1 1130 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → 𝑅 ∈ Ring)
84 eqid 2798 . . . . . . . . . . . 12 (1r𝑅) = (1r𝑅)
855, 84zrh1 20225 . . . . . . . . . . 11 (𝑅 ∈ Ring → ((ℤRHom‘𝑅)‘1) = (1r𝑅))
8683, 85syl 17 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((ℤRHom‘𝑅)‘1) = (1r𝑅))
8766, 81, 863eqtrd 2837 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩}) = (1r𝑅))
88 simp2l 1196 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → 𝑁 = {𝐼})
8988mpteq1d 5122 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥)) = (𝑥 ∈ {𝐼} ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥)))
9089oveq2d 7158 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))) = ((mulGrp‘𝑅) Σg (𝑥 ∈ {𝐼} ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))))
918ringmgp 19314 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
9282, 91syl 17 . . . . . . . . . . . 12 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ Mnd)
93923ad2ant1 1130 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (mulGrp‘𝑅) ∈ Mnd)
94 snidg 4561 . . . . . . . . . . . . . . . . 17 (𝐼𝑉𝐼 ∈ {𝐼})
9594adantl 485 . . . . . . . . . . . . . . . 16 ((𝑁 = {𝐼} ∧ 𝐼𝑉) → 𝐼 ∈ {𝐼})
96 eleq2 2878 . . . . . . . . . . . . . . . . 17 (𝑁 = {𝐼} → (𝐼𝑁𝐼 ∈ {𝐼}))
9796adantr 484 . . . . . . . . . . . . . . . 16 ((𝑁 = {𝐼} ∧ 𝐼𝑉) → (𝐼𝑁𝐼 ∈ {𝐼}))
9895, 97mpbird 260 . . . . . . . . . . . . . . 15 ((𝑁 = {𝐼} ∧ 𝐼𝑉) → 𝐼𝑁)
993eleq2i 2881 . . . . . . . . . . . . . . . 16 (𝑀𝐵𝑀 ∈ (Base‘𝐴))
10099biimpi 219 . . . . . . . . . . . . . . 15 (𝑀𝐵𝑀 ∈ (Base‘𝐴))
101 simpl 486 . . . . . . . . . . . . . . . 16 ((𝐼𝑁𝑀 ∈ (Base‘𝐴)) → 𝐼𝑁)
102 simpr 488 . . . . . . . . . . . . . . . 16 ((𝐼𝑁𝑀 ∈ (Base‘𝐴)) → 𝑀 ∈ (Base‘𝐴))
103101, 101, 1023jca 1125 . . . . . . . . . . . . . . 15 ((𝐼𝑁𝑀 ∈ (Base‘𝐴)) → (𝐼𝑁𝐼𝑁𝑀 ∈ (Base‘𝐴)))
10498, 100, 103syl2an 598 . . . . . . . . . . . . . 14 (((𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝐼𝑁𝐼𝑁𝑀 ∈ (Base‘𝐴)))
1051043adant1 1127 . . . . . . . . . . . . 13 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝐼𝑁𝐼𝑁𝑀 ∈ (Base‘𝐴)))
106 eqid 2798 . . . . . . . . . . . . . 14 (Base‘𝑅) = (Base‘𝑅)
1072, 106matecl 21068 . . . . . . . . . . . . 13 ((𝐼𝑁𝐼𝑁𝑀 ∈ (Base‘𝐴)) → (𝐼𝑀𝐼) ∈ (Base‘𝑅))
108105, 107syl 17 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝐼𝑀𝐼) ∈ (Base‘𝑅))
1098, 106mgpbas 19256 . . . . . . . . . . . 12 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
110108, 109eleqtrdi 2900 . . . . . . . . . . 11 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝐼𝑀𝐼) ∈ (Base‘(mulGrp‘𝑅)))
111 eqid 2798 . . . . . . . . . . . 12 (Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅))
112 fveq2 6652 . . . . . . . . . . . . . 14 (𝑥 = 𝐼 → ({⟨𝐼, 𝐼⟩}‘𝑥) = ({⟨𝐼, 𝐼⟩}‘𝐼))
113 eqvisset 3458 . . . . . . . . . . . . . . 15 (𝑥 = 𝐼𝐼 ∈ V)
114 fvsng 6926 . . . . . . . . . . . . . . 15 ((𝐼 ∈ V ∧ 𝐼 ∈ V) → ({⟨𝐼, 𝐼⟩}‘𝐼) = 𝐼)
115113, 113, 114syl2anc 587 . . . . . . . . . . . . . 14 (𝑥 = 𝐼 → ({⟨𝐼, 𝐼⟩}‘𝐼) = 𝐼)
116112, 115eqtrd 2833 . . . . . . . . . . . . 13 (𝑥 = 𝐼 → ({⟨𝐼, 𝐼⟩}‘𝑥) = 𝐼)
117 id 22 . . . . . . . . . . . . 13 (𝑥 = 𝐼𝑥 = 𝐼)
118116, 117oveq12d 7160 . . . . . . . . . . . 12 (𝑥 = 𝐼 → (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥) = (𝐼𝑀𝐼))
119111, 118gsumsn 19085 . . . . . . . . . . 11 (((mulGrp‘𝑅) ∈ Mnd ∧ 𝐼𝑉 ∧ (𝐼𝑀𝐼) ∈ (Base‘(mulGrp‘𝑅))) → ((mulGrp‘𝑅) Σg (𝑥 ∈ {𝐼} ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼))
12093, 14, 110, 119syl3anc 1368 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((mulGrp‘𝑅) Σg (𝑥 ∈ {𝐼} ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼))
12190, 120eqtrd 2833 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))) = (𝐼𝑀𝐼))
12287, 121oveq12d 7160 . . . . . . . 8 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥)))) = ((1r𝑅)(.r𝑅)(𝐼𝑀𝐼)))
123983ad2ant2 1131 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → 𝐼𝑁)
1241003ad2ant3 1132 . . . . . . . . . 10 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → 𝑀 ∈ (Base‘𝐴))
125123, 123, 124, 107syl3anc 1368 . . . . . . . . 9 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝐼𝑀𝐼) ∈ (Base‘𝑅))
126106, 7, 84ringlidm 19335 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ (𝐼𝑀𝐼) ∈ (Base‘𝑅)) → ((1r𝑅)(.r𝑅)(𝐼𝑀𝐼)) = (𝐼𝑀𝐼))
12783, 125, 126syl2anc 587 . . . . . . . 8 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((1r𝑅)(.r𝑅)(𝐼𝑀𝐼)) = (𝐼𝑀𝐼))
128122, 127eqtrd 2833 . . . . . . 7 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥)))) = (𝐼𝑀𝐼))
129128opeq2d 4775 . . . . . 6 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → ⟨{⟨𝐼, 𝐼⟩}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))))⟩ = ⟨{⟨𝐼, 𝐼⟩}, (𝐼𝑀𝐼)⟩)
130129sneqd 4539 . . . . 5 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → {⟨{⟨𝐼, 𝐼⟩}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))))⟩} = {⟨{⟨𝐼, 𝐼⟩}, (𝐼𝑀𝐼)⟩})
131 ovex 7175 . . . . . 6 (𝐼𝑀𝐼) ∈ V
132 eqidd 2799 . . . . . . 7 (𝑦 = {⟨𝐼, 𝐼⟩} → (𝐼𝑀𝐼) = (𝐼𝑀𝐼))
133132fmptsng 6914 . . . . . 6 (({⟨𝐼, 𝐼⟩} ∈ V ∧ (𝐼𝑀𝐼) ∈ V) → {⟨{⟨𝐼, 𝐼⟩}, (𝐼𝑀𝐼)⟩} = (𝑦 ∈ {{⟨𝐼, 𝐼⟩}} ↦ (𝐼𝑀𝐼)))
13423, 131, 133sylancl 589 . . . . 5 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → {⟨{⟨𝐼, 𝐼⟩}, (𝐼𝑀𝐼)⟩} = (𝑦 ∈ {{⟨𝐼, 𝐼⟩}} ↦ (𝐼𝑀𝐼)))
135130, 134eqtrd 2833 . . . 4 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → {⟨{⟨𝐼, 𝐼⟩}, ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘{⟨𝐼, 𝐼⟩})(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ (({⟨𝐼, 𝐼⟩}‘𝑥)𝑀𝑥))))⟩} = (𝑦 ∈ {{⟨𝐼, 𝐼⟩}} ↦ (𝐼𝑀𝐼)))
13621, 33, 1353eqtrd 2837 . . 3 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥))))) = (𝑦 ∈ {{⟨𝐼, 𝐼⟩}} ↦ (𝐼𝑀𝐼)))
137136oveq2d 7158 . 2 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r𝑅)((mulGrp‘𝑅) Σg (𝑥𝑁 ↦ ((𝑝𝑥)𝑀𝑥)))))) = (𝑅 Σg (𝑦 ∈ {{⟨𝐼, 𝐼⟩}} ↦ (𝐼𝑀𝐼))))
138 ringmnd 19318 . . . . 5 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
13982, 138syl 17 . . . 4 (𝑅 ∈ CRing → 𝑅 ∈ Mnd)
1401393ad2ant1 1130 . . 3 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → 𝑅 ∈ Mnd)
141106, 132gsumsn 19085 . . 3 ((𝑅 ∈ Mnd ∧ {⟨𝐼, 𝐼⟩} ∈ V ∧ (𝐼𝑀𝐼) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑦 ∈ {{⟨𝐼, 𝐼⟩}} ↦ (𝐼𝑀𝐼))) = (𝐼𝑀𝐼))
142140, 23, 125, 141syl3anc 1368 . 2 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝑅 Σg (𝑦 ∈ {{⟨𝐼, 𝐼⟩}} ↦ (𝐼𝑀𝐼))) = (𝐼𝑀𝐼))
14310, 137, 1423eqtrd 2837 1 ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼𝑉) ∧ 𝑀𝐵) → (𝐷𝑀) = (𝐼𝑀𝐼))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {crab 3110  Vcvv 3441   ∖ cdif 3879  ∅c0 4245  ifcif 4427  {csn 4527  ⟨cop 4533   ↦ cmpt 5113   I cid 5427   × cxp 5520  dom cdm 5522   ↾ cres 5524   ∘ ccom 5526   Fn wfn 6324  ‘cfv 6329  (class class class)co 7142  Fincfn 8507  1c1 10542  Basecbs 16492  .rcmulr 16575   Σg cgsu 16723  Mndcmnd 17920  SymGrpcsymg 18505  pmSgncpsgn 18627  mulGrpcmgp 19250  1rcur 19262  Ringcrg 19308  CRingccrg 19309  ℤRHomczrh 20212   Mat cmat 21050   maDet cmdat 21227 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7451  ax-cnex 10597  ax-resscn 10598  ax-1cn 10599  ax-icn 10600  ax-addcl 10601  ax-addrcl 10602  ax-mulcl 10603  ax-mulrcl 10604  ax-mulcom 10605  ax-addass 10606  ax-mulass 10607  ax-distr 10608  ax-i2m1 10609  ax-1ne0 10610  ax-1rid 10611  ax-rnegex 10612  ax-rrecex 10613  ax-cnre 10614  ax-pre-lttri 10615  ax-pre-lttrn 10616  ax-pre-ltadd 10617  ax-pre-mulgt0 10618  ax-addf 10620  ax-mulf 10621 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-xor 1503  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4246  df-if 4428  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-ot 4536  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-se 5482  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-isom 6338  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7571  df-1st 7681  df-2nd 7682  df-supp 7824  df-tpos 7890  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-2o 8101  df-oadd 8104  df-er 8287  df-map 8406  df-ixp 8460  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-fsupp 8833  df-sup 8905  df-oi 8973  df-card 9367  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-div 11302  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-xnn0 11973  df-z 11987  df-dec 12104  df-uz 12249  df-rp 12395  df-fz 12903  df-fzo 13046  df-seq 13382  df-exp 13443  df-hash 13704  df-word 13875  df-lsw 13923  df-concat 13931  df-s1 13958  df-substr 14011  df-pfx 14041  df-splice 14120  df-reverse 14129  df-s2 14218  df-struct 16494  df-ndx 16495  df-slot 16496  df-base 16498  df-sets 16499  df-ress 16500  df-plusg 16587  df-mulr 16588  df-starv 16589  df-sca 16590  df-vsca 16591  df-ip 16592  df-tset 16593  df-ple 16594  df-ds 16596  df-unif 16597  df-hom 16598  df-cco 16599  df-0g 16724  df-gsum 16725  df-prds 16730  df-pws 16732  df-mre 16866  df-mrc 16867  df-acs 16869  df-mgm 17861  df-sgrp 17910  df-mnd 17921  df-mhm 17965  df-submnd 17966  df-efmnd 18043  df-grp 18115  df-minusg 18116  df-mulg 18235  df-subg 18286  df-ghm 18366  df-gim 18409  df-cntz 18457  df-oppg 18484  df-symg 18506  df-pmtr 18580  df-psgn 18629  df-cmn 18918  df-mgp 19251  df-ur 19263  df-ring 19310  df-cring 19311  df-rnghom 19481  df-subrg 19544  df-sra 19955  df-rgmod 19956  df-cnfld 20110  df-zring 20182  df-zrh 20216  df-dsmm 20440  df-frlm 20455  df-mat 21051  df-mdet 21228 This theorem is referenced by:  chpmat1d  21479
 Copyright terms: Public domain W3C validator