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

Theorem mdetdiaglem 20901
Description: Lemma for mdetdiag 20902. Previously part of proof for mdet1 20904. (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 = (0g𝑅)
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.
StepHypRef Expression
1 mdetdiaglem.z . . . . . 6 𝑍 = (ℤRHom‘𝑅)
21a1i 11 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → 𝑍 = (ℤRHom‘𝑅))
3 mdetdiaglem.s . . . . . 6 𝑆 = (pmSgn‘𝑁)
43a1i 11 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → 𝑆 = (pmSgn‘𝑁))
52, 4coeq12d 5578 . . . 4 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → (𝑍𝑆) = ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)))
65fveq1d 6495 . . 3 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → ((𝑍𝑆)‘𝑃) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃))
7 eqid 2772 . . . . . . . . . . . 12 (SymGrp‘𝑁) = (SymGrp‘𝑁)
8 mdetdiaglem.g . . . . . . . . . . . 12 𝐻 = (Base‘(SymGrp‘𝑁))
97, 8symgbasf1o 18262 . . . . . . . . . . 11 (𝑃𝐻𝑃:𝑁1-1-onto𝑁)
10 f1ofn 6439 . . . . . . . . . . 11 (𝑃:𝑁1-1-onto𝑁𝑃 Fn 𝑁)
119, 10syl 17 . . . . . . . . . 10 (𝑃𝐻𝑃 Fn 𝑁)
12 fnnfpeq0 6757 . . . . . . . . . 10 (𝑃 Fn 𝑁 → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
1311, 12syl 17 . . . . . . . . 9 (𝑃𝐻 → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
1413adantl 474 . . . . . . . 8 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
1514bicomd 215 . . . . . . 7 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (𝑃 = ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) = ∅))
1615necon3bid 3005 . . . . . 6 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (𝑃 ≠ ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) ≠ ∅))
17 n0 4191 . . . . . . 7 (dom (𝑃 ∖ I ) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ dom (𝑃 ∖ I ))
18 eqid 2772 . . . . . . . . . . 11 (Base‘𝐺) = (Base‘𝐺)
19 mdetdiag.g . . . . . . . . . . . 12 𝐺 = (mulGrp‘𝑅)
20 eqid 2772 . . . . . . . . . . . 12 (.r𝑅) = (.r𝑅)
2119, 20mgpplusg 18956 . . . . . . . . . . 11 (.r𝑅) = (+g𝐺)
2219crngmgp 19018 . . . . . . . . . . . . 13 (𝑅 ∈ CRing → 𝐺 ∈ CMnd)
23223ad2ant1 1113 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝐺 ∈ CMnd)
2423ad2antrr 713 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ CMnd)
25 simpll2 1193 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑁 ∈ Fin)
26 mdetdiag.a . . . . . . . . . . . . . . . . 17 𝐴 = (𝑁 Mat 𝑅)
27 eqid 2772 . . . . . . . . . . . . . . . . 17 (Base‘𝑅) = (Base‘𝑅)
28 mdetdiag.b . . . . . . . . . . . . . . . . 17 𝐵 = (Base‘𝐴)
2926, 27, 28matbas2i 20725 . . . . . . . . . . . . . . . 16 (𝑀𝐵𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
30293ad2ant3 1115 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
31 elmapi 8220 . . . . . . . . . . . . . . 15 (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
3230, 31syl 17 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
3319, 27mgpbas 18958 . . . . . . . . . . . . . . . . 17 (Base‘𝑅) = (Base‘𝐺)
3433eqcomi 2781 . . . . . . . . . . . . . . . 16 (Base‘𝐺) = (Base‘𝑅)
3534a1i 11 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → (Base‘𝐺) = (Base‘𝑅))
3635feq3d 6325 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → (𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺) ↔ 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)))
3732, 36mpbird 249 . . . . . . . . . . . . 13 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
3837ad3antrrr 717 . . . . . . . . . . . 12 (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
397, 8symgbasf 18263 . . . . . . . . . . . . . 14 (𝑃𝐻𝑃:𝑁𝑁)
4039ad2antrl 715 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁𝑁)
4140ffvelrnda 6670 . . . . . . . . . . . 12 (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘𝑁) → (𝑃𝑘) ∈ 𝑁)
42 simpr 477 . . . . . . . . . . . 12 (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘𝑁) → 𝑘𝑁)
4338, 41, 42fovrnd 7130 . . . . . . . . . . 11 (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘𝑁) → ((𝑃𝑘)𝑀𝑘) ∈ (Base‘𝐺))
44 disjdif 4298 . . . . . . . . . . . 12 ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅
4544a1i 11 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅)
46 difss 3994 . . . . . . . . . . . . . . . . . 18 (𝑃 ∖ I ) ⊆ 𝑃
47 dmss 5614 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃)
4846, 47ax-mp 5 . . . . . . . . . . . . . . . . 17 dom (𝑃 ∖ I ) ⊆ dom 𝑃
4939adantl 474 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → 𝑃:𝑁𝑁)
5048, 49fssdm 6354 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
5150sseld 3853 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠𝑁))
5251impr 447 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠𝑁)
5352snssd 4610 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → {𝑠} ⊆ 𝑁)
54 undif 4307 . . . . . . . . . . . . 13 ({𝑠} ⊆ 𝑁 ↔ ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
5553, 54sylib 210 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
5655eqcomd 2778 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑁 = ({𝑠} ∪ (𝑁 ∖ {𝑠})))
5718, 21, 24, 25, 43, 45, 56gsummptfidmsplit 18793 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = ((𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃𝑘)𝑀𝑘)))(.r𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘)))))
58 crngring 19021 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
5958adantr 473 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝑅 ∈ Ring)
6019ringmgp 19016 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
6159, 60syl 17 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝐺 ∈ Mnd)
62613adant3 1112 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝐺 ∈ Mnd)
6362ad2antrr 713 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ Mnd)
64 vex 3412 . . . . . . . . . . . . . 14 𝑠 ∈ V
6564a1i 11 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ V)
6632ad2antrr 713 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
6740, 52ffvelrnd 6671 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃𝑠) ∈ 𝑁)
6866, 67, 52fovrnd 7130 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃𝑠)𝑀𝑠) ∈ (Base‘𝑅))
69 fveq2 6493 . . . . . . . . . . . . . . 15 (𝑘 = 𝑠 → (𝑃𝑘) = (𝑃𝑠))
70 id 22 . . . . . . . . . . . . . . 15 (𝑘 = 𝑠𝑘 = 𝑠)
7169, 70oveq12d 6988 . . . . . . . . . . . . . 14 (𝑘 = 𝑠 → ((𝑃𝑘)𝑀𝑘) = ((𝑃𝑠)𝑀𝑠))
7233, 71gsumsn 18817 . . . . . . . . . . . . 13 ((𝐺 ∈ Mnd ∧ 𝑠 ∈ V ∧ ((𝑃𝑠)𝑀𝑠) ∈ (Base‘𝑅)) → (𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃𝑘)𝑀𝑘))) = ((𝑃𝑠)𝑀𝑠))
7363, 65, 68, 72syl3anc 1351 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃𝑘)𝑀𝑘))) = ((𝑃𝑠)𝑀𝑠))
74 simprr 760 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ dom (𝑃 ∖ I ))
7511ad2antrl 715 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃 Fn 𝑁)
76 fnelnfp 6756 . . . . . . . . . . . . . . 15 ((𝑃 Fn 𝑁𝑠𝑁) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃𝑠) ≠ 𝑠))
7775, 52, 76syl2anc 576 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃𝑠) ≠ 𝑠))
7874, 77mpbid 224 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃𝑠) ≠ 𝑠)
7939ad2antrl 715 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁𝑁)
8039adantl 474 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → 𝑃:𝑁𝑁)
8148, 80fssdm 6354 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
8281sseld 3853 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠𝑁))
8382impr 447 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠𝑁)
8479, 83ffvelrnd 6671 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃𝑠) ∈ 𝑁)
85 neeq1 3023 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑃𝑠) → (𝑖𝑗 ↔ (𝑃𝑠) ≠ 𝑗))
86 oveq1 6977 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑃𝑠) → (𝑖𝑀𝑗) = ((𝑃𝑠)𝑀𝑗))
8786eqeq1d 2774 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑃𝑠) → ((𝑖𝑀𝑗) = 0 ↔ ((𝑃𝑠)𝑀𝑗) = 0 ))
8885, 87imbi12d 337 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑃𝑠) → ((𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ↔ ((𝑃𝑠) ≠ 𝑗 → ((𝑃𝑠)𝑀𝑗) = 0 )))
89 neeq2 3024 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑠 → ((𝑃𝑠) ≠ 𝑗 ↔ (𝑃𝑠) ≠ 𝑠))
90 oveq2 6978 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑠 → ((𝑃𝑠)𝑀𝑗) = ((𝑃𝑠)𝑀𝑠))
9190eqeq1d 2774 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑠 → (((𝑃𝑠)𝑀𝑗) = 0 ↔ ((𝑃𝑠)𝑀𝑠) = 0 ))
9289, 91imbi12d 337 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑠 → (((𝑃𝑠) ≠ 𝑗 → ((𝑃𝑠)𝑀𝑗) = 0 ) ↔ ((𝑃𝑠) ≠ 𝑠 → ((𝑃𝑠)𝑀𝑠) = 0 )))
9388, 92rspc2v 3542 . . . . . . . . . . . . . . . 16 (((𝑃𝑠) ∈ 𝑁𝑠𝑁) → (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃𝑠) ≠ 𝑠 → ((𝑃𝑠)𝑀𝑠) = 0 )))
9484, 83, 93syl2anc 576 . . . . . . . . . . . . . . 15 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃𝑠) ≠ 𝑠 → ((𝑃𝑠)𝑀𝑠) = 0 )))
9594impancom 444 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) → ((𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I )) → ((𝑃𝑠) ≠ 𝑠 → ((𝑃𝑠)𝑀𝑠) = 0 )))
9695imp 398 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃𝑠) ≠ 𝑠 → ((𝑃𝑠)𝑀𝑠) = 0 ))
9778, 96mpd 15 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃𝑠)𝑀𝑠) = 0 )
9873, 97eqtrd 2808 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃𝑘)𝑀𝑘))) = 0 )
9998oveq1d 6985 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃𝑘)𝑀𝑘)))(.r𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘)))) = ( 0 (.r𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘)))))
100583ad2ant1 1113 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝑅 ∈ Ring)
101100ad2antrr 713 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑅 ∈ Ring)
10223adantr 473 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → 𝐺 ∈ CMnd)
103 simpl2 1172 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → 𝑁 ∈ Fin)
104 difss 3994 . . . . . . . . . . . . . 14 (𝑁 ∖ {𝑠}) ⊆ 𝑁
105 ssfi 8525 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ (𝑁 ∖ {𝑠}) ⊆ 𝑁) → (𝑁 ∖ {𝑠}) ∈ Fin)
106103, 104, 105sylancl 577 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → (𝑁 ∖ {𝑠}) ∈ Fin)
10732ad2antrr 713 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
10880adantr 473 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑃:𝑁𝑁)
109 eldifi 3989 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝑁 ∖ {𝑠}) → 𝑘𝑁)
110109adantl 474 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑘𝑁)
111108, 110ffvelrnd 6671 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → (𝑃𝑘) ∈ 𝑁)
112107, 111, 110fovrnd 7130 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → ((𝑃𝑘)𝑀𝑘) ∈ (Base‘𝑅))
113112ralrimiva 3126 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → ∀𝑘 ∈ (𝑁 ∖ {𝑠})((𝑃𝑘)𝑀𝑘) ∈ (Base‘𝑅))
11433, 102, 106, 113gsummptcl 18830 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → (𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
115114ad2ant2r 734 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
116 mdetdiag.0 . . . . . . . . . . . 12 0 = (0g𝑅)
11727, 20, 116ringlz 19050 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘))) ∈ (Base‘𝑅)) → ( 0 (.r𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘)))) = 0 )
118101, 115, 117syl2anc 576 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ( 0 (.r𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘)))) = 0 )
11957, 99, 1183eqtrd 2812 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 )
120119expr 449 . . . . . . . 8 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 ))
121120exlimdv 1892 . . . . . . 7 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (∃𝑠 𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 ))
12217, 121syl5bi 234 . . . . . 6 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (dom (𝑃 ∖ I ) ≠ ∅ → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 ))
12316, 122sylbid 232 . . . . 5 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (𝑃 ≠ ( I ↾ 𝑁) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 ))
124123expimpd 446 . . . 4 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) → ((𝑃𝐻𝑃 ≠ ( I ↾ 𝑁)) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 ))
1251243impia 1097 . . 3 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 )
1266, 125oveq12d 6988 . 2 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍𝑆)‘𝑃) · (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘)))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ))
127 3simpa 1128 . . . 4 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → (𝑅 ∈ CRing ∧ 𝑁 ∈ Fin))
128 simpl 475 . . . 4 ((𝑃𝐻𝑃 ≠ ( I ↾ 𝑁)) → 𝑃𝐻)
12958ad2antrr 713 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃𝐻) → 𝑅 ∈ Ring)
130 zrhpsgnmhm 20420 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
13158, 130sylan 572 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
132 eqid 2772 . . . . . . . 8 (Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅))
1338, 132mhmf 17798 . . . . . . 7 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):𝐻⟶(Base‘(mulGrp‘𝑅)))
134131, 133syl 17 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):𝐻⟶(Base‘(mulGrp‘𝑅)))
135134ffvelrnda 6670 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃𝐻) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅)))
136 eqid 2772 . . . . . . . 8 (mulGrp‘𝑅) = (mulGrp‘𝑅)
137136, 27mgpbas 18958 . . . . . . 7 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
138137eqcomi 2781 . . . . . 6 (Base‘(mulGrp‘𝑅)) = (Base‘𝑅)
139 mdetdiaglem.t . . . . . 6 · = (.r𝑅)
140138, 139, 116ringrz 19051 . . . . 5 ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
141129, 135, 140syl2anc 576 . . . 4 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃𝐻) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
142127, 128, 141syl2an 586 . . 3 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
1431423adant2 1111 . 2 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
144126, 143eqtrd 2808 1 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍𝑆)‘𝑃) · (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘)))) = 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wex 1742  wcel 2048  wne 2961  wral 3082  Vcvv 3409  cdif 3822  cun 3823  cin 3824  wss 3825  c0 4173  {csn 4435  cmpt 5002   I cid 5304   × cxp 5398  dom cdm 5400  cres 5402  ccom 5404   Fn wfn 6177  wf 6178  1-1-ontowf1o 6181  cfv 6182  (class class class)co 6970  𝑚 cmap 8198  Fincfn 8298  Basecbs 16329  .rcmulr 16412  0gc0g 16559   Σg cgsu 16560  Mndcmnd 17752   MndHom cmhm 17791  SymGrpcsymg 18256  pmSgncpsgn 18368  CMndccmn 18656  mulGrpcmgp 18952  Ringcrg 19010  CRingccrg 19011  ℤRHomczrh 20339   Mat cmat 20710   maDet cmdat 20887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-cnex 10383  ax-resscn 10384  ax-1cn 10385  ax-icn 10386  ax-addcl 10387  ax-addrcl 10388  ax-mulcl 10389  ax-mulrcl 10390  ax-mulcom 10391  ax-addass 10392  ax-mulass 10393  ax-distr 10394  ax-i2m1 10395  ax-1ne0 10396  ax-1rid 10397  ax-rnegex 10398  ax-rrecex 10399  ax-cnre 10400  ax-pre-lttri 10401  ax-pre-lttrn 10402  ax-pre-ltadd 10403  ax-pre-mulgt0 10404  ax-addf 10406  ax-mulf 10407
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-xor 1489  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-ot 4444  df-uni 4707  df-int 4744  df-iun 4788  df-iin 4789  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-se 5360  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-of 7221  df-om 7391  df-1st 7494  df-2nd 7495  df-supp 7627  df-tpos 7688  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-1o 7897  df-2o 7898  df-oadd 7901  df-er 8081  df-map 8200  df-ixp 8252  df-en 8299  df-dom 8300  df-sdom 8301  df-fin 8302  df-fsupp 8621  df-sup 8693  df-oi 8761  df-card 9154  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472  df-sub 10664  df-neg 10665  df-div 11091  df-nn 11432  df-2 11496  df-3 11497  df-4 11498  df-5 11499  df-6 11500  df-7 11501  df-8 11502  df-9 11503  df-n0 11701  df-xnn0 11773  df-z 11787  df-dec 11905  df-uz 12052  df-rp 12198  df-fz 12702  df-fzo 12843  df-seq 13178  df-exp 13238  df-hash 13499  df-word 13663  df-lsw 13716  df-concat 13724  df-s1 13749  df-substr 13794  df-pfx 13843  df-splice 13950  df-reverse 13968  df-s2 14062  df-struct 16331  df-ndx 16332  df-slot 16333  df-base 16335  df-sets 16336  df-ress 16337  df-plusg 16424  df-mulr 16425  df-starv 16426  df-sca 16427  df-vsca 16428  df-ip 16429  df-tset 16430  df-ple 16431  df-ds 16433  df-unif 16434  df-hom 16435  df-cco 16436  df-0g 16561  df-gsum 16562  df-prds 16567  df-pws 16569  df-mre 16705  df-mrc 16706  df-acs 16708  df-mgm 17700  df-sgrp 17742  df-mnd 17753  df-mhm 17793  df-submnd 17794  df-grp 17884  df-minusg 17885  df-mulg 18002  df-subg 18050  df-ghm 18117  df-gim 18160  df-cntz 18208  df-oppg 18235  df-symg 18257  df-pmtr 18321  df-psgn 18370  df-cmn 18658  df-abl 18659  df-mgp 18953  df-ur 18965  df-ring 19012  df-cring 19013  df-oppr 19086  df-dvdsr 19104  df-unit 19105  df-invr 19135  df-dvr 19146  df-rnghom 19180  df-drng 19217  df-subrg 19246  df-sra 19656  df-rgmod 19657  df-cnfld 20238  df-zring 20310  df-zrh 20343  df-dsmm 20568  df-frlm 20583  df-mat 20711
This theorem is referenced by:  mdetdiag  20902
  Copyright terms: Public domain W3C validator