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 22736

Description: Lemma for mdetdiag 22737. Previously part of proof for mdet1 22739. (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 5852	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (𝑍 ∘ 𝑆) = ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)))
6	5	fveq1d 6885	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((𝑍 ∘ 𝑆)‘𝑃) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃))
7		eqid 2763	. . . . . . . . . . . 12 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
8		mdetdiaglem.g	. . . . . . . . . . . 12 ⊢ 𝐻 = (Base‘(SymGrp‘𝑁))
9	7, 8	symgbasf1o 19446	. . . . . . . . . . 11 ⊢ (𝑃 ∈ 𝐻 → 𝑃:𝑁–1-1-onto→𝑁)
10		f1ofn 6823	. . . . . . . . . . 11 ⊢ (𝑃:𝑁–1-1-onto→𝑁 → 𝑃 Fn 𝑁)
11	9, 10	syl 18	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝐻 → 𝑃 Fn 𝑁)
12		fnnfpeq0 7178	. . . . . . . . . 10 ⊢ (𝑃 Fn 𝑁 → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
13	11, 12	syl 18	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝐻 → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
14	13	adantl 486	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
15	14	bicomd 226	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑃 = ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) = ∅))
16	15	necon3bid 3002	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑃 ≠ ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) ≠ ∅))
17		n0 4308	. . . . . . 7 ⊢ (dom (𝑃 ∖ I ) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ dom (𝑃 ∖ I ))
18		eqid 2763	. . . . . . . . . . 11 ⊢ (Base‘𝐺) = (Base‘𝐺)
19		mdetdiag.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (mulGrp‘𝑅)
20		eqid 2763	. . . . . . . . . . . 12 ⊢ (._r‘𝑅) = (._r‘𝑅)
21	19, 20	mgpplusg 20221	. . . . . . . . . . 11 ⊢ (._r‘𝑅) = (+_g‘𝐺)
22	19	crngmgp 20324	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd)
23	22	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ CMnd)
24	23	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ CMnd)
25		simpll2 1232	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑁 ∈ Fin)
26		mdetdiag.a	. . . . . . . . . . . . . . . . 17 ⊢ 𝐴 = (𝑁 Mat 𝑅)
27		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝑅)
28		mdetdiag.b	. . . . . . . . . . . . . . . . 17 ⊢ 𝐵 = (Base‘𝐴)
29	26, 27, 28	matbas2i 22560	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
30	29	3ad2ant3 1153	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
31		elmapi 8847	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
32	30, 31	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
33	19, 27	mgpbas 20222	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝐺)
34	33	eqcomi 2772	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐺) = (Base‘𝑅)
35	34	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (Base‘𝐺) = (Base‘𝑅))
36	35	feq3d 6692	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺) ↔ 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)))
37	32, 36	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
38	37	ad3antrrr 742	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
39	7, 8	symgbasf 19447	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ 𝐻 → 𝑃:𝑁⟶𝑁)
40	39	ad2antrl 740	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁⟶𝑁)
41	40	ffvelcdmda 7081	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → (𝑃‘𝑘) ∈ 𝑁)
42		simpr 489	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁)
43	38, 41, 42	fovcdmd 7584	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → ((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝐺))
44		disjdif 4434	. . . . . . . . . . . 12 ⊢ ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅
45	44	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅)
46		difss 4091	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∖ I ) ⊆ 𝑃
47		dmss 5894	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃)
48	46, 47	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ dom (𝑃 ∖ I ) ⊆ dom 𝑃
49	39	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → 𝑃:𝑁⟶𝑁)
50	48, 49	fssdm 6727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
51	50	sseld 3937	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠 ∈ 𝑁))
52	51	impr 459	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ 𝑁)
53	52	snssd 4753	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → {𝑠} ⊆ 𝑁)
54		undif 4444	. . . . . . . . . . . . 13 ⊢ ({𝑠} ⊆ 𝑁 ↔ ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
55	53, 54	sylib 221	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
56	55	eqcomd 2769	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑁 = ({𝑠} ∪ (𝑁 ∖ {𝑠})))
57	18, 21, 24, 25, 43, 45, 56	gsummptfidmsplit 20001	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘)))(._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))))
58		crngring 20328	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
59	58	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝑅 ∈ Ring)
60	19	ringmgp 20322	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
61	59, 60	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝐺 ∈ Mnd)
62	61	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ Mnd)
63	62	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ Mnd)
64		vex 3459	. . . . . . . . . . . . . 14 ⊢ 𝑠 ∈ V
65	64	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ V)
66	32	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
67	40, 52	ffvelcdmd 7082	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ∈ 𝑁)
68	66, 67, 52	fovcdmd 7584	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠)𝑀𝑠) ∈ (Base‘𝑅))
69		fveq2 6883	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑠 → (𝑃‘𝑘) = (𝑃‘𝑠))
70		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑠 → 𝑘 = 𝑠)
71	69, 70	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑠 → ((𝑃‘𝑘)𝑀𝑘) = ((𝑃‘𝑠)𝑀𝑠))
72	33, 71	gsumsn 20025	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Mnd ∧ 𝑠 ∈ V ∧ ((𝑃‘𝑠)𝑀𝑠) ∈ (Base‘𝑅)) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝑃‘𝑠)𝑀𝑠))
73	63, 65, 68, 72	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝑃‘𝑠)𝑀𝑠))
74		simprr 784	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ dom (𝑃 ∖ I ))
75	11	ad2antrl 740	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃 Fn 𝑁)
76		fnelnfp 7177	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 Fn 𝑁 ∧ 𝑠 ∈ 𝑁) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃‘𝑠) ≠ 𝑠))
77	75, 52, 76	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃‘𝑠) ≠ 𝑠))
78	74, 77	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ≠ 𝑠)
79	39	ad2antrl 740	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁⟶𝑁)
80	39	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝑃:𝑁⟶𝑁)
81	48, 80	fssdm 6727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
82	81	sseld 3937	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠 ∈ 𝑁))
83	82	impr 459	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ 𝑁)
84	79, 83	ffvelcdmd 7082	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ∈ 𝑁)
85		neeq1 3020	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑃‘𝑠) → (𝑖 ≠ 𝑗 ↔ (𝑃‘𝑠) ≠ 𝑗))
86		oveq1 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑃‘𝑠) → (𝑖𝑀𝑗) = ((𝑃‘𝑠)𝑀𝑗))
87	86	eqeq1d 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑃‘𝑠) → ((𝑖𝑀𝑗) = 0 ↔ ((𝑃‘𝑠)𝑀𝑗) = 0 ))
88	85, 87	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑃‘𝑠) → ((𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ↔ ((𝑃‘𝑠) ≠ 𝑗 → ((𝑃‘𝑠)𝑀𝑗) = 0 )))
89		neeq2 3021	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑠 → ((𝑃‘𝑠) ≠ 𝑗 ↔ (𝑃‘𝑠) ≠ 𝑠))
90		oveq2 7420	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑠 → ((𝑃‘𝑠)𝑀𝑗) = ((𝑃‘𝑠)𝑀𝑠))
91	90	eqeq1d 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑠 → (((𝑃‘𝑠)𝑀𝑗) = 0 ↔ ((𝑃‘𝑠)𝑀𝑠) = 0 ))
92	89, 91	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑠 → (((𝑃‘𝑠) ≠ 𝑗 → ((𝑃‘𝑠)𝑀𝑗) = 0 ) ↔ ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
93	88, 92	rspc2v 3593	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃‘𝑠) ∈ 𝑁 ∧ 𝑠 ∈ 𝑁) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
94	84, 83, 93	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
95	94	impancom 456	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) → ((𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I )) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
96	95	imp 411	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 ))
97	78, 96	mpd 16	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠)𝑀𝑠) = 0 )
98	73, 97	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
99	98	oveq1d 7427	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘)))(._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))) = ( 0 (._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))))
100	58	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring)
101	100	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑅 ∈ Ring)
102	23	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝐺 ∈ CMnd)
103		simpl2 1211	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝑁 ∈ Fin)
104		difss 4091	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∖ {𝑠}) ⊆ 𝑁
105		ssfi 9158	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ Fin ∧ (𝑁 ∖ {𝑠}) ⊆ 𝑁) → (𝑁 ∖ {𝑠}) ∈ Fin)
106	103, 104, 105	sylancl 597	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝑁 ∖ {𝑠}) ∈ Fin)
107	32	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
108	80	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑃:𝑁⟶𝑁)
109		eldifi 4086	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝑁 ∖ {𝑠}) → 𝑘 ∈ 𝑁)
110	109	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑘 ∈ 𝑁)
111	108, 110	ffvelcdmd 7082	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → (𝑃‘𝑘) ∈ 𝑁)
112	107, 111, 110	fovcdmd 7584	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → ((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝑅))
113	112	ralrimiva 3157	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → ∀𝑘 ∈ (𝑁 ∖ {𝑠})((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝑅))
114	33, 102, 106, 113	gsummptcl 20038	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
115	114	ad2ant2r 759	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
116		mdetdiag.0	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘𝑅)
117	27, 20, 116	ringlz 20377	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅)) → ( 0 (._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )
118	101, 115, 117	syl2anc 595	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ( 0 (._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )
119	57, 99, 118	3eqtrd 2802	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
120	119	expr 461	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
121	120	exlimdv 1963	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (∃𝑠 𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
122	17, 121	biimtrid 245	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (dom (𝑃 ∖ I ) ≠ ∅ → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
123	16, 122	sylbid 243	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑃 ≠ ( I ↾ 𝑁) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
124	123	expimpd 458	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) → ((𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁)) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
125	124	3impia 1135	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
126	6, 125	oveq12d 7430	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ))
127		3simpa 1166	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (𝑅 ∈ CRing ∧ 𝑁 ∈ Fin))
128		simpl 487	. . . 4 ⊢ ((𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁)) → 𝑃 ∈ 𝐻)
129	58	ad2antrr 738	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → 𝑅 ∈ Ring)
130		zrhpsgnmhm 21715	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
131	58, 130	sylan 591	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
132		eqid 2763	. . . . . . . 8 ⊢ (Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅))
133	8, 132	mhmf 18848	. . . . . . 7 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):𝐻⟶(Base‘(mulGrp‘𝑅)))
134	131, 133	syl 18	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):𝐻⟶(Base‘(mulGrp‘𝑅)))
135	134	ffvelcdmda 7081	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅)))
136		eqid 2763	. . . . . . . 8 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
137	136, 27	mgpbas 20222	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
138	137	eqcomi 2772	. . . . . 6 ⊢ (Base‘(mulGrp‘𝑅)) = (Base‘𝑅)
139		mdetdiaglem.t	. . . . . 6 ⊢ · = (._r‘𝑅)
140	138, 139, 116	ringrz 20378	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
141	129, 135, 140	syl2anc 595	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
142	127, 128, 141	syl2an 607	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
143	142	3adant2 1149	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
144	126, 143	eqtrd 2798	1 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∃wex 1809 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 Vcvv 3455 ∖ cdif 3903 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4287 {csn 4590 ↦ cmpt 5193 I cid 5557 × cxp 5661 dom cdm 5663 ↾ cres 5665 ∘ ccom 5667 Fn wfn 6533 ⟶wf 6534 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7412 ↑_m cmap 8825 Fincfn 8944 Basecbs 17270 ._rcmulr 17312 0_gc0g 17493 Σ_g cgsu 17494 Mndcmnd 18793 MndHom cmhm 18840 SymGrpcsymg 19440 pmSgncpsgn 19560 CMndccmn 19851 mulGrpcmgp 20217 Ringcrg 20316 CRingccrg 20317 ℤRHomczrh 21630 Mat cmat 22545 maDet cmdat 22722

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178 ax-addf 11180 ax-mulf 11181

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-xor 1542 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-tp 4595 df-op 4597 df-ot 4599 df-uni 4874 df-int 4914 df-iun 4959 df-iin 4960 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8158 df-tpos 8223 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-1o 8454 df-2o 8455 df-er 8695 df-map 8827 df-ixp 8897 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-fsupp 9323 df-sup 9403 df-oi 9473 df-card 9926 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-div 11873 df-nn 12235 df-2 12304 df-3 12305 df-4 12306 df-5 12307 df-6 12308 df-7 12309 df-8 12310 df-9 12311 df-n0 12506 df-xnn0 12579 df-z 12593 df-dec 12713 df-uz 12864 df-rp 13018 df-fz 13537 df-fzo 13685 df-seq 14040 df-exp 14100 df-hash 14369 df-word 14553 df-lsw 14602 df-concat 14610 df-s1 14636 df-substr 14681 df-pfx 14711 df-splice 14789 df-reverse 14798 df-s2 14887 df-struct 17208 df-sets 17225 df-slot 17243 df-ndx 17255 df-base 17271 df-ress 17292 df-plusg 17324 df-mulr 17325 df-starv 17326 df-sca 17327 df-vsca 17328 df-ip 17329 df-tset 17330 df-ple 17331 df-ds 17333 df-unif 17334 df-hom 17335 df-cco 17336 df-0g 17495 df-gsum 17496 df-prds 17501 df-pws 17503 df-mre 17639 df-mrc 17640 df-acs 17642 df-mgm 18699 df-sgrp 18778 df-mnd 18794 df-mhm 18842 df-submnd 18843 df-efmnd 18929 df-grp 19004 df-minusg 19005 df-mulg 19135 df-subg 19190 df-ghm 19285 df-gim 19330 df-cntz 19388 df-oppg 19417 df-symg 19441 df-pmtr 19513 df-psgn 19562 df-cmn 19853 df-abl 19854 df-mgp 20218 df-rng 20232 df-ur 20265 df-ring 20318 df-cring 20319 df-oppr 20420 df-dvdsr 20440 df-unit 20441 df-invr 20471 df-dvr 20484 df-rhm 20555 df-subrng 20632 df-subrg 20656 df-drng 20816 df-sra 21275 df-rgmod 21276 df-cnfld 21504 df-zring 21578 df-zrh 21634 df-dsmm 21863 df-frlm 21878 df-mat 22546

This theorem is referenced by: mdetdiag 22737

W3C validator