mdetdiaglem - Metamath Proof Explorer

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

Theorem mdetdiaglem 22541

Description: Lemma for mdetdiag 22542. Previously part of proof for mdet1 22544. (Contributed by SO, 10-Jul-2018.) (Revised by AV, 17-Aug-2019.)

**Hypotheses**
Ref	Expression
mdetdiag.d	⊢ 𝐷 = (𝑁 maDet 𝑅)
mdetdiag.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mdetdiag.b	⊢ 𝐵 = (Base‘𝐴)
mdetdiag.g	⊢ 𝐺 = (mulGrp‘𝑅)
mdetdiag.0	⊢ 0 = (0_g‘𝑅)
mdetdiaglem.g	⊢ 𝐻 = (Base‘(SymGrp‘𝑁))
mdetdiaglem.z	⊢ 𝑍 = (ℤRHom‘𝑅)
mdetdiaglem.s	⊢ 𝑆 = (pmSgn‘𝑁)
mdetdiaglem.t	⊢ · = (._r‘𝑅)

**Assertion**
Ref	Expression
mdetdiaglem	⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )

Distinct variable groups: 𝐵,𝑘 𝑘,𝐺 𝑘,𝐻 𝑖,𝑀,𝑗,𝑘 𝑖,𝑁,𝑗,𝑘 𝑃,𝑖,𝑗,𝑘 𝑅,𝑘 0 ,𝑖,𝑗,𝑘 Allowed substitution hints: 𝐴(𝑖,𝑗,𝑘) 𝐵(𝑖,𝑗) 𝐷(𝑖,𝑗,𝑘) 𝑅(𝑖,𝑗) 𝑆(𝑖,𝑗,𝑘) · (𝑖,𝑗,𝑘) 𝐺(𝑖,𝑗) 𝐻(𝑖,𝑗) 𝑍(𝑖,𝑗,𝑘)

