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 22573

Description: Lemma for mdetdiag 22574. Previously part of proof for mdet1 22576. (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 5813	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (𝑍 ∘ 𝑆) = ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)))
6	5	fveq1d 6836	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((𝑍 ∘ 𝑆)‘𝑃) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃))
7		eqid 2737	. . . . . . . . . . . 12 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
8		mdetdiaglem.g	. . . . . . . . . . . 12 ⊢ 𝐻 = (Base‘(SymGrp‘𝑁))
9	7, 8	symgbasf1o 19341	. . . . . . . . . . 11 ⊢ (𝑃 ∈ 𝐻 → 𝑃:𝑁–1-1-onto→𝑁)
10		f1ofn 6775	. . . . . . . . . . 11 ⊢ (𝑃:𝑁–1-1-onto→𝑁 → 𝑃 Fn 𝑁)
11	9, 10	syl 17	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝐻 → 𝑃 Fn 𝑁)
12		fnnfpeq0 7126	. . . . . . . . . 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 4294	. . . . . . 7 ⊢ (dom (𝑃 ∖ I ) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ dom (𝑃 ∖ I ))
18		eqid 2737	. . . . . . . . . . 11 ⊢ (Base‘𝐺) = (Base‘𝐺)
19		mdetdiag.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (mulGrp‘𝑅)
20		eqid 2737	. . . . . . . . . . . 12 ⊢ (._r‘𝑅) = (._r‘𝑅)
21	19, 20	mgpplusg 20116	. . . . . . . . . . 11 ⊢ (._r‘𝑅) = (+_g‘𝐺)
22	19	crngmgp 20213	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd)
23	22	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ CMnd)
24	23	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ CMnd)
25		simpll2 1215	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑁 ∈ Fin)
26		mdetdiag.a	. . . . . . . . . . . . . . . . 17 ⊢ 𝐴 = (𝑁 Mat 𝑅)
27		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝑅)
28		mdetdiag.b	. . . . . . . . . . . . . . . . 17 ⊢ 𝐵 = (Base‘𝐴)
29	26, 27, 28	matbas2i 22397	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
30	29	3ad2ant3 1136	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
31		elmapi 8789	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
32	30, 31	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
33	19, 27	mgpbas 20117	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝐺)
34	33	eqcomi 2746	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐺) = (Base‘𝑅)
35	34	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (Base‘𝐺) = (Base‘𝑅))
36	35	feq3d 6647	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺) ↔ 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)))
37	32, 36	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
38	37	ad3antrrr 731	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
39	7, 8	symgbasf 19342	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ 𝐻 → 𝑃:𝑁⟶𝑁)
40	39	ad2antrl 729	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁⟶𝑁)
41	40	ffvelcdmda 7030	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → (𝑃‘𝑘) ∈ 𝑁)
42		simpr 484	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁)
43	38, 41, 42	fovcdmd 7532	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → ((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝐺))
44		disjdif 4413	. . . . . . . . . . . 12 ⊢ ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅
45	44	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅)
46		difss 4077	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∖ I ) ⊆ 𝑃
47		dmss 5851	. . . . . . . . . . . . . . . . . 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 6681	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
51	50	sseld 3921	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠 ∈ 𝑁))
52	51	impr 454	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ 𝑁)
53	52	snssd 4753	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → {𝑠} ⊆ 𝑁)
54		undif 4423	. . . . . . . . . . . . 13 ⊢ ({𝑠} ⊆ 𝑁 ↔ ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
55	53, 54	sylib 218	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
56	55	eqcomd 2743	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑁 = ({𝑠} ∪ (𝑁 ∖ {𝑠})))
57	18, 21, 24, 25, 43, 45, 56	gsummptfidmsplit 19896	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘)))(._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))))
58		crngring 20217	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
59	58	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝑅 ∈ Ring)
60	19	ringmgp 20211	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
61	59, 60	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝐺 ∈ Mnd)
62	61	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ Mnd)
63	62	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ Mnd)
64		vex 3434	. . . . . . . . . . . . . 14 ⊢ 𝑠 ∈ V
65	64	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ V)
66	32	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
67	40, 52	ffvelcdmd 7031	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ∈ 𝑁)
68	66, 67, 52	fovcdmd 7532	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠)𝑀𝑠) ∈ (Base‘𝑅))
69		fveq2 6834	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑠 → (𝑃‘𝑘) = (𝑃‘𝑠))
70		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑠 → 𝑘 = 𝑠)
71	69, 70	oveq12d 7378	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑠 → ((𝑃‘𝑘)𝑀𝑘) = ((𝑃‘𝑠)𝑀𝑠))
72	33, 71	gsumsn 19920	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Mnd ∧ 𝑠 ∈ V ∧ ((𝑃‘𝑠)𝑀𝑠) ∈ (Base‘𝑅)) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝑃‘𝑠)𝑀𝑠))
73	63, 65, 68, 72	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝑃‘𝑠)𝑀𝑠))
74		simprr 773	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ dom (𝑃 ∖ I ))
75	11	ad2antrl 729	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃 Fn 𝑁)
76		fnelnfp 7125	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 Fn 𝑁 ∧ 𝑠 ∈ 𝑁) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃‘𝑠) ≠ 𝑠))
77	75, 52, 76	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃‘𝑠) ≠ 𝑠))
78	74, 77	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ≠ 𝑠)
79	39	ad2antrl 729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁⟶𝑁)
80	39	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝑃:𝑁⟶𝑁)
81	48, 80	fssdm 6681	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
82	81	sseld 3921	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠 ∈ 𝑁))
83	82	impr 454	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ 𝑁)
84	79, 83	ffvelcdmd 7031	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ∈ 𝑁)
85		neeq1 2995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑃‘𝑠) → (𝑖 ≠ 𝑗 ↔ (𝑃‘𝑠) ≠ 𝑗))
86		oveq1 7367	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑃‘𝑠) → (𝑖𝑀𝑗) = ((𝑃‘𝑠)𝑀𝑗))
87	86	eqeq1d 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑃‘𝑠) → ((𝑖𝑀𝑗) = 0 ↔ ((𝑃‘𝑠)𝑀𝑗) = 0 ))
88	85, 87	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑃‘𝑠) → ((𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ↔ ((𝑃‘𝑠) ≠ 𝑗 → ((𝑃‘𝑠)𝑀𝑗) = 0 )))
89		neeq2 2996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑠 → ((𝑃‘𝑠) ≠ 𝑗 ↔ (𝑃‘𝑠) ≠ 𝑠))
90		oveq2 7368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑠 → ((𝑃‘𝑠)𝑀𝑗) = ((𝑃‘𝑠)𝑀𝑠))
91	90	eqeq1d 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑠 → (((𝑃‘𝑠)𝑀𝑗) = 0 ↔ ((𝑃‘𝑠)𝑀𝑠) = 0 ))
92	89, 91	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑠 → (((𝑃‘𝑠) ≠ 𝑗 → ((𝑃‘𝑠)𝑀𝑗) = 0 ) ↔ ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
93	88, 92	rspc2v 3576	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃‘𝑠) ∈ 𝑁 ∧ 𝑠 ∈ 𝑁) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
94	84, 83, 93	syl2anc 585	. . . . . . . . . . . . . . 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 2772	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
99	98	oveq1d 7375	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘)))(._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))) = ( 0 (._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))))
100	58	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring)
101	100	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑅 ∈ Ring)
102	23	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝐺 ∈ CMnd)
103		simpl2 1194	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝑁 ∈ Fin)
104		difss 4077	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∖ {𝑠}) ⊆ 𝑁
105		ssfi 9100	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ Fin ∧ (𝑁 ∖ {𝑠}) ⊆ 𝑁) → (𝑁 ∖ {𝑠}) ∈ Fin)
106	103, 104, 105	sylancl 587	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝑁 ∖ {𝑠}) ∈ Fin)
107	32	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
108	80	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑃:𝑁⟶𝑁)
109		eldifi 4072	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝑁 ∖ {𝑠}) → 𝑘 ∈ 𝑁)
110	109	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑘 ∈ 𝑁)
111	108, 110	ffvelcdmd 7031	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → (𝑃‘𝑘) ∈ 𝑁)
112	107, 111, 110	fovcdmd 7532	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → ((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝑅))
113	112	ralrimiva 3130	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → ∀𝑘 ∈ (𝑁 ∖ {𝑠})((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝑅))
114	33, 102, 106, 113	gsummptcl 19933	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
115	114	ad2ant2r 748	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
116		mdetdiag.0	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘𝑅)
117	27, 20, 116	ringlz 20265	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅)) → ( 0 (._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )
118	101, 115, 117	syl2anc 585	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ( 0 (._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )
119	57, 99, 118	3eqtrd 2776	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
120	119	expr 456	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
121	120	exlimdv 1935	. . . . . . 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 1118	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
126	6, 125	oveq12d 7378	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ))
127		3simpa 1149	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (𝑅 ∈ CRing ∧ 𝑁 ∈ Fin))
128		simpl 482	. . . 4 ⊢ ((𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁)) → 𝑃 ∈ 𝐻)
129	58	ad2antrr 727	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → 𝑅 ∈ Ring)
130		zrhpsgnmhm 21574	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
131	58, 130	sylan 581	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
132		eqid 2737	. . . . . . . 8 ⊢ (Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅))
133	8, 132	mhmf 18748	. . . . . . 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 7030	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅)))
136		eqid 2737	. . . . . . . 8 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
137	136, 27	mgpbas 20117	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
138	137	eqcomi 2746	. . . . . 6 ⊢ (Base‘(mulGrp‘𝑅)) = (Base‘𝑅)
139		mdetdiaglem.t	. . . . . 6 ⊢ · = (._r‘𝑅)
140	138, 139, 116	ringrz 20266	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
141	129, 135, 140	syl2anc 585	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
142	127, 128, 141	syl2an 597	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
143	142	3adant2 1132	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
144	126, 143	eqtrd 2772	1 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 Vcvv 3430 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 {csn 4568 ↦ cmpt 5167 I cid 5518 × cxp 5622 dom cdm 5624 ↾ cres 5626 ∘ ccom 5628 Fn wfn 6487 ⟶wf 6488 –1-1-onto→wf1o 6491 ‘cfv 6492 (class class class)co 7360 ↑_m cmap 8766 Fincfn 8886 Basecbs 17170 ._rcmulr 17212 0_gc0g 17393 Σ_g cgsu 17394 Mndcmnd 18693 MndHom cmhm 18740 SymGrpcsymg 19335 pmSgncpsgn 19455 CMndccmn 19746 mulGrpcmgp 20112 Ringcrg 20205 CRingccrg 20206 ℤRHomczrh 21489 Mat cmat 22382 maDet cmdat 22559

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-addf 11108 ax-mulf 11109

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-xor 1514 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-ot 4577 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-of 7624 df-om 7811 df-1st 7935 df-2nd 7936 df-supp 8104 df-tpos 8169 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-2o 8399 df-er 8636 df-map 8768 df-ixp 8839 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-fsupp 9268 df-sup 9348 df-oi 9418 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-xnn0 12502 df-z 12516 df-dec 12636 df-uz 12780 df-rp 12934 df-fz 13453 df-fzo 13600 df-seq 13955 df-exp 14015 df-hash 14284 df-word 14467 df-lsw 14516 df-concat 14524 df-s1 14550 df-substr 14595 df-pfx 14625 df-splice 14703 df-reverse 14712 df-s2 14801 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-starv 17226 df-sca 17227 df-vsca 17228 df-ip 17229 df-tset 17230 df-ple 17231 df-ds 17233 df-unif 17234 df-hom 17235 df-cco 17236 df-0g 17395 df-gsum 17396 df-prds 17401 df-pws 17403 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-mhm 18742 df-submnd 18743 df-efmnd 18828 df-grp 18903 df-minusg 18904 df-mulg 19035 df-subg 19090 df-ghm 19179 df-gim 19225 df-cntz 19283 df-oppg 19312 df-symg 19336 df-pmtr 19408 df-psgn 19457 df-cmn 19748 df-abl 19749 df-mgp 20113 df-rng 20125 df-ur 20154 df-ring 20207 df-cring 20208 df-oppr 20308 df-dvdsr 20328 df-unit 20329 df-invr 20359 df-dvr 20372 df-rhm 20443 df-subrng 20514 df-subrg 20538 df-drng 20699 df-sra 21160 df-rgmod 21161 df-cnfld 21345 df-zring 21437 df-zrh 21493 df-dsmm 21722 df-frlm 21737 df-mat 22383

This theorem is referenced by: mdetdiag 22574

W3C validator