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 21818

Description: Lemma for mdetdiag 21819. Previously part of proof for mdet1 21821. (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 5791	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (𝑍 ∘ 𝑆) = ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)))
6	5	fveq1d 6811	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((𝑍 ∘ 𝑆)‘𝑃) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃))
7		eqid 2737	. . . . . . . . . . . 12 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
8		mdetdiaglem.g	. . . . . . . . . . . 12 ⊢ 𝐻 = (Base‘(SymGrp‘𝑁))
9	7, 8	symgbasf1o 19049	. . . . . . . . . . 11 ⊢ (𝑃 ∈ 𝐻 → 𝑃:𝑁–1-1-onto→𝑁)
10		f1ofn 6752	. . . . . . . . . . 11 ⊢ (𝑃:𝑁–1-1-onto→𝑁 → 𝑃 Fn 𝑁)
11	9, 10	syl 17	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝐻 → 𝑃 Fn 𝑁)
12		fnnfpeq0 7087	. . . . . . . . . 10 ⊢ (𝑃 Fn 𝑁 → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
13	11, 12	syl 17	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝐻 → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
14	13	adantl 482	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
15	14	bicomd 222	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑃 = ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) = ∅))
16	15	necon3bid 2986	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑃 ≠ ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) ≠ ∅))
17		n0 4290	. . . . . . 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 19791	. . . . . . . . . . 11 ⊢ (._r‘𝑅) = (+_g‘𝐺)
22	19	crngmgp 19858	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd)
23	22	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ CMnd)
24	23	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ CMnd)
25		simpll2 1212	. . . . . . . . . . 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 21642	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
30	29	3ad2ant3 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
31		elmapi 8683	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
32	30, 31	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
33	19, 27	mgpbas 19793	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝑅) = (Base‘𝐺)
34	33	eqcomi 2746	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐺) = (Base‘𝑅)
35	34	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (Base‘𝐺) = (Base‘𝑅))
36	35	feq3d 6622	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺) ↔ 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)))
37	32, 36	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
38	37	ad3antrrr 727	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
39	7, 8	symgbasf 19050	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ 𝐻 → 𝑃:𝑁⟶𝑁)
40	39	ad2antrl 725	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁⟶𝑁)
41	40	ffvelcdmda 6998	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → (𝑃‘𝑘) ∈ 𝑁)
42		simpr 485	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁)
43	38, 41, 42	fovcdmd 7482	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → ((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝐺))
44		disjdif 4415	. . . . . . . . . . . 12 ⊢ ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅
45	44	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅)
46		difss 4076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∖ I ) ⊆ 𝑃
47		dmss 5829	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃)
48	46, 47	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ dom (𝑃 ∖ I ) ⊆ dom 𝑃
49	39	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → 𝑃:𝑁⟶𝑁)
50	48, 49	fssdm 6655	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
51	50	sseld 3929	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠 ∈ 𝑁))
52	51	impr 455	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ 𝑁)
53	52	snssd 4752	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → {𝑠} ⊆ 𝑁)
54		undif 4425	. . . . . . . . . . . . 13 ⊢ ({𝑠} ⊆ 𝑁 ↔ ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
55	53, 54	sylib 217	. . . . . . . . . . . 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 19598	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘)))(._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))))
58		crngring 19862	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
59	58	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝑅 ∈ Ring)
60	19	ringmgp 19856	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
61	59, 60	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝐺 ∈ Mnd)
62	61	3adant3 1131	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ Mnd)
63	62	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ Mnd)
64		vex 3445	. . . . . . . . . . . . . 14 ⊢ 𝑠 ∈ V
65	64	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ V)
66	32	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
67	40, 52	ffvelcdmd 6999	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ∈ 𝑁)
68	66, 67, 52	fovcdmd 7482	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠)𝑀𝑠) ∈ (Base‘𝑅))
69		fveq2 6809	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑠 → (𝑃‘𝑘) = (𝑃‘𝑠))
70		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑠 → 𝑘 = 𝑠)
71	69, 70	oveq12d 7331	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑠 → ((𝑃‘𝑘)𝑀𝑘) = ((𝑃‘𝑠)𝑀𝑠))
72	33, 71	gsumsn 19622	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Mnd ∧ 𝑠 ∈ V ∧ ((𝑃‘𝑠)𝑀𝑠) ∈ (Base‘𝑅)) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝑃‘𝑠)𝑀𝑠))
73	63, 65, 68, 72	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝑃‘𝑠)𝑀𝑠))
74		simprr 770	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ dom (𝑃 ∖ I ))
75	11	ad2antrl 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃 Fn 𝑁)
76		fnelnfp 7086	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 Fn 𝑁 ∧ 𝑠 ∈ 𝑁) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃‘𝑠) ≠ 𝑠))
77	75, 52, 76	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃‘𝑠) ≠ 𝑠))
78	74, 77	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ≠ 𝑠)
79	39	ad2antrl 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁⟶𝑁)
80	39	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝑃:𝑁⟶𝑁)
81	48, 80	fssdm 6655	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
82	81	sseld 3929	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠 ∈ 𝑁))
83	82	impr 455	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ 𝑁)
84	79, 83	ffvelcdmd 6999	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ∈ 𝑁)
85		neeq1 3004	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑃‘𝑠) → (𝑖 ≠ 𝑗 ↔ (𝑃‘𝑠) ≠ 𝑗))
86		oveq1 7320	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑃‘𝑠) → (𝑖𝑀𝑗) = ((𝑃‘𝑠)𝑀𝑗))
87	86	eqeq1d 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑃‘𝑠) → ((𝑖𝑀𝑗) = 0 ↔ ((𝑃‘𝑠)𝑀𝑗) = 0 ))
88	85, 87	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑃‘𝑠) → ((𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ↔ ((𝑃‘𝑠) ≠ 𝑗 → ((𝑃‘𝑠)𝑀𝑗) = 0 )))
89		neeq2 3005	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑠 → ((𝑃‘𝑠) ≠ 𝑗 ↔ (𝑃‘𝑠) ≠ 𝑠))
90		oveq2 7321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑠 → ((𝑃‘𝑠)𝑀𝑗) = ((𝑃‘𝑠)𝑀𝑠))
91	90	eqeq1d 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑠 → (((𝑃‘𝑠)𝑀𝑗) = 0 ↔ ((𝑃‘𝑠)𝑀𝑠) = 0 ))
92	89, 91	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑠 → (((𝑃‘𝑠) ≠ 𝑗 → ((𝑃‘𝑠)𝑀𝑗) = 0 ) ↔ ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
93	88, 92	rspc2v 3579	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃‘𝑠) ∈ 𝑁 ∧ 𝑠 ∈ 𝑁) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
94	84, 83, 93	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
95	94	impancom 452	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) → ((𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I )) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 )))
96	95	imp 407	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 ))
97	78, 96	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠)𝑀𝑠) = 0 )
98	73, 97	eqtrd 2777	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
99	98	oveq1d 7328	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝐺 Σ_g (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘)))(._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))) = ( 0 (._r‘𝑅)(𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘)))))
100	58	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring)
101	100	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑅 ∈ Ring)
102	23	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝐺 ∈ CMnd)
103		simpl2 1191	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝑁 ∈ Fin)
104		difss 4076	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∖ {𝑠}) ⊆ 𝑁
105		ssfi 9013	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ Fin ∧ (𝑁 ∖ {𝑠}) ⊆ 𝑁) → (𝑁 ∖ {𝑠}) ∈ Fin)
106	103, 104, 105	sylancl 586	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝑁 ∖ {𝑠}) ∈ Fin)
107	32	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
108	80	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑃:𝑁⟶𝑁)
109		eldifi 4071	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝑁 ∖ {𝑠}) → 𝑘 ∈ 𝑁)
110	109	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑘 ∈ 𝑁)
111	108, 110	ffvelcdmd 6999	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → (𝑃‘𝑘) ∈ 𝑁)
112	107, 111, 110	fovcdmd 7482	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → ((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝑅))
113	112	ralrimiva 3140	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → ∀𝑘 ∈ (𝑁 ∖ {𝑠})((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝑅))
114	33, 102, 106, 113	gsummptcl 19635	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
115	114	ad2ant2r 744	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
116		mdetdiag.0	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘𝑅)
117	27, 20, 116	ringlz 19893	. . . . . . . . . . 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 2781	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
120	119	expr 457	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
121	120	exlimdv 1935	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (∃𝑠 𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
122	17, 121	biimtrid 241	. . . . . 6 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (dom (𝑃 ∖ I ) ≠ ∅ → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
123	16, 122	sylbid 239	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑃 ≠ ( I ↾ 𝑁) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
124	123	expimpd 454	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) → ((𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁)) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ))
125	124	3impia 1116	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )
126	6, 125	oveq12d 7331	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ))
127		3simpa 1147	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (𝑅 ∈ CRing ∧ 𝑁 ∈ Fin))
128		simpl 483	. . . 4 ⊢ ((𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁)) → 𝑃 ∈ 𝐻)
129	58	ad2antrr 723	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → 𝑅 ∈ Ring)
130		zrhpsgnmhm 20860	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
131	58, 130	sylan 580	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
132		eqid 2737	. . . . . . . 8 ⊢ (Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅))
133	8, 132	mhmf 18502	. . . . . . 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 6998	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅)))
136		eqid 2737	. . . . . . . 8 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
137	136, 27	mgpbas 19793	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
138	137	eqcomi 2746	. . . . . 6 ⊢ (Base‘(mulGrp‘𝑅)) = (Base‘𝑅)
139		mdetdiaglem.t	. . . . . 6 ⊢ · = (._r‘𝑅)
140	138, 139, 116	ringrz 19894	. . . . 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 1130	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
144	126, 143	eqtrd 2777	1 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σ_g (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1540 ∃wex 1780 ∈ wcel 2105 ≠ wne 2941 ∀wral 3062 Vcvv 3441 ∖ cdif 3893 ∪ cun 3894 ∩ cin 3895 ⊆ wss 3896 ∅c0 4266 {csn 4569 ↦ cmpt 5168 I cid 5504 × cxp 5603 dom cdm 5605 ↾ cres 5607 ∘ ccom 5609 Fn wfn 6458 ⟶wf 6459 –1-1-onto→wf1o 6462 ‘cfv 6463 (class class class)co 7313 ↑_m cmap 8661 Fincfn 8779 Basecbs 16979 ._rcmulr 17030 0_gc0g 17217 Σ_g cgsu 17218 Mndcmnd 18452 MndHom cmhm 18495 SymGrpcsymg 19041 pmSgncpsgn 19164 CMndccmn 19453 mulGrpcmgp 19787 Ringcrg 19850 CRingccrg 19851 ℤRHomczrh 20772 Mat cmat 21625 maDet cmdat 21804

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2708 ax-rep 5222 ax-sep 5236 ax-nul 5243 ax-pow 5301 ax-pr 5365 ax-un 7626 ax-cnex 10997 ax-resscn 10998 ax-1cn 10999 ax-icn 11000 ax-addcl 11001 ax-addrcl 11002 ax-mulcl 11003 ax-mulrcl 11004 ax-mulcom 11005 ax-addass 11006 ax-mulass 11007 ax-distr 11008 ax-i2m1 11009 ax-1ne0 11010 ax-1rid 11011 ax-rnegex 11012 ax-rrecex 11013 ax-cnre 11014 ax-pre-lttri 11015 ax-pre-lttrn 11016 ax-pre-ltadd 11017 ax-pre-mulgt0 11018 ax-addf 11020 ax-mulf 11021

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-xor 1509 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3443 df-sbc 3726 df-csb 3842 df-dif 3899 df-un 3901 df-in 3903 df-ss 3913 df-pss 3915 df-nul 4267 df-if 4470 df-pw 4545 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-ot 4578 df-uni 4849 df-int 4891 df-iun 4937 df-iin 4938 df-br 5086 df-opab 5148 df-mpt 5169 df-tr 5203 df-id 5505 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5560 df-se 5561 df-we 5562 df-xp 5611 df-rel 5612 df-cnv 5613 df-co 5614 df-dm 5615 df-rn 5616 df-res 5617 df-ima 5618 df-pred 6222 df-ord 6289 df-on 6290 df-lim 6291 df-suc 6292 df-iota 6415 df-fun 6465 df-fn 6466 df-f 6467 df-f1 6468 df-fo 6469 df-f1o 6470 df-fv 6471 df-isom 6472 df-riota 7270 df-ov 7316 df-oprab 7317 df-mpo 7318 df-of 7571 df-om 7756 df-1st 7874 df-2nd 7875 df-supp 8023 df-tpos 8087 df-frecs 8142 df-wrecs 8173 df-recs 8247 df-rdg 8286 df-1o 8342 df-2o 8343 df-er 8544 df-map 8663 df-ixp 8732 df-en 8780 df-dom 8781 df-sdom 8782 df-fin 8783 df-fsupp 9197 df-sup 9269 df-oi 9337 df-card 9765 df-pnf 11081 df-mnf 11082 df-xr 11083 df-ltxr 11084 df-le 11085 df-sub 11277 df-neg 11278 df-div 11703 df-nn 12044 df-2 12106 df-3 12107 df-4 12108 df-5 12109 df-6 12110 df-7 12111 df-8 12112 df-9 12113 df-n0 12304 df-xnn0 12376 df-z 12390 df-dec 12508 df-uz 12653 df-rp 12801 df-fz 13310 df-fzo 13453 df-seq 13792 df-exp 13853 df-hash 14115 df-word 14287 df-lsw 14335 df-concat 14343 df-s1 14370 df-substr 14423 df-pfx 14453 df-splice 14532 df-reverse 14541 df-s2 14630 df-struct 16915 df-sets 16932 df-slot 16950 df-ndx 16962 df-base 16980 df-ress 17009 df-plusg 17042 df-mulr 17043 df-starv 17044 df-sca 17045 df-vsca 17046 df-ip 17047 df-tset 17048 df-ple 17049 df-ds 17051 df-unif 17052 df-hom 17053 df-cco 17054 df-0g 17219 df-gsum 17220 df-prds 17225 df-pws 17227 df-mre 17362 df-mrc 17363 df-acs 17365 df-mgm 18393 df-sgrp 18442 df-mnd 18453 df-mhm 18497 df-submnd 18498 df-efmnd 18575 df-grp 18647 df-minusg 18648 df-mulg 18768 df-subg 18819 df-ghm 18899 df-gim 18942 df-cntz 18990 df-oppg 19017 df-symg 19042 df-pmtr 19117 df-psgn 19166 df-cmn 19455 df-abl 19456 df-mgp 19788 df-ur 19805 df-ring 19852 df-cring 19853 df-oppr 19929 df-dvdsr 19950 df-unit 19951 df-invr 19981 df-dvr 19992 df-rnghom 20026 df-drng 20064 df-subrg 20093 df-sra 20505 df-rgmod 20506 df-cnfld 20669 df-zring 20742 df-zrh 20776 df-dsmm 21010 df-frlm 21025 df-mat 21626

This theorem is referenced by: mdetdiag 21819

W3C validator