Proof of Theorem mdetdiaglem Dummy variable 𝑠 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mdetdiaglem.z	. . . . . 6 ⊢ 𝑍 = (ℤRHom‘𝑅)
2	1	a1i 11	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → 𝑍 = (ℤRHom‘𝑅))
3		mdetdiaglem.s	. . . . . 6 ⊢ 𝑆 = (pmSgn‘𝑁)
4	3	a1i 11	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → 𝑆 = (pmSgn‘𝑁))
5	2, 4	coeq12d 5849	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (𝑍 ∘ 𝑆) = ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)))
6	5	fveq1d 6883	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((𝑍 ∘ 𝑆)‘𝑃) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃))
7		eqid 2736	. . . . . . . . . . . 12 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
8		mdetdiaglem.g	. . . . . . . . . . . 12 ⊢ 𝐻 = (Base‘(SymGrp‘𝑁))
9	7, 8	symgbasf1o 19361	. . . . . . . . . . 11 ⊢ (𝑃 ∈ 𝐻 → 𝑃:𝑁–1-1-onto→𝑁)
10		f1ofn 6824	. . . . . . . . . . 11 ⊢ (𝑃:𝑁–1-1-onto→𝑁 → 𝑃 Fn 𝑁)
11	9, 10	syl 17	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝐻 → 𝑃 Fn 𝑁)
12		fnnfpeq0 7175	. . . . . . . . . 10 ⊢ (𝑃 Fn 𝑁 → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝐻 → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
14	13	adantl 481	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
15	14	bicomd 223	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑃 = ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) = ∅))
16	15	necon3bid 2977	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑃 ≠ ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) ≠ ∅))
17		n0 4333	. . . . . . 7 ⊢ (dom (𝑃 ∖ I ) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ dom (𝑃 ∖ I ))
18		eqid 2736	. . . . . . . . . . 11 ⊢ (Base‘𝐺) = (Base‘𝐺)
19		mdetdiag.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (mulGrp‘𝑅)
20		eqid 2736	. . . . . . . . . . . 12 ⊢ (._r‘𝑅) = (._r‘𝑅)
21	19, 20	mgpplusg 20109	. . . . . . . . . . 11 ⊢ (._r‘𝑅) = (+_g‘𝐺)
22	19	crngmgp 20206	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd)
23	22	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ CMnd)
24	23	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ CMnd)
25		simpll2 1214	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑁 ∈ Fin)
26		mdetdiag.a	. . . . . . . . . . . . . . . . 17 ⊢ 𝐴 = (𝑁 Mat 𝑅)
27		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝑅)
28		mdetdiag.b	. . . . . . . . . . . . . . . . 17 ⊢ 𝐵 = (Base‘𝐴)
29	26, 27, 28	matbas2i 22365	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
30	29	3ad2ant3 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
31		elmapi 8868	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
32	30, 31	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
33	19, 27	mgpbas 20110	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝐺)
34	33	eqcomi 2745	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐺) = (Base‘𝑅)
35	34	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (Base‘𝐺) = (Base‘𝑅))
36	35	feq3d 6698	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺) ↔ 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)))
37	32, 36	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
38	37	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
39	7, 8	symgbasf 19362	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ 𝐻 → 𝑃:𝑁⟶𝑁)
40	39	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁⟶𝑁)
41	40	ffvelcdmda 7079	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → (𝑃‘𝑘) ∈ 𝑁)
42		simpr 484	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁)
43	38, 41, 42	fovcdmd 7584	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → ((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝐺))
44		disjdif 4452	. . . . . . . . . . . 12 ⊢ ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅
45	44	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅)
46		difss 4116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∖ I ) ⊆ 𝑃
47		dmss 5887	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃)
48	46, 47	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ dom (𝑃 ∖ I ) ⊆ dom 𝑃
49	39	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → 𝑃:𝑁⟶𝑁)
50	48, 49	fssdm 6730	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
51	50	sseld 3962	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠 ∈ 𝑁))
52	51	impr 454	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ 𝑁)
53	52	snssd 4790	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → {𝑠} ⊆ 𝑁)
54		undif 4462	. . . . . . . . . . . . 13 ⊢ ({𝑠} ⊆ 𝑁 ↔ ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
55	53, 54	sylib 218	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
56	55	eqcomd 2742	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑁 = ({𝑠} ∪ (𝑁 ∖ {𝑠})))
57	18, 21, 24, 25, 43, 45, 56	gsummptfidmsplit 19916	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘)))(._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))))
58		crngring 20210	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
59	58	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝑅 ∈ Ring)
60	19	ringmgp 20204	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
61	59, 60	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝐺 ∈ Mnd)
62	61	3adant3 1132	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ Mnd)
63	62	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ Mnd)
64		vex 3468	. . . . . . . . . . . . . 14 ⊢ 𝑠 ∈ V
65	64	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ V)
66	32	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
67	40, 52	ffvelcdmd 7080	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ∈ 𝑁)
68	66, 67, 52	fovcdmd 7584	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠)𝑀𝑠) ∈ (Base‘𝑅))
69		fveq2 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑠 → (𝑃‘𝑘) = (𝑃‘𝑠))
70		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑠 → 𝑘 = 𝑠)
71	69, 70	oveq12d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑠 → ((𝑃‘𝑘)𝑀𝑘) = ((𝑃‘𝑠)𝑀𝑠))
72	33, 71	gsumsn 19940	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Mnd ∧ 𝑠 ∈ V ∧ ((𝑃‘𝑠)𝑀𝑠) ∈ (Base‘𝑅)) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝑃‘𝑠)𝑀𝑠))
73	63, 65, 68, 72	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝑃‘𝑠)𝑀𝑠))
74		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ dom (𝑃 ∖ I ))
75	11	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃 Fn 𝑁)
76		fnelnfp 7174	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 Fn 𝑁 ∧ 𝑠 ∈ 𝑁) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃‘𝑠) ≠ 𝑠))
77	75, 52, 76	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃‘𝑠) ≠ 𝑠))
78	74, 77	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ≠ 𝑠)
79	39	ad2antrl 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁⟶𝑁)
80	39	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝑃:𝑁⟶𝑁)
81	48, 80	fssdm 6730	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
82	81	sseld 3962	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠 ∈ 𝑁))
83	82	impr 454	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ 𝑁)
84	79, 83	ffvelcdmd 7080	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ∈ 𝑁)
85		neeq1 2995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑃‘𝑠) → (𝑖 ≠ 𝑗 ↔ (𝑃‘𝑠) ≠ 𝑗))
86		oveq1 7417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑃‘𝑠) → (𝑖𝑀𝑗) = ((𝑃‘𝑠)𝑀𝑗))
87	86	eqeq1d 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑃‘𝑠) → ((𝑖𝑀𝑗) = 0 ↔ ((𝑃‘𝑠)𝑀𝑗) = 0 ))
88	85, 87	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑃‘𝑠) → ((𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ↔ ((𝑃‘𝑠) ≠ 𝑗 → ((𝑃‘𝑠)𝑀𝑗) = 0 )))
89		neeq2 2996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑠 → ((𝑃‘𝑠) ≠ 𝑗 ↔ (𝑃‘𝑠) ≠ 𝑠))
90		oveq2 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑠 → ((𝑃‘𝑠)𝑀𝑗) = ((𝑃‘𝑠)𝑀𝑠))
91	90	eqeq1d 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑠 → (((𝑃‘𝑠)𝑀𝑗) = 0 ↔ ((𝑃‘𝑠)𝑀𝑠) = 0 ))
92	89, 91	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑠 → (((𝑃‘𝑠) ≠ 𝑗 → ((𝑃‘𝑠)𝑀𝑗) = 0 ) ↔ ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
93	88, 92	rspc2v 3617	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃‘𝑠) ∈ 𝑁 ∧ 𝑠 ∈ 𝑁) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
94	84, 83, 93	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
95	94	impancom 451	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) → ((𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I )) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
96	95	imp 406	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 ))
97	78, 96	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠)𝑀𝑠) = 0 )
98	73, 97	eqtrd 2771	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
99	98	oveq1d 7425	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘)))(._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))) = ( 0 (._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))))
100	58	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring)
101	100	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑅 ∈ Ring)
102	23	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝐺 ∈ CMnd)
103		simpl2 1193	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝑁 ∈ Fin)
104		difss 4116	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∖ {𝑠}) ⊆ 𝑁
105		ssfi 9192	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ Fin ∧ (𝑁 ∖ {𝑠}) ⊆ 𝑁) → (𝑁 ∖ {𝑠}) ∈ Fin)
106	103, 104, 105	sylancl 586	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝑁 ∖ {𝑠}) ∈ Fin)
107	32	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
108	80	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑃:𝑁⟶𝑁)
109		eldifi 4111	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝑁 ∖ {𝑠}) → 𝑘 ∈ 𝑁)
110	109	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑘 ∈ 𝑁)
111	108, 110	ffvelcdmd 7080	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → (𝑃‘𝑘) ∈ 𝑁)
112	107, 111, 110	fovcdmd 7584	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → ((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝑅))
113	112	ralrimiva 3133	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → ∀𝑘 ∈ (𝑁 ∖ {𝑠})((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝑅))
114	33, 102, 106, 113	gsummptcl 19953	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
115	114	ad2ant2r 747	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
116		mdetdiag.0	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘𝑅)
117	27, 20, 116	ringlz 20258	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅)) → ( 0 (._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )
118	101, 115, 117	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ( 0 (._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )
119	57, 99, 118	3eqtrd 2775	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
120	119	expr 456	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
121	120	exlimdv 1933	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (∃𝑠 𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
122	17, 121	biimtrid 242	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (dom (𝑃 ∖ I ) ≠ ∅ → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
123	16, 122	sylbid 240	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑃 ≠ ( I ↾ 𝑁) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
124	123	expimpd 453	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) → ((𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁)) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
125	124	3impia 1117	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
126	6, 125	oveq12d 7428	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ))
127		3simpa 1148	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (𝑅 ∈ CRing ∧ 𝑁 ∈ Fin))
128		simpl 482	. . . 4 ⊢ ((𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁)) → 𝑃 ∈ 𝐻)
129	58	ad2antrr 726	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → 𝑅 ∈ Ring)
130		zrhpsgnmhm 21549	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
131	58, 130	sylan 580	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
132		eqid 2736	. . . . . . . 8 ⊢ (Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅))
133	8, 132	mhmf 18772	. . . . . . 7 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):𝐻⟶(Base‘(mulGrp‘𝑅)))
134	131, 133	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):𝐻⟶(Base‘(mulGrp‘𝑅)))
135	134	ffvelcdmda 7079	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅)))
136		eqid 2736	. . . . . . . 8 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
137	136, 27	mgpbas 20110	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
138	137	eqcomi 2745	. . . . . 6 ⊢ (Base‘(mulGrp‘𝑅)) = (Base‘𝑅)
139		mdetdiaglem.t	. . . . . 6 ⊢ · = (._r‘𝑅)
140	138, 139, 116	ringrz 20259	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
141	129, 135, 140	syl2anc 584	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
142	127, 128, 141	syl2an 596	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
143	142	3adant2 1131	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
144	126, 143	eqtrd 2771	1 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 Vcvv 3464 ∖ cdif 3928 ∪ cun 3929 ∩ cin 3930 ⊆ wss 3931 ∅c0 4313 {csn 4606 ↦ cmpt 5206 I cid 5552 × cxp 5657 dom cdm 5659 ↾ cres 5661 ∘ ccom 5663 Fn wfn 6531 ⟶wf 6532 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 ↑_m cmap 8845 Fincfn 8964 Basecbs 17233 ._rcmulr 17277 0_gc0g 17458 Σ_g cgsu 17459 Mndcmnd 18717 MndHom cmhm 18764 SymGrpcsymg 19355 pmSgncpsgn 19475 CMndccmn 19766 mulGrpcmgp 20105 Ringcrg 20198 CRingccrg 20199 ℤRHomczrh 21465 Mat cmat 22350 maDet cmdat 22527

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-addf 11213 ax-mulf 11214

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-xor 1512 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-ot 4615 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7676 df-om 7867 df-1st 7993 df-2nd 7994 df-supp 8165 df-tpos 8230 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-er 8724 df-map 8847 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9379 df-sup 9459 df-oi 9529 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-xnn0 12580 df-z 12594 df-dec 12714 df-uz 12858 df-rp 13014 df-fz 13530 df-fzo 13677 df-seq 14025 df-exp 14085 df-hash 14354 df-word 14537 df-lsw 14586 df-concat 14594 df-s1 14619 df-substr 14664 df-pfx 14694 df-splice 14773 df-reverse 14782 df-s2 14872 df-struct 17171 df-sets 17188 df-slot 17206 df-ndx 17218 df-base 17234 df-ress 17257 df-plusg 17289 df-mulr 17290 df-starv 17291 df-sca 17292 df-vsca 17293 df-ip 17294 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-hom 17300 df-cco 17301 df-0g 17460 df-gsum 17461 df-prds 17466 df-pws 17468 df-mre 17603 df-mrc 17604 df-acs 17606 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-mhm 18766 df-submnd 18767 df-efmnd 18852 df-grp 18924 df-minusg 18925 df-mulg 19056 df-subg 19111 df-ghm 19201 df-gim 19247 df-cntz 19305 df-oppg 19334 df-symg 19356 df-pmtr 19428 df-psgn 19477 df-cmn 19768 df-abl 19769 df-mgp 20106 df-rng 20118 df-ur 20147 df-ring 20200 df-cring 20201 df-oppr 20302 df-dvdsr 20322 df-unit 20323 df-invr 20353 df-dvr 20366 df-rhm 20437 df-subrng 20511 df-subrg 20535 df-drng 20696 df-sra 21136 df-rgmod 21137 df-cnfld 21321 df-zring 21413 df-zrh 21469 df-dsmm 21697 df-frlm 21712 df-mat 22351

This theorem is referenced by: mdetdiag 22542

W3C validator