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

Theorem mdetralt 21973
Description: The determinant function is alternating regarding rows: if a matrix has two identical rows, its determinant is 0. Corollary 4.9 in [Lang] p. 515. (Contributed by SO, 10-Jul-2018.) (Proof shortened by AV, 23-Jul-2018.)
Hypotheses
Ref Expression
mdetralt.d ๐ท = (๐‘ maDet ๐‘…)
mdetralt.a ๐ด = (๐‘ Mat ๐‘…)
mdetralt.b ๐ต = (Baseโ€˜๐ด)
mdetralt.z 0 = (0gโ€˜๐‘…)
mdetralt.r (๐œ‘ โ†’ ๐‘… โˆˆ CRing)
mdetralt.x (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
mdetralt.i (๐œ‘ โ†’ ๐ผ โˆˆ ๐‘)
mdetralt.j (๐œ‘ โ†’ ๐ฝ โˆˆ ๐‘)
mdetralt.ij (๐œ‘ โ†’ ๐ผ โ‰  ๐ฝ)
mdetralt.eq (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ ๐‘ (๐ผ๐‘‹๐‘Ž) = (๐ฝ๐‘‹๐‘Ž))
Assertion
Ref Expression
mdetralt (๐œ‘ โ†’ (๐ทโ€˜๐‘‹) = 0 )
Distinct variable groups:   ๐ผ,๐‘Ž   ๐ฝ,๐‘Ž   ๐‘,๐‘Ž   ๐‘‹,๐‘Ž
Allowed substitution hints:   ๐œ‘(๐‘Ž)   ๐ด(๐‘Ž)   ๐ต(๐‘Ž)   ๐ท(๐‘Ž)   ๐‘…(๐‘Ž)   0 (๐‘Ž)

Proof of Theorem mdetralt
Dummy variables ๐‘ ๐‘ ๐‘ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetralt.x . . 3 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
2 mdetralt.d . . . 4 ๐ท = (๐‘ maDet ๐‘…)
3 mdetralt.a . . . 4 ๐ด = (๐‘ Mat ๐‘…)
4 mdetralt.b . . . 4 ๐ต = (Baseโ€˜๐ด)
5 eqid 2733 . . . 4 (Baseโ€˜(SymGrpโ€˜๐‘)) = (Baseโ€˜(SymGrpโ€˜๐‘))
6 eqid 2733 . . . 4 (โ„คRHomโ€˜๐‘…) = (โ„คRHomโ€˜๐‘…)
7 eqid 2733 . . . 4 (pmSgnโ€˜๐‘) = (pmSgnโ€˜๐‘)
8 eqid 2733 . . . 4 (.rโ€˜๐‘…) = (.rโ€˜๐‘…)
9 eqid 2733 . . . 4 (mulGrpโ€˜๐‘…) = (mulGrpโ€˜๐‘…)
102, 3, 4, 5, 6, 7, 8, 9mdetleib 21952 . . 3 (๐‘‹ โˆˆ ๐ต โ†’ (๐ทโ€˜๐‘‹) = (๐‘… ฮฃg (๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))))
111, 10syl 17 . 2 (๐œ‘ โ†’ (๐ทโ€˜๐‘‹) = (๐‘… ฮฃg (๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))))
12 eqid 2733 . . 3 (Baseโ€˜๐‘…) = (Baseโ€˜๐‘…)
13 eqid 2733 . . 3 (+gโ€˜๐‘…) = (+gโ€˜๐‘…)
14 mdetralt.r . . . . 5 (๐œ‘ โ†’ ๐‘… โˆˆ CRing)
15 crngring 19981 . . . . 5 (๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring)
1614, 15syl 17 . . . 4 (๐œ‘ โ†’ ๐‘… โˆˆ Ring)
17 ringcmn 20008 . . . 4 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ CMnd)
1816, 17syl 17 . . 3 (๐œ‘ โ†’ ๐‘… โˆˆ CMnd)
193, 4matrcl 21775 . . . . . 6 (๐‘‹ โˆˆ ๐ต โ†’ (๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ V))
201, 19syl 17 . . . . 5 (๐œ‘ โ†’ (๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ V))
2120simpld 496 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ Fin)
22 eqid 2733 . . . . 5 (SymGrpโ€˜๐‘) = (SymGrpโ€˜๐‘)
2322, 5symgbasfi 19165 . . . 4 (๐‘ โˆˆ Fin โ†’ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆˆ Fin)
2421, 23syl 17 . . 3 (๐œ‘ โ†’ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆˆ Fin)
2516adantr 482 . . . 4 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ๐‘… โˆˆ Ring)
26 zrhpsgnmhm 21004 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin) โ†’ ((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)) โˆˆ ((SymGrpโ€˜๐‘) MndHom (mulGrpโ€˜๐‘…)))
2716, 21, 26syl2anc 585 . . . . . 6 (๐œ‘ โ†’ ((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)) โˆˆ ((SymGrpโ€˜๐‘) MndHom (mulGrpโ€˜๐‘…)))
289, 12mgpbas 19907 . . . . . . 7 (Baseโ€˜๐‘…) = (Baseโ€˜(mulGrpโ€˜๐‘…))
295, 28mhmf 18612 . . . . . 6 (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)) โˆˆ ((SymGrpโ€˜๐‘) MndHom (mulGrpโ€˜๐‘…)) โ†’ ((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)):(Baseโ€˜(SymGrpโ€˜๐‘))โŸถ(Baseโ€˜๐‘…))
3027, 29syl 17 . . . . 5 (๐œ‘ โ†’ ((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)):(Baseโ€˜(SymGrpโ€˜๐‘))โŸถ(Baseโ€˜๐‘…))
3130ffvelcdmda 7036 . . . 4 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) โˆˆ (Baseโ€˜๐‘…))
329crngmgp 19977 . . . . . . 7 (๐‘… โˆˆ CRing โ†’ (mulGrpโ€˜๐‘…) โˆˆ CMnd)
3314, 32syl 17 . . . . . 6 (๐œ‘ โ†’ (mulGrpโ€˜๐‘…) โˆˆ CMnd)
3433adantr 482 . . . . 5 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ (mulGrpโ€˜๐‘…) โˆˆ CMnd)
3521adantr 482 . . . . 5 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ๐‘ โˆˆ Fin)
363, 12, 4matbas2i 21787 . . . . . . . . . 10 (๐‘‹ โˆˆ ๐ต โ†’ ๐‘‹ โˆˆ ((Baseโ€˜๐‘…) โ†‘m (๐‘ ร— ๐‘)))
371, 36syl 17 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‹ โˆˆ ((Baseโ€˜๐‘…) โ†‘m (๐‘ ร— ๐‘)))
38 elmapi 8790 . . . . . . . . 9 (๐‘‹ โˆˆ ((Baseโ€˜๐‘…) โ†‘m (๐‘ ร— ๐‘)) โ†’ ๐‘‹:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘…))
3937, 38syl 17 . . . . . . . 8 (๐œ‘ โ†’ ๐‘‹:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘…))
4039ad2antrr 725 . . . . . . 7 (((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘‹:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘…))
4122, 5symgbasf1o 19161 . . . . . . . . . 10 (๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†’ ๐‘:๐‘โ€“1-1-ontoโ†’๐‘)
4241adantl 483 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ๐‘:๐‘โ€“1-1-ontoโ†’๐‘)
43 f1of 6785 . . . . . . . . 9 (๐‘:๐‘โ€“1-1-ontoโ†’๐‘ โ†’ ๐‘:๐‘โŸถ๐‘)
4442, 43syl 17 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ๐‘:๐‘โŸถ๐‘)
4544ffvelcdmda 7036 . . . . . . 7 (((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐‘โ€˜๐‘) โˆˆ ๐‘)
46 simpr 486 . . . . . . 7 (((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘ โˆˆ ๐‘)
4740, 45, 46fovcdmd 7527 . . . . . 6 (((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘)๐‘‹๐‘) โˆˆ (Baseโ€˜๐‘…))
4847ralrimiva 3140 . . . . 5 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ โˆ€๐‘ โˆˆ ๐‘ ((๐‘โ€˜๐‘)๐‘‹๐‘) โˆˆ (Baseโ€˜๐‘…))
4928, 34, 35, 48gsummptcl 19749 . . . 4 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…))
5012, 8ringcl 19986 . . . 4 ((๐‘… โˆˆ Ring โˆง (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) โˆˆ (Baseโ€˜๐‘…) โˆง ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) โˆˆ (Baseโ€˜๐‘…))
5125, 31, 49, 50syl3anc 1372 . . 3 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) โˆˆ (Baseโ€˜๐‘…))
52 disjdif 4432 . . . 4 ((pmEvenโ€˜๐‘) โˆฉ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) = โˆ…
5352a1i 11 . . 3 (๐œ‘ โ†’ ((pmEvenโ€˜๐‘) โˆฉ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) = โˆ…)
5422, 5evpmss 21006 . . . . . 6 (pmEvenโ€˜๐‘) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘))
55 undif 4442 . . . . . 6 ((pmEvenโ€˜๐‘) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘)) โ†” ((pmEvenโ€˜๐‘) โˆช ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) = (Baseโ€˜(SymGrpโ€˜๐‘)))
5654, 55mpbi 229 . . . . 5 ((pmEvenโ€˜๐‘) โˆช ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) = (Baseโ€˜(SymGrpโ€˜๐‘))
5756eqcomi 2742 . . . 4 (Baseโ€˜(SymGrpโ€˜๐‘)) = ((pmEvenโ€˜๐‘) โˆช ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
5857a1i 11 . . 3 (๐œ‘ โ†’ (Baseโ€˜(SymGrpโ€˜๐‘)) = ((pmEvenโ€˜๐‘) โˆช ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))))
59 eqid 2733 . . 3 (๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) = (๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
6012, 13, 18, 24, 51, 53, 58, 59gsummptfidmsplitres 19713 . 2 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))) = ((๐‘… ฮฃg ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ (pmEvenโ€˜๐‘)))(+gโ€˜๐‘…)(๐‘… ฮฃg ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))))))
61 resmpt 5992 . . . . . . 7 ((pmEvenโ€˜๐‘) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘)) โ†’ ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ (pmEvenโ€˜๐‘)) = (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
6254, 61ax-mp 5 . . . . . 6 ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ (pmEvenโ€˜๐‘)) = (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
6316adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ๐‘… โˆˆ Ring)
6421adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ๐‘ โˆˆ Fin)
65 simpr 486 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ๐‘ โˆˆ (pmEvenโ€˜๐‘))
66 eqid 2733 . . . . . . . . . . 11 (1rโ€˜๐‘…) = (1rโ€˜๐‘…)
676, 7, 66zrhpsgnevpm 21011 . . . . . . . . . 10 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) = (1rโ€˜๐‘…))
6863, 64, 65, 67syl3anc 1372 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) = (1rโ€˜๐‘…))
6968oveq1d 7373 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = ((1rโ€˜๐‘…)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
7054sseli 3941 . . . . . . . . . 10 (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†’ ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
7170, 49sylan2 594 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…))
7212, 8, 66ringlidm 19997 . . . . . . . . 9 ((๐‘… โˆˆ Ring โˆง ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((1rโ€˜๐‘…)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))
7363, 71, 72syl2anc 585 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((1rโ€˜๐‘…)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))
7469, 73eqtrd 2773 . . . . . . 7 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))
7574mpteq2dva 5206 . . . . . 6 (๐œ‘ โ†’ (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) = (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
7662, 75eqtrid 2785 . . . . 5 (๐œ‘ โ†’ ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ (pmEvenโ€˜๐‘)) = (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
7776oveq2d 7374 . . . 4 (๐œ‘ โ†’ (๐‘… ฮฃg ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ (pmEvenโ€˜๐‘))) = (๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
78 difss 4092 . . . . . . . 8 ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘))
79 resmpt 5992 . . . . . . . 8 (((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘)) โ†’ ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) = (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
8078, 79ax-mp 5 . . . . . . 7 ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) = (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
8116adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ ๐‘… โˆˆ Ring)
8221adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ ๐‘ โˆˆ Fin)
83 simpr 486 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
84 eqid 2733 . . . . . . . . . . . . 13 (invgโ€˜๐‘…) = (invgโ€˜๐‘…)
856, 7, 66, 5, 84zrhpsgnodpm 21012 . . . . . . . . . . . 12 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) = ((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…)))
8681, 82, 83, 85syl3anc 1372 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) = ((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…)))
8786oveq1d 7373 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = (((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…))(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
88 eldifi 4087 . . . . . . . . . . . 12 (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†’ ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
8988, 49sylan2 594 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…))
9012, 8, 66, 84, 81, 89ringnegl 20023 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ (((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…))(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = ((invgโ€˜๐‘…)โ€˜((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
9187, 90eqtrd 2773 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = ((invgโ€˜๐‘…)โ€˜((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
9291mpteq2dva 5206 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) = (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((invgโ€˜๐‘…)โ€˜((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
93 ringgrp 19974 . . . . . . . . . . 11 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Grp)
9416, 93syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘… โˆˆ Grp)
9512, 84grpinvf 18802 . . . . . . . . . 10 (๐‘… โˆˆ Grp โ†’ (invgโ€˜๐‘…):(Baseโ€˜๐‘…)โŸถ(Baseโ€˜๐‘…))
9694, 95syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (invgโ€˜๐‘…):(Baseโ€˜๐‘…)โŸถ(Baseโ€˜๐‘…))
9796, 89cofmpt 7079 . . . . . . . 8 (๐œ‘ โ†’ ((invgโ€˜๐‘…) โˆ˜ (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) = (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((invgโ€˜๐‘…)โ€˜((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
9892, 97eqtr4d 2776 . . . . . . 7 (๐œ‘ โ†’ (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) = ((invgโ€˜๐‘…) โˆ˜ (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
9980, 98eqtrid 2785 . . . . . 6 (๐œ‘ โ†’ ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) = ((invgโ€˜๐‘…) โˆ˜ (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
10099oveq2d 7374 . . . . 5 (๐œ‘ โ†’ (๐‘… ฮฃg ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))) = (๐‘… ฮฃg ((invgโ€˜๐‘…) โˆ˜ (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))))
101 mdetralt.z . . . . . 6 0 = (0gโ€˜๐‘…)
102 ringabl 20007 . . . . . . 7 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Abel)
10316, 102syl 17 . . . . . 6 (๐œ‘ โ†’ ๐‘… โˆˆ Abel)
104 difssd 4093 . . . . . . 7 (๐œ‘ โ†’ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘)))
10524, 104ssfid 9214 . . . . . 6 (๐œ‘ โ†’ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โˆˆ Fin)
106 eqid 2733 . . . . . 6 (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))
10712, 101, 84, 103, 105, 89, 106gsummptfidminv 19729 . . . . 5 (๐œ‘ โ†’ (๐‘… ฮฃg ((invgโ€˜๐‘…) โˆ˜ (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))) = ((invgโ€˜๐‘…)โ€˜(๐‘… ฮฃg (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))))
10889ralrimiva 3140 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…))
109 mdetralt.i . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ผ โˆˆ ๐‘)
110 mdetralt.j . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ฝ โˆˆ ๐‘)
111109, 110prssd 4783 . . . . . . . . . . 11 (๐œ‘ โ†’ {๐ผ, ๐ฝ} โŠ† ๐‘)
112 mdetralt.ij . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ผ โ‰  ๐ฝ)
113 enpr2 9943 . . . . . . . . . . . 12 ((๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ โˆง ๐ผ โ‰  ๐ฝ) โ†’ {๐ผ, ๐ฝ} โ‰ˆ 2o)
114109, 110, 112, 113syl3anc 1372 . . . . . . . . . . 11 (๐œ‘ โ†’ {๐ผ, ๐ฝ} โ‰ˆ 2o)
115 eqid 2733 . . . . . . . . . . . 12 (pmTrspโ€˜๐‘) = (pmTrspโ€˜๐‘)
116 eqid 2733 . . . . . . . . . . . 12 ran (pmTrspโ€˜๐‘) = ran (pmTrspโ€˜๐‘)
117115, 116pmtrrn 19244 . . . . . . . . . . 11 ((๐‘ โˆˆ Fin โˆง {๐ผ, ๐ฝ} โŠ† ๐‘ โˆง {๐ผ, ๐ฝ} โ‰ˆ 2o) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ran (pmTrspโ€˜๐‘))
11821, 111, 114, 117syl3anc 1372 . . . . . . . . . 10 (๐œ‘ โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ran (pmTrspโ€˜๐‘))
11922, 5, 116pmtrodpm 21017 . . . . . . . . . 10 ((๐‘ โˆˆ Fin โˆง ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ran (pmTrspโ€˜๐‘)) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
12021, 118, 119syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
12122, 5evpmodpmf1o 21016 . . . . . . . . 9 ((๐‘ โˆˆ Fin โˆง ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)):(pmEvenโ€˜๐‘)โ€“1-1-ontoโ†’((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
12221, 120, 121syl2anc 585 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)):(pmEvenโ€˜๐‘)โ€“1-1-ontoโ†’((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
12312, 18, 105, 108, 106, 122gsummptfif1o 19750 . . . . . . 7 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) = (๐‘… ฮฃg ((๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) โˆ˜ (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)))))
124 eleq1w 2817 . . . . . . . . . . . . 13 (๐‘ = ๐‘ž โ†’ (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†” ๐‘ž โˆˆ (pmEvenโ€˜๐‘)))
125124anbi2d 630 . . . . . . . . . . . 12 (๐‘ = ๐‘ž โ†’ ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†” (๐œ‘ โˆง ๐‘ž โˆˆ (pmEvenโ€˜๐‘))))
126 oveq2 7366 . . . . . . . . . . . . 13 (๐‘ = ๐‘ž โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž))
127126eleq1d 2819 . . . . . . . . . . . 12 (๐‘ = ๐‘ž โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†” (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))))
128125, 127imbi12d 345 . . . . . . . . . . 11 (๐‘ = ๐‘ž โ†’ (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†” ((๐œ‘ โˆง ๐‘ž โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))))
12922symggrp 19187 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ Fin โ†’ (SymGrpโ€˜๐‘) โˆˆ Grp)
13021, 129syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (SymGrpโ€˜๐‘) โˆˆ Grp)
131130adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (SymGrpโ€˜๐‘) โˆˆ Grp)
132116, 22, 5symgtrf 19256 . . . . . . . . . . . . . 14 ran (pmTrspโ€˜๐‘) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘))
133118adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ran (pmTrspโ€˜๐‘))
134132, 133sselid 3943 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
13570adantl 483 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
136 eqid 2733 . . . . . . . . . . . . . 14 (+gโ€˜(SymGrpโ€˜๐‘)) = (+gโ€˜(SymGrpโ€˜๐‘))
1375, 136grpcl 18761 . . . . . . . . . . . . 13 (((SymGrpโ€˜๐‘) โˆˆ Grp โˆง ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
138131, 134, 135, 137syl3anc 1372 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
139 eqid 2733 . . . . . . . . . . . . . . . . 17 ((mulGrpโ€˜โ„‚fld) โ†พs {1, -1}) = ((mulGrpโ€˜โ„‚fld) โ†พs {1, -1})
14022, 7, 139psgnghm2 21001 . . . . . . . . . . . . . . . 16 (๐‘ โˆˆ Fin โ†’ (pmSgnโ€˜๐‘) โˆˆ ((SymGrpโ€˜๐‘) GrpHom ((mulGrpโ€˜โ„‚fld) โ†พs {1, -1})))
14121, 140syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (pmSgnโ€˜๐‘) โˆˆ ((SymGrpโ€˜๐‘) GrpHom ((mulGrpโ€˜โ„‚fld) โ†พs {1, -1})))
142141adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (pmSgnโ€˜๐‘) โˆˆ ((SymGrpโ€˜๐‘) GrpHom ((mulGrpโ€˜โ„‚fld) โ†พs {1, -1})))
143 prex 5390 . . . . . . . . . . . . . . . 16 {1, -1} โˆˆ V
144 eqid 2733 . . . . . . . . . . . . . . . . . 18 (mulGrpโ€˜โ„‚fld) = (mulGrpโ€˜โ„‚fld)
145 cnfldmul 20818 . . . . . . . . . . . . . . . . . 18 ยท = (.rโ€˜โ„‚fld)
146144, 145mgpplusg 19905 . . . . . . . . . . . . . . . . 17 ยท = (+gโ€˜(mulGrpโ€˜โ„‚fld))
147139, 146ressplusg 17176 . . . . . . . . . . . . . . . 16 ({1, -1} โˆˆ V โ†’ ยท = (+gโ€˜((mulGrpโ€˜โ„‚fld) โ†พs {1, -1})))
148143, 147ax-mp 5 . . . . . . . . . . . . . . 15 ยท = (+gโ€˜((mulGrpโ€˜โ„‚fld) โ†พs {1, -1}))
1495, 136, 148ghmlin 19018 . . . . . . . . . . . . . 14 (((pmSgnโ€˜๐‘) โˆˆ ((SymGrpโ€˜๐‘) GrpHom ((mulGrpโ€˜โ„‚fld) โ†พs {1, -1})) โˆง ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((pmSgnโ€˜๐‘)โ€˜(((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)) = (((pmSgnโ€˜๐‘)โ€˜((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})) ยท ((pmSgnโ€˜๐‘)โ€˜๐‘)))
150142, 134, 135, 149syl3anc 1372 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmSgnโ€˜๐‘)โ€˜(((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)) = (((pmSgnโ€˜๐‘)โ€˜((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})) ยท ((pmSgnโ€˜๐‘)โ€˜๐‘)))
15122, 116, 7psgnpmtr 19297 . . . . . . . . . . . . . . . 16 (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ran (pmTrspโ€˜๐‘) โ†’ ((pmSgnโ€˜๐‘)โ€˜((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})) = -1)
152133, 151syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmSgnโ€˜๐‘)โ€˜((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})) = -1)
15322, 5, 7psgnevpm 21009 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ Fin โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmSgnโ€˜๐‘)โ€˜๐‘) = 1)
15421, 153sylan 581 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmSgnโ€˜๐‘)โ€˜๐‘) = 1)
155152, 154oveq12d 7376 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((pmSgnโ€˜๐‘)โ€˜((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})) ยท ((pmSgnโ€˜๐‘)โ€˜๐‘)) = (-1 ยท 1))
156 neg1cn 12272 . . . . . . . . . . . . . . 15 -1 โˆˆ โ„‚
157156mulid1i 11164 . . . . . . . . . . . . . 14 (-1 ยท 1) = -1
158155, 157eqtrdi 2789 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((pmSgnโ€˜๐‘)โ€˜((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})) ยท ((pmSgnโ€˜๐‘)โ€˜๐‘)) = -1)
159150, 158eqtrd 2773 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmSgnโ€˜๐‘)โ€˜(((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)) = -1)
16022, 5, 7psgnodpmr 21010 . . . . . . . . . . . 12 ((๐‘ โˆˆ Fin โˆง (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆง ((pmSgnโ€˜๐‘)โ€˜(((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)) = -1) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
16164, 138, 159, 160syl3anc 1372 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
162128, 161chvarvv 2003 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ž โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
163 eqidd 2734 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)) = (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)))
164 eqidd 2734 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
165 fveq1 6842 . . . . . . . . . . . . 13 (๐‘ = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โ†’ (๐‘โ€˜๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘))
166165oveq1d 7373 . . . . . . . . . . . 12 (๐‘ = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โ†’ ((๐‘โ€˜๐‘)๐‘‹๐‘) = (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘))
167166mpteq2dv 5208 . . . . . . . . . . 11 (๐‘ = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)) = (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘)))
168167oveq2d 7374 . . . . . . . . . 10 (๐‘ = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘))))
169162, 163, 164, 168fmptco 7076 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) โˆ˜ (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž))) = (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘)))))
170 oveq2 7366 . . . . . . . . . . . . . . 15 (๐‘ž = ๐‘ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘))
171170fveq1d 6845 . . . . . . . . . . . . . 14 (๐‘ž = ๐‘ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘))
172171oveq1d 7373 . . . . . . . . . . . . 13 (๐‘ž = ๐‘ โ†’ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘) = (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘))
173172mpteq2dv 5208 . . . . . . . . . . . 12 (๐‘ž = ๐‘ โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘)) = (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘)))
174173oveq2d 7374 . . . . . . . . . . 11 (๐‘ž = ๐‘ โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘))))
175174cbvmptv 5219 . . . . . . . . . 10 (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘)))) = (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘))))
176175a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘)))) = (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘)))))
177134adantr 482 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
178135adantr 482 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
17922, 5, 136symgov 19170 . . . . . . . . . . . . . . . . 17 ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ˜ ๐‘))
180177, 178, 179syl2anc 585 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ˜ ๐‘))
181180fveq1d 6845 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ˜ ๐‘)โ€˜๐‘))
18270, 44sylan2 594 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ๐‘:๐‘โŸถ๐‘)
183 fvco3 6941 . . . . . . . . . . . . . . . 16 ((๐‘:๐‘โŸถ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ˜ ๐‘)โ€˜๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)))
184182, 183sylan 581 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ˜ ๐‘)โ€˜๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)))
185181, 184eqtrd 2773 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)))
186185oveq1d 7373 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘))
187115pmtrprfv 19240 . . . . . . . . . . . . . . . . . . 19 ((๐‘ โˆˆ Fin โˆง (๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ โˆง ๐ผ โ‰  ๐ฝ)) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ) = ๐ฝ)
18821, 109, 110, 112, 187syl13anc 1373 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ) = ๐ฝ)
189188ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ) = ๐ฝ)
190189oveq1d 7373 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ)๐‘‹๐‘) = (๐ฝ๐‘‹๐‘))
191 oveq2 7366 . . . . . . . . . . . . . . . . . 18 (๐‘Ž = ๐‘ โ†’ (๐ผ๐‘‹๐‘Ž) = (๐ผ๐‘‹๐‘))
192 oveq2 7366 . . . . . . . . . . . . . . . . . 18 (๐‘Ž = ๐‘ โ†’ (๐ฝ๐‘‹๐‘Ž) = (๐ฝ๐‘‹๐‘))
193191, 192eqeq12d 2749 . . . . . . . . . . . . . . . . 17 (๐‘Ž = ๐‘ โ†’ ((๐ผ๐‘‹๐‘Ž) = (๐ฝ๐‘‹๐‘Ž) โ†” (๐ผ๐‘‹๐‘) = (๐ฝ๐‘‹๐‘)))
194 mdetralt.eq . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ ๐‘ (๐ผ๐‘‹๐‘Ž) = (๐ฝ๐‘‹๐‘Ž))
195194ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ โˆ€๐‘Ž โˆˆ ๐‘ (๐ผ๐‘‹๐‘Ž) = (๐ฝ๐‘‹๐‘Ž))
196 simpr 486 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘ โˆˆ ๐‘)
197193, 195, 196rspcdva 3581 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐ผ๐‘‹๐‘) = (๐ฝ๐‘‹๐‘))
198190, 197eqtr4d 2776 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ)๐‘‹๐‘) = (๐ผ๐‘‹๐‘))
199 fveq2 6843 . . . . . . . . . . . . . . . . 17 ((๐‘โ€˜๐‘) = ๐ผ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ))
200199oveq1d 7373 . . . . . . . . . . . . . . . 16 ((๐‘โ€˜๐‘) = ๐ผ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ)๐‘‹๐‘))
201 oveq1 7365 . . . . . . . . . . . . . . . 16 ((๐‘โ€˜๐‘) = ๐ผ โ†’ ((๐‘โ€˜๐‘)๐‘‹๐‘) = (๐ผ๐‘‹๐‘))
202200, 201eqeq12d 2749 . . . . . . . . . . . . . . 15 ((๐‘โ€˜๐‘) = ๐ผ โ†’ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘) โ†” ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ)๐‘‹๐‘) = (๐ผ๐‘‹๐‘)))
203198, 202syl5ibrcom 247 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) = ๐ผ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘)))
204 prcom 4694 . . . . . . . . . . . . . . . . . . . . . . 23 {๐ผ, ๐ฝ} = {๐ฝ, ๐ผ}
205204fveq2i 6846 . . . . . . . . . . . . . . . . . . . . . 22 ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) = ((pmTrspโ€˜๐‘)โ€˜{๐ฝ, ๐ผ})
206205fveq1i 6844 . . . . . . . . . . . . . . . . . . . . 21 (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ) = (((pmTrspโ€˜๐‘)โ€˜{๐ฝ, ๐ผ})โ€˜๐ฝ)
207112necomd 2996 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ๐ฝ โ‰  ๐ผ)
208115pmtrprfv 19240 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ โˆˆ Fin โˆง (๐ฝ โˆˆ ๐‘ โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โ‰  ๐ผ)) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ฝ, ๐ผ})โ€˜๐ฝ) = ๐ผ)
20921, 110, 109, 207, 208syl13anc 1373 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ฝ, ๐ผ})โ€˜๐ฝ) = ๐ผ)
210206, 209eqtrid 2785 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ) = ๐ผ)
211210oveq1d 7373 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ)๐‘‹๐‘) = (๐ผ๐‘‹๐‘))
212211ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ)๐‘‹๐‘) = (๐ผ๐‘‹๐‘))
213212, 197eqtrd 2773 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ)๐‘‹๐‘) = (๐ฝ๐‘‹๐‘))
214 fveq2 6843 . . . . . . . . . . . . . . . . . . 19 ((๐‘โ€˜๐‘) = ๐ฝ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ))
215214oveq1d 7373 . . . . . . . . . . . . . . . . . 18 ((๐‘โ€˜๐‘) = ๐ฝ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ)๐‘‹๐‘))
216 oveq1 7365 . . . . . . . . . . . . . . . . . 18 ((๐‘โ€˜๐‘) = ๐ฝ โ†’ ((๐‘โ€˜๐‘)๐‘‹๐‘) = (๐ฝ๐‘‹๐‘))
217215, 216eqeq12d 2749 . . . . . . . . . . . . . . . . 17 ((๐‘โ€˜๐‘) = ๐ฝ โ†’ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘) โ†” ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ)๐‘‹๐‘) = (๐ฝ๐‘‹๐‘)))
218213, 217syl5ibrcom 247 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) = ๐ฝ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘)))
219218a1dd 50 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) = ๐ฝ โ†’ ((๐‘โ€˜๐‘) โ‰  ๐ผ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘))))
220 neanior 3034 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†” ยฌ ((๐‘โ€˜๐‘) = ๐ฝ โˆจ (๐‘โ€˜๐‘) = ๐ผ))
221 elpri 4609 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘โ€˜๐‘) โˆˆ {๐ผ, ๐ฝ} โ†’ ((๐‘โ€˜๐‘) = ๐ผ โˆจ (๐‘โ€˜๐‘) = ๐ฝ))
222221orcomd 870 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘โ€˜๐‘) โˆˆ {๐ผ, ๐ฝ} โ†’ ((๐‘โ€˜๐‘) = ๐ฝ โˆจ (๐‘โ€˜๐‘) = ๐ผ))
223222con3i 154 . . . . . . . . . . . . . . . . . . . . 21 (ยฌ ((๐‘โ€˜๐‘) = ๐ฝ โˆจ (๐‘โ€˜๐‘) = ๐ผ) โ†’ ยฌ (๐‘โ€˜๐‘) โˆˆ {๐ผ, ๐ฝ})
224220, 223sylbi 216 . . . . . . . . . . . . . . . . . . . 20 (((๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ ยฌ (๐‘โ€˜๐‘) โˆˆ {๐ผ, ๐ฝ})
2252243adant1 1131 . . . . . . . . . . . . . . . . . . 19 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ ยฌ (๐‘โ€˜๐‘) โˆˆ {๐ผ, ๐ฝ})
226115pmtrmvd 19243 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ โˆˆ Fin โˆง {๐ผ, ๐ฝ} โŠ† ๐‘ โˆง {๐ผ, ๐ฝ} โ‰ˆ 2o) โ†’ dom (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ– I ) = {๐ผ, ๐ฝ})
22721, 111, 114, 226syl3anc 1372 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ dom (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ– I ) = {๐ผ, ๐ฝ})
228227ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ dom (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ– I ) = {๐ผ, ๐ฝ})
2292283ad2ant1 1134 . . . . . . . . . . . . . . . . . . 19 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ dom (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ– I ) = {๐ผ, ๐ฝ})
230225, 229neleqtrrd 2857 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ ยฌ (๐‘โ€˜๐‘) โˆˆ dom (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ– I ))
231115pmtrf 19242 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ โˆˆ Fin โˆง {๐ผ, ๐ฝ} โŠ† ๐‘ โˆง {๐ผ, ๐ฝ} โ‰ˆ 2o) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}):๐‘โŸถ๐‘)
23221, 111, 114, 231syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}):๐‘โŸถ๐‘)
233232ffnd 6670 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) Fn ๐‘)
234233ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) Fn ๐‘)
235182ffvelcdmda 7036 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐‘โ€˜๐‘) โˆˆ ๐‘)
236 fnelnfp 7124 . . . . . . . . . . . . . . . . . . . . 21 ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) Fn ๐‘ โˆง (๐‘โ€˜๐‘) โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) โˆˆ dom (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ– I ) โ†” (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) โ‰  (๐‘โ€˜๐‘)))
237234, 235, 236syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) โˆˆ dom (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ– I ) โ†” (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) โ‰  (๐‘โ€˜๐‘)))
2382373ad2ant1 1134 . . . . . . . . . . . . . . . . . . 19 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ ((๐‘โ€˜๐‘) โˆˆ dom (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ– I ) โ†” (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) โ‰  (๐‘โ€˜๐‘)))
239238necon2bbid 2984 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) = (๐‘โ€˜๐‘) โ†” ยฌ (๐‘โ€˜๐‘) โˆˆ dom (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ– I )))
240230, 239mpbird 257 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) = (๐‘โ€˜๐‘))
241240oveq1d 7373 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘))
2422413exp 1120 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) โ‰  ๐ฝ โ†’ ((๐‘โ€˜๐‘) โ‰  ๐ผ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘))))
243219, 242pm2.61dne 3028 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) โ‰  ๐ผ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘)))
244203, 243pm2.61dne 3028 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘))
245186, 244eqtrd 2773 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘))
246245mpteq2dva 5206 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘)) = (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))
247246oveq2d 7374 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))
248247mpteq2dva 5206 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘)))) = (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
249169, 176, 2483eqtrd 2777 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) โˆ˜ (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž))) = (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
250249oveq2d 7374 . . . . . . 7 (๐œ‘ โ†’ (๐‘… ฮฃg ((๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) โˆ˜ (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)))) = (๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
251123, 250eqtrd 2773 . . . . . 6 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) = (๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
252251fveq2d 6847 . . . . 5 (๐œ‘ โ†’ ((invgโ€˜๐‘…)โ€˜(๐‘… ฮฃg (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))) = ((invgโ€˜๐‘…)โ€˜(๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))))
253100, 107, 2523eqtrd 2777 . . . 4 (๐œ‘ โ†’ (๐‘… ฮฃg ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))) = ((invgโ€˜๐‘…)โ€˜(๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))))
25477, 253oveq12d 7376 . . 3 (๐œ‘ โ†’ ((๐‘… ฮฃg ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ (pmEvenโ€˜๐‘)))(+gโ€˜๐‘…)(๐‘… ฮฃg ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))))) = ((๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))(+gโ€˜๐‘…)((invgโ€˜๐‘…)โ€˜(๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))))
25554a1i 11 . . . . . 6 (๐œ‘ โ†’ (pmEvenโ€˜๐‘) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘)))
25624, 255ssfid 9214 . . . . 5 (๐œ‘ โ†’ (pmEvenโ€˜๐‘) โˆˆ Fin)
25771ralrimiva 3140 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘ โˆˆ (pmEvenโ€˜๐‘)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…))
25812, 18, 256, 257gsummptcl 19749 . . . 4 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โˆˆ (Baseโ€˜๐‘…))
25912, 13, 101, 84grprinv 18806 . . . 4 ((๐‘… โˆˆ Grp โˆง (๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))(+gโ€˜๐‘…)((invgโ€˜๐‘…)โ€˜(๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))) = 0 )
26094, 258, 259syl2anc 585 . . 3 (๐œ‘ โ†’ ((๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))(+gโ€˜๐‘…)((invgโ€˜๐‘…)โ€˜(๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))) = 0 )
261254, 260eqtrd 2773 . 2 (๐œ‘ โ†’ ((๐‘… ฮฃg ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ (pmEvenโ€˜๐‘)))(+gโ€˜๐‘…)(๐‘… ฮฃg ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))))) = 0 )
26211, 60, 2613eqtrd 2777 1 (๐œ‘ โ†’ (๐ทโ€˜๐‘‹) = 0 )
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940  โˆ€wral 3061  Vcvv 3444   โˆ– cdif 3908   โˆช cun 3909   โˆฉ cin 3910   โŠ† wss 3911  โˆ…c0 4283  {cpr 4589   class class class wbr 5106   โ†ฆ cmpt 5189   I cid 5531   ร— cxp 5632  dom cdm 5634  ran crn 5635   โ†พ cres 5636   โˆ˜ ccom 5638   Fn wfn 6492  โŸถwf 6493  โ€“1-1-ontoโ†’wf1o 6496  โ€˜cfv 6497  (class class class)co 7358  2oc2o 8407   โ†‘m cmap 8768   โ‰ˆ cen 8883  Fincfn 8886  1c1 11057   ยท cmul 11061  -cneg 11391  Basecbs 17088   โ†พs cress 17117  +gcplusg 17138  .rcmulr 17139  0gc0g 17326   ฮฃg cgsu 17327   MndHom cmhm 18604  Grpcgrp 18753  invgcminusg 18754   GrpHom cghm 19010  SymGrpcsymg 19153  pmTrspcpmtr 19228  pmSgncpsgn 19276  pmEvencevpm 19277  CMndccmn 19567  Abelcabl 19568  mulGrpcmgp 19901  1rcur 19918  Ringcrg 19969  CRingccrg 19970  โ„‚fldccnfld 20812  โ„คRHomczrh 20916   Mat cmat 21770   maDet cmdat 21949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-xor 1511  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-ot 4596  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-tpos 8158  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-sup 9383  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-xnn0 12491  df-z 12505  df-dec 12624  df-uz 12769  df-rp 12921  df-fz 13431  df-fzo 13574  df-seq 13913  df-exp 13974  df-hash 14237  df-word 14409  df-lsw 14457  df-concat 14465  df-s1 14490  df-substr 14535  df-pfx 14565  df-splice 14644  df-reverse 14653  df-s2 14743  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-0g 17328  df-gsum 17329  df-prds 17334  df-pws 17336  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-mhm 18606  df-submnd 18607  df-efmnd 18684  df-grp 18756  df-minusg 18757  df-mulg 18878  df-subg 18930  df-ghm 19011  df-gim 19054  df-cntz 19102  df-oppg 19129  df-symg 19154  df-pmtr 19229  df-psgn 19278  df-evpm 19279  df-cmn 19569  df-abl 19570  df-mgp 19902  df-ur 19919  df-ring 19971  df-cring 19972  df-oppr 20054  df-dvdsr 20075  df-unit 20076  df-invr 20106  df-dvr 20117  df-rnghom 20153  df-drng 20199  df-subrg 20234  df-sra 20649  df-rgmod 20650  df-cnfld 20813  df-zring 20886  df-zrh 20920  df-dsmm 21154  df-frlm 21169  df-mat 21771  df-mdet 21950
This theorem is referenced by:  mdetralt2  21974  mdetuni0  21986  mdetmul  21988
  Copyright terms: Public domain W3C validator