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

Theorem mdetdiaglem 20171
Description: Lemma for mdetdiag 20172. Previously part of proof for mdet1 20174. (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 5196 . . . 4 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → (𝑍𝑆) = ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)))
65fveq1d 6090 . . 3 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → ((𝑍𝑆)‘𝑃) = (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃))
7 eqid 2610 . . . . . . . . . . . 12 (SymGrp‘𝑁) = (SymGrp‘𝑁)
8 mdetdiaglem.g . . . . . . . . . . . 12 𝐻 = (Base‘(SymGrp‘𝑁))
97, 8symgbasf1o 17575 . . . . . . . . . . 11 (𝑃𝐻𝑃:𝑁1-1-onto𝑁)
10 f1ofn 6036 . . . . . . . . . . 11 (𝑃:𝑁1-1-onto𝑁𝑃 Fn 𝑁)
119, 10syl 17 . . . . . . . . . 10 (𝑃𝐻𝑃 Fn 𝑁)
12 fnnfpeq0 6327 . . . . . . . . . 10 (𝑃 Fn 𝑁 → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
1311, 12syl 17 . . . . . . . . 9 (𝑃𝐻 → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
1413adantl 481 . . . . . . . 8 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (dom (𝑃 ∖ I ) = ∅ ↔ 𝑃 = ( I ↾ 𝑁)))
1514bicomd 212 . . . . . . 7 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (𝑃 = ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) = ∅))
1615necon3bid 2826 . . . . . 6 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (𝑃 ≠ ( I ↾ 𝑁) ↔ dom (𝑃 ∖ I ) ≠ ∅))
17 n0 3890 . . . . . . 7 (dom (𝑃 ∖ I ) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ dom (𝑃 ∖ I ))
18 eqid 2610 . . . . . . . . . . 11 (Base‘𝐺) = (Base‘𝐺)
19 mdetdiag.g . . . . . . . . . . . 12 𝐺 = (mulGrp‘𝑅)
20 eqid 2610 . . . . . . . . . . . 12 (.r𝑅) = (.r𝑅)
2119, 20mgpplusg 18265 . . . . . . . . . . 11 (.r𝑅) = (+g𝐺)
2219crngmgp 18327 . . . . . . . . . . . . 13 (𝑅 ∈ CRing → 𝐺 ∈ CMnd)
23223ad2ant1 1075 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝐺 ∈ CMnd)
2423ad2antrr 758 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ CMnd)
25 simpll2 1094 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑁 ∈ Fin)
26 mdetdiag.a . . . . . . . . . . . . . . . . 17 𝐴 = (𝑁 Mat 𝑅)
27 eqid 2610 . . . . . . . . . . . . . . . . 17 (Base‘𝑅) = (Base‘𝑅)
28 mdetdiag.b . . . . . . . . . . . . . . . . 17 𝐵 = (Base‘𝐴)
2926, 27, 28matbas2i 19995 . . . . . . . . . . . . . . . 16 (𝑀𝐵𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
30293ad2ant3 1077 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
31 elmapi 7743 . . . . . . . . . . . . . . 15 (𝑀 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
3230, 31syl 17 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
3319, 27mgpbas 18267 . . . . . . . . . . . . . . . . 17 (Base‘𝑅) = (Base‘𝐺)
3433eqcomi 2619 . . . . . . . . . . . . . . . 16 (Base‘𝐺) = (Base‘𝑅)
3534a1i 11 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → (Base‘𝐺) = (Base‘𝑅))
3635feq3d 5931 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → (𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺) ↔ 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅)))
3732, 36mpbird 246 . . . . . . . . . . . . 13 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
3837ad3antrrr 762 . . . . . . . . . . . 12 (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘𝑁) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝐺))
397, 8symgbasf 17576 . . . . . . . . . . . . . 14 (𝑃𝐻𝑃:𝑁𝑁)
4039ad2antrl 760 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁𝑁)
4140ffvelrnda 6252 . . . . . . . . . . . 12 (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘𝑁) → (𝑃𝑘) ∈ 𝑁)
42 simpr 476 . . . . . . . . . . . 12 (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘𝑁) → 𝑘𝑁)
4338, 41, 42fovrnd 6682 . . . . . . . . . . 11 (((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) ∧ 𝑘𝑁) → ((𝑃𝑘)𝑀𝑘) ∈ (Base‘𝐺))
44 disjdif 3992 . . . . . . . . . . . 12 ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅
4544a1i 11 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∩ (𝑁 ∖ {𝑠})) = ∅)
46 difss 3699 . . . . . . . . . . . . . . . . . 18 (𝑃 ∖ I ) ⊆ 𝑃
47 dmss 5232 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃)
4846, 47ax-mp 5 . . . . . . . . . . . . . . . . 17 dom (𝑃 ∖ I ) ⊆ dom 𝑃
4939adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → 𝑃:𝑁𝑁)
50 fdm 5950 . . . . . . . . . . . . . . . . . 18 (𝑃:𝑁𝑁 → dom 𝑃 = 𝑁)
5149, 50syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → dom 𝑃 = 𝑁)
5248, 51syl5sseq 3616 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
5352sseld 3567 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠𝑁))
5453impr 647 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠𝑁)
5554snssd 4281 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → {𝑠} ⊆ 𝑁)
56 undif 4001 . . . . . . . . . . . . 13 ({𝑠} ⊆ 𝑁 ↔ ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
5755, 56sylib 207 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ({𝑠} ∪ (𝑁 ∖ {𝑠})) = 𝑁)
5857eqcomd 2616 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑁 = ({𝑠} ∪ (𝑁 ∖ {𝑠})))
5918, 21, 24, 25, 43, 45, 58gsummptfidmsplit 18102 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = ((𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃𝑘)𝑀𝑘)))(.r𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘)))))
60 crngring 18330 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
6160adantr 480 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝑅 ∈ Ring)
6219ringmgp 18325 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Ring → 𝐺 ∈ Mnd)
6361, 62syl 17 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝐺 ∈ Mnd)
64633adant3 1074 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝐺 ∈ Mnd)
6564ad2antrr 758 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝐺 ∈ Mnd)
66 vex 3176 . . . . . . . . . . . . . 14 𝑠 ∈ V
6766a1i 11 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ V)
6832ad2antrr 758 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
6940, 54ffvelrnd 6253 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃𝑠) ∈ 𝑁)
7068, 69, 54fovrnd 6682 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃𝑠)𝑀𝑠) ∈ (Base‘𝑅))
71 fveq2 6088 . . . . . . . . . . . . . . 15 (𝑘 = 𝑠 → (𝑃𝑘) = (𝑃𝑠))
72 id 22 . . . . . . . . . . . . . . 15 (𝑘 = 𝑠𝑘 = 𝑠)
7371, 72oveq12d 6545 . . . . . . . . . . . . . 14 (𝑘 = 𝑠 → ((𝑃𝑘)𝑀𝑘) = ((𝑃𝑠)𝑀𝑠))
7433, 73gsumsn 18126 . . . . . . . . . . . . 13 ((𝐺 ∈ Mnd ∧ 𝑠 ∈ V ∧ ((𝑃𝑠)𝑀𝑠) ∈ (Base‘𝑅)) → (𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃𝑘)𝑀𝑘))) = ((𝑃𝑠)𝑀𝑠))
7565, 67, 70, 74syl3anc 1318 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃𝑘)𝑀𝑘))) = ((𝑃𝑠)𝑀𝑠))
76 simprr 792 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠 ∈ dom (𝑃 ∖ I ))
7711ad2antrl 760 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃 Fn 𝑁)
78 fnelnfp 6326 . . . . . . . . . . . . . . 15 ((𝑃 Fn 𝑁𝑠𝑁) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃𝑠) ≠ 𝑠))
7977, 54, 78syl2anc 691 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑠 ∈ dom (𝑃 ∖ I ) ↔ (𝑃𝑠) ≠ 𝑠))
8076, 79mpbid 221 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃𝑠) ≠ 𝑠)
8139ad2antrl 760 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑃:𝑁𝑁)
8239adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → 𝑃:𝑁𝑁)
8382, 50syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → dom 𝑃 = 𝑁)
8448, 83syl5sseq 3616 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → dom (𝑃 ∖ I ) ⊆ 𝑁)
8584sseld 3567 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → 𝑠𝑁))
8685impr 647 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑠𝑁)
8781, 86ffvelrnd 6253 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝑃𝑠) ∈ 𝑁)
88 neeq1 2844 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑃𝑠) → (𝑖𝑗 ↔ (𝑃𝑠) ≠ 𝑗))
89 oveq1 6534 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑃𝑠) → (𝑖𝑀𝑗) = ((𝑃𝑠)𝑀𝑗))
9089eqeq1d 2612 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑃𝑠) → ((𝑖𝑀𝑗) = 0 ↔ ((𝑃𝑠)𝑀𝑗) = 0 ))
9188, 90imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑃𝑠) → ((𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ↔ ((𝑃𝑠) ≠ 𝑗 → ((𝑃𝑠)𝑀𝑗) = 0 )))
92 neeq2 2845 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑠 → ((𝑃𝑠) ≠ 𝑗 ↔ (𝑃𝑠) ≠ 𝑠))
93 oveq2 6535 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑠 → ((𝑃𝑠)𝑀𝑗) = ((𝑃𝑠)𝑀𝑠))
9493eqeq1d 2612 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑠 → (((𝑃𝑠)𝑀𝑗) = 0 ↔ ((𝑃𝑠)𝑀𝑠) = 0 ))
9592, 94imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑠 → (((𝑃𝑠) ≠ 𝑗 → ((𝑃𝑠)𝑀𝑗) = 0 ) ↔ ((𝑃𝑠) ≠ 𝑠 → ((𝑃𝑠)𝑀𝑠) = 0 )))
9691, 95rspc2v 3293 . . . . . . . . . . . . . . . 16 (((𝑃𝑠) ∈ 𝑁𝑠𝑁) → (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃𝑠) ≠ 𝑠 → ((𝑃𝑠)𝑀𝑠) = 0 )))
9787, 86, 96syl2anc 691 . . . . . . . . . . . . . . 15 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) → ((𝑃𝑠) ≠ 𝑠 → ((𝑃𝑠)𝑀𝑠) = 0 )))
9897impancom 455 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) → ((𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I )) → ((𝑃𝑠) ≠ 𝑠 → ((𝑃𝑠)𝑀𝑠) = 0 )))
9998imp 444 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃𝑠) ≠ 𝑠 → ((𝑃𝑠)𝑀𝑠) = 0 ))
10080, 99mpd 15 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝑃𝑠)𝑀𝑠) = 0 )
10175, 100eqtrd 2644 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃𝑘)𝑀𝑘))) = 0 )
102101oveq1d 6542 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ((𝐺 Σg (𝑘 ∈ {𝑠} ↦ ((𝑃𝑘)𝑀𝑘)))(.r𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘)))) = ( 0 (.r𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘)))))
103603ad2ant1 1075 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → 𝑅 ∈ Ring)
104103ad2antrr 758 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → 𝑅 ∈ Ring)
10523adantr 480 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → 𝐺 ∈ CMnd)
106 simpl2 1058 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → 𝑁 ∈ Fin)
107 difss 3699 . . . . . . . . . . . . . 14 (𝑁 ∖ {𝑠}) ⊆ 𝑁
108 ssfi 8043 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ (𝑁 ∖ {𝑠}) ⊆ 𝑁) → (𝑁 ∖ {𝑠}) ∈ Fin)
109106, 107, 108sylancl 693 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → (𝑁 ∖ {𝑠}) ∈ Fin)
11032ad2antrr 758 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑀:(𝑁 × 𝑁)⟶(Base‘𝑅))
11182adantr 480 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑃:𝑁𝑁)
112 eldifi 3694 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝑁 ∖ {𝑠}) → 𝑘𝑁)
113112adantl 481 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → 𝑘𝑁)
114111, 113ffvelrnd 6253 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → (𝑃𝑘) ∈ 𝑁)
115110, 114, 113fovrnd 6682 . . . . . . . . . . . . . 14 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) ∧ 𝑘 ∈ (𝑁 ∖ {𝑠})) → ((𝑃𝑘)𝑀𝑘) ∈ (Base‘𝑅))
116115ralrimiva 2949 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → ∀𝑘 ∈ (𝑁 ∖ {𝑠})((𝑃𝑘)𝑀𝑘) ∈ (Base‘𝑅))
11733, 105, 109, 116gsummptcl 18138 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ 𝑃𝐻) → (𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
118117ad2ant2r 779 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘))) ∈ (Base‘𝑅))
119 mdetdiag.0 . . . . . . . . . . . 12 0 = (0g𝑅)
12027, 20, 119ringlz 18359 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘))) ∈ (Base‘𝑅)) → ( 0 (.r𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘)))) = 0 )
121104, 118, 120syl2anc 691 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → ( 0 (.r𝑅)(𝐺 Σg (𝑘 ∈ (𝑁 ∖ {𝑠}) ↦ ((𝑃𝑘)𝑀𝑘)))) = 0 )
12259, 102, 1213eqtrd 2648 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ (𝑃𝐻𝑠 ∈ dom (𝑃 ∖ I ))) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 )
123122expr 641 . . . . . . . 8 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 ))
124123exlimdv 1848 . . . . . . 7 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (∃𝑠 𝑠 ∈ dom (𝑃 ∖ I ) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 ))
12517, 124syl5bi 231 . . . . . 6 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (dom (𝑃 ∖ I ) ≠ ∅ → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 ))
12616, 125sylbid 229 . . . . 5 ((((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) ∧ 𝑃𝐻) → (𝑃 ≠ ( I ↾ 𝑁) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 ))
127126expimpd 627 . . . 4 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 )) → ((𝑃𝐻𝑃 ≠ ( I ↾ 𝑁)) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 ))
1281273impia 1253 . . 3 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘))) = 0 )
1296, 128oveq12d 6545 . 2 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍𝑆)‘𝑃) · (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘)))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ))
130 3simpa 1051 . . . 4 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) → (𝑅 ∈ CRing ∧ 𝑁 ∈ Fin))
131 simpl 472 . . . 4 ((𝑃𝐻𝑃 ≠ ( I ↾ 𝑁)) → 𝑃𝐻)
13260ad2antrr 758 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃𝐻) → 𝑅 ∈ Ring)
133 zrhpsgnmhm 19697 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
13460, 133sylan 487 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
135 eqid 2610 . . . . . . . 8 (Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅))
1368, 135mhmf 17112 . . . . . . 7 (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):𝐻⟶(Base‘(mulGrp‘𝑅)))
137134, 136syl 17 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):𝐻⟶(Base‘(mulGrp‘𝑅)))
138137ffvelrnda 6252 . . . . 5 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃𝐻) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅)))
139 eqid 2610 . . . . . . . 8 (mulGrp‘𝑅) = (mulGrp‘𝑅)
140139, 27mgpbas 18267 . . . . . . 7 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
141140eqcomi 2619 . . . . . 6 (Base‘(mulGrp‘𝑅)) = (Base‘𝑅)
142 mdetdiaglem.t . . . . . 6 · = (.r𝑅)
143141, 142, 119ringrz 18360 . . . . 5 ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) ∈ (Base‘(mulGrp‘𝑅))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
144132, 138, 143syl2anc 691 . . . 4 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ 𝑃𝐻) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
145130, 131, 144syl2an 493 . . 3 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
1461453adant2 1073 . 2 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑃) · 0 ) = 0 )
147129, 146eqtrd 2644 1 (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀𝐵) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃𝐻𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍𝑆)‘𝑃) · (𝐺 Σg (𝑘𝑁 ↦ ((𝑃𝑘)𝑀𝑘)))) = 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wex 1695  wcel 1977  wne 2780  wral 2896  Vcvv 3173  cdif 3537  cun 3538  cin 3539  wss 3540  c0 3874  {csn 4125  cmpt 4638   I cid 4938   × cxp 5026  dom cdm 5028  cres 5030  ccom 5032   Fn wfn 5785  wf 5786  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  𝑚 cmap 7722  Fincfn 7819  Basecbs 15644  .rcmulr 15718  0gc0g 15872   Σg cgsu 15873  Mndcmnd 17066   MndHom cmhm 17105  SymGrpcsymg 17569  pmSgncpsgn 17681  CMndccmn 17965  mulGrpcmgp 18261  Ringcrg 18319  CRingccrg 18320  ℤRHomczrh 19615   Mat cmat 19980   maDet cmdat 20157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-xor 1457  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-ot 4134  df-uni 4368  df-int 4406  df-iun 4452  df-iin 4453  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-tpos 7217  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-sup 8209  df-oi 8276  df-card 8626  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-rp 11668  df-fz 12156  df-fzo 12293  df-seq 12622  df-exp 12681  df-hash 12938  df-word 13103  df-lsw 13104  df-concat 13105  df-s1 13106  df-substr 13107  df-splice 13108  df-reverse 13109  df-s2 13393  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-0g 15874  df-gsum 15875  df-prds 15880  df-pws 15882  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-mhm 17107  df-submnd 17108  df-grp 17197  df-minusg 17198  df-mulg 17313  df-subg 17363  df-ghm 17430  df-gim 17473  df-cntz 17522  df-oppg 17548  df-symg 17570  df-pmtr 17634  df-psgn 17683  df-cmn 17967  df-abl 17968  df-mgp 18262  df-ur 18274  df-ring 18321  df-cring 18322  df-oppr 18395  df-dvdsr 18413  df-unit 18414  df-invr 18444  df-dvr 18455  df-rnghom 18487  df-drng 18521  df-subrg 18550  df-sra 18942  df-rgmod 18943  df-cnfld 19517  df-zring 19587  df-zrh 19619  df-dsmm 19843  df-frlm 19858  df-mat 19981
This theorem is referenced by:  mdetdiag  20172
  Copyright terms: Public domain W3C validator