| 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 5874 | . . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (𝑍 ∘ 𝑆) = ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))) | 
| 6 | 5 | fveq1d 6907 | . . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → ((𝑍 ∘ 𝑆)‘𝑃) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃)) | 
| 7 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(SymGrp‘𝑁) =
(SymGrp‘𝑁) | 
| 8 |  | mdetdiaglem.g | . . . . . . . . . . . 12
⊢ 𝐻 =
(Base‘(SymGrp‘𝑁)) | 
| 9 | 7, 8 | symgbasf1o 19393 | . . . . . . . . . . 11
⊢ (𝑃 ∈ 𝐻 → 𝑃:𝑁–1-1-onto→𝑁) | 
| 10 |  | f1ofn 6848 | . . . . . . . . . . 11
⊢ (𝑃:𝑁–1-1-onto→𝑁 → 𝑃 Fn 𝑁) | 
| 11 | 9, 10 | syl 17 | . . . . . . . . . 10
⊢ (𝑃 ∈ 𝐻 → 𝑃 Fn 𝑁) | 
| 12 |  | fnnfpeq0 7199 | . . . . . . . . . 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 2984 | . . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑃 ≠ ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) ≠ ∅)) | 
| 17 |  | n0 4352 | . . . . . . 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 20142 | . . . . . . . . . . 11
⊢
(.r‘𝑅) = (+g‘𝐺) | 
| 22 | 19 | crngmgp 20239 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd) | 
| 23 | 22 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ CMnd) | 
| 24 | 23 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ CMnd) | 
| 25 |  | simpll2 1213 | . . . . . . . . . . 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 22429 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) | 
| 30 | 29 | 3ad2ant3 1135 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) | 
| 31 |  | elmapi 8890 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) | 
| 32 | 30, 31 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)) | 
| 33 | 19, 27 | mgpbas 20143 | . . . . . . . . . . . . . . . . 17
⊢
(Base‘𝑅) =
(Base‘𝐺) | 
| 34 | 33 | eqcomi 2745 | . . . . . . . . . . . . . . . 16
⊢
(Base‘𝐺) =
(Base‘𝑅) | 
| 35 | 34 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (Base‘𝐺) = (Base‘𝑅)) | 
| 36 | 35 | feq3d 6722 | . . . . . . . . . . . . . 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 19394 | . . . . . . . . . . . . . 14
⊢ (𝑃 ∈ 𝐻 → 𝑃:𝑁⟶𝑁) | 
| 40 | 39 | ad2antrl 728 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁⟶𝑁) | 
| 41 | 40 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin ∧
𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → (𝑃‘𝑘) ∈ 𝑁) | 
| 42 |  | simpr 484 | . . . . . . . . . . . 12
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin ∧
𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁) | 
| 43 | 38, 41, 42 | fovcdmd 7606 | . . . . . . . . . . 11
⊢
(((((𝑅 ∈ CRing
∧ 𝑁 ∈ Fin ∧
𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘 ∈ 𝑁) → ((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝐺)) | 
| 44 |  | disjdif 4471 | . . . . . . . . . . . 12
⊢ ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅ | 
| 45 | 44 | a1i 11 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅) | 
| 46 |  | difss 4135 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∖ I ) ⊆ 𝑃 | 
| 47 |  | dmss 5912 | . . . . . . . . . . . . . . . . . 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 6754 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁) | 
| 51 | 50 | sseld 3981 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠 ∈ 𝑁)) | 
| 52 | 51 | impr 454 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ 𝑁) | 
| 53 | 52 | snssd 4808 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → {𝑠} ⊆ 𝑁) | 
| 54 |  | undif 4481 | . . . . . . . . . . . . 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 19949 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘)))(.r‘𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))))) | 
| 58 |  | crngring 20243 | . . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 59 | 58 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝑅 ∈ Ring) | 
| 60 | 19 | ringmgp 20237 | . . . . . . . . . . . . . . . 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 3483 | . . . . . . . . . . . . . 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 7104 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ∈ 𝑁) | 
| 68 | 66, 67, 52 | fovcdmd 7606 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃‘𝑠)𝑀𝑠) ∈ (Base‘𝑅)) | 
| 69 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑠 → (𝑃‘𝑘) = (𝑃‘𝑠)) | 
| 70 |  | id 22 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑠 → 𝑘 = 𝑠) | 
| 71 | 69, 70 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑠 → ((𝑃‘𝑘)𝑀𝑘) = ((𝑃‘𝑠)𝑀𝑠)) | 
| 72 | 33, 71 | gsumsn 19973 | . . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Mnd ∧ 𝑠 ∈ V ∧ ((𝑃‘𝑠)𝑀𝑠) ∈ (Base‘𝑅)) → (𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = ((𝑃‘𝑠)𝑀𝑠)) | 
| 73 | 63, 65, 68, 72 | syl3anc 1372 | . . . . . . . . . . . 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 7198 | . . . . . . . . . . . . . . 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 6754 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁) | 
| 82 | 81 | sseld 3981 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠 ∈ 𝑁)) | 
| 83 | 82 | impr 454 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ 𝑁) | 
| 84 | 79, 83 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃‘𝑠) ∈ 𝑁) | 
| 85 |  | neeq1 3002 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (𝑃‘𝑠) → (𝑖 ≠ 𝑗 ↔ (𝑃‘𝑠) ≠ 𝑗)) | 
| 86 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = (𝑃‘𝑠) → (𝑖𝑀𝑗) = ((𝑃‘𝑠)𝑀𝑗)) | 
| 87 | 86 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (𝑃‘𝑠) → ((𝑖𝑀𝑗) = 0 ↔ ((𝑃‘𝑠)𝑀𝑗) = 0 )) | 
| 88 | 85, 87 | imbi12d 344 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑃‘𝑠) → ((𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ↔ ((𝑃‘𝑠) ≠ 𝑗 → ((𝑃‘𝑠)𝑀𝑗) = 0 ))) | 
| 89 |  | neeq2 3003 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑠 → ((𝑃‘𝑠) ≠ 𝑗 ↔ (𝑃‘𝑠) ≠ 𝑠)) | 
| 90 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑠 → ((𝑃‘𝑠)𝑀𝑗) = ((𝑃‘𝑠)𝑀𝑠)) | 
| 91 | 90 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑠 → (((𝑃‘𝑠)𝑀𝑗) = 0 ↔ ((𝑃‘𝑠)𝑀𝑠) = 0 )) | 
| 92 | 89, 91 | imbi12d 344 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑠 → (((𝑃‘𝑠) ≠ 𝑗 → ((𝑃‘𝑠)𝑀𝑗) = 0 ) ↔ ((𝑃‘𝑠) ≠ 𝑠 → ((𝑃‘𝑠)𝑀𝑠) = 0 ))) | 
| 93 | 88, 92 | rspc2v 3632 | . . . . . . . . . . . . . . . 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 2776 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ) | 
| 99 | 98 | oveq1d 7447 | . . . . . . . . . 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 1192 | . . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → 𝑁 ∈ Fin) | 
| 104 |  | difss 4135 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∖ {𝑠}) ⊆ 𝑁 | 
| 105 |  | ssfi 9214 | . . . . . . . . . . . . . 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 4130 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (𝑁 ∖ {𝑠}) → 𝑘 ∈ 𝑁) | 
| 110 | 109 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑘 ∈ 𝑁) | 
| 111 | 108, 110 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → (𝑃‘𝑘) ∈ 𝑁) | 
| 112 | 107, 111,
110 | fovcdmd 7606 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → ((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝑅)) | 
| 113 | 112 | ralrimiva 3145 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → ∀𝑘 ∈ (𝑁 ∖ {𝑠})((𝑃‘𝑘)𝑀𝑘) ∈ (Base‘𝑅)) | 
| 114 | 33, 102, 106, 113 | gsummptcl 19986 | . . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ 𝑃 ∈ 𝐻) → (𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅)) | 
| 115 | 114 | ad2ant2r 747 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃‘𝑘)𝑀𝑘))) ∈ (Base‘𝑅)) | 
| 116 |  | mdetdiag.0 | . . . . . . . . . . . 12
⊢  0 =
(0g‘𝑅) | 
| 117 | 27, 20, 116 | ringlz 20291 | . . . . . . . . . . 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 2780 | . . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃 ∈ 𝐻 ∧ 𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 ) | 
| 120 | 119 | expr 456 | . . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃 ∈ 𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σg (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘))) = 0 )) | 
| 121 | 120 | exlimdv 1932 | . . . . . . 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 7450 | . 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 21603 | . . . . . . . 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 18803 | . . . . . . 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 7103 | . . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃 ∈ 𝐻) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅))) | 
| 136 |  | eqid 2736 | . . . . . . . 8
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) | 
| 137 | 136, 27 | mgpbas 20143 | . . . . . . 7
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) | 
| 138 | 137 | eqcomi 2745 | . . . . . 6
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘𝑅) | 
| 139 |  | mdetdiaglem.t | . . . . . 6
⊢  · =
(.r‘𝑅) | 
| 140 | 138, 139,
116 | ringrz 20292 | . . . . 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 2776 | 1
⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σg (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 ) |