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

Theorem mdetralt 22110
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 22089 . . 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 20068 . . . . 5 (๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring)
1614, 15syl 17 . . . 4 (๐œ‘ โ†’ ๐‘… โˆˆ Ring)
17 ringcmn 20099 . . . 4 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ CMnd)
1816, 17syl 17 . . 3 (๐œ‘ โ†’ ๐‘… โˆˆ CMnd)
193, 4matrcl 21912 . . . . . 6 (๐‘‹ โˆˆ ๐ต โ†’ (๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ V))
201, 19syl 17 . . . . 5 (๐œ‘ โ†’ (๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ V))
2120simpld 496 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ Fin)
22 eqid 2733 . . . . 5 (SymGrpโ€˜๐‘) = (SymGrpโ€˜๐‘)
2322, 5symgbasfi 19246 . . . 4 (๐‘ โˆˆ Fin โ†’ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆˆ Fin)
2421, 23syl 17 . . 3 (๐œ‘ โ†’ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆˆ Fin)
2516adantr 482 . . . 4 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ๐‘… โˆˆ Ring)
26 zrhpsgnmhm 21137 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin) โ†’ ((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)) โˆˆ ((SymGrpโ€˜๐‘) MndHom (mulGrpโ€˜๐‘…)))
2716, 21, 26syl2anc 585 . . . . . 6 (๐œ‘ โ†’ ((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)) โˆˆ ((SymGrpโ€˜๐‘) MndHom (mulGrpโ€˜๐‘…)))
289, 12mgpbas 19993 . . . . . . 7 (Baseโ€˜๐‘…) = (Baseโ€˜(mulGrpโ€˜๐‘…))
295, 28mhmf 18677 . . . . . 6 (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)) โˆˆ ((SymGrpโ€˜๐‘) MndHom (mulGrpโ€˜๐‘…)) โ†’ ((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)):(Baseโ€˜(SymGrpโ€˜๐‘))โŸถ(Baseโ€˜๐‘…))
3027, 29syl 17 . . . . 5 (๐œ‘ โ†’ ((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)):(Baseโ€˜(SymGrpโ€˜๐‘))โŸถ(Baseโ€˜๐‘…))
3130ffvelcdmda 7087 . . . 4 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) โˆˆ (Baseโ€˜๐‘…))
329crngmgp 20064 . . . . . . 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 21924 . . . . . . . . . 10 (๐‘‹ โˆˆ ๐ต โ†’ ๐‘‹ โˆˆ ((Baseโ€˜๐‘…) โ†‘m (๐‘ ร— ๐‘)))
371, 36syl 17 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‹ โˆˆ ((Baseโ€˜๐‘…) โ†‘m (๐‘ ร— ๐‘)))
38 elmapi 8843 . . . . . . . . 9 (๐‘‹ โˆˆ ((Baseโ€˜๐‘…) โ†‘m (๐‘ ร— ๐‘)) โ†’ ๐‘‹:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘…))
3937, 38syl 17 . . . . . . . 8 (๐œ‘ โ†’ ๐‘‹:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘…))
4039ad2antrr 725 . . . . . . 7 (((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘‹:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘…))
4122, 5symgbasf1o 19242 . . . . . . . . . 10 (๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†’ ๐‘:๐‘โ€“1-1-ontoโ†’๐‘)
4241adantl 483 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ๐‘:๐‘โ€“1-1-ontoโ†’๐‘)
43 f1of 6834 . . . . . . . . 9 (๐‘:๐‘โ€“1-1-ontoโ†’๐‘ โ†’ ๐‘:๐‘โŸถ๐‘)
4442, 43syl 17 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ๐‘:๐‘โŸถ๐‘)
4544ffvelcdmda 7087 . . . . . . 7 (((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐‘โ€˜๐‘) โˆˆ ๐‘)
46 simpr 486 . . . . . . 7 (((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘ โˆˆ ๐‘)
4740, 45, 46fovcdmd 7579 . . . . . 6 (((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘)๐‘‹๐‘) โˆˆ (Baseโ€˜๐‘…))
4847ralrimiva 3147 . . . . 5 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ โˆ€๐‘ โˆˆ ๐‘ ((๐‘โ€˜๐‘)๐‘‹๐‘) โˆˆ (Baseโ€˜๐‘…))
4928, 34, 35, 48gsummptcl 19835 . . . 4 ((๐œ‘ โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…))
5012, 8ringcl 20073 . . . 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 4472 . . . 4 ((pmEvenโ€˜๐‘) โˆฉ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) = โˆ…
5352a1i 11 . . 3 (๐œ‘ โ†’ ((pmEvenโ€˜๐‘) โˆฉ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) = โˆ…)
5422, 5evpmss 21139 . . . . . 6 (pmEvenโ€˜๐‘) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘))
55 undif 4482 . . . . . 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 19799 . 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 6038 . . . . . . 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 21144 . . . . . . . . . 10 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) = (1rโ€˜๐‘…))
6863, 64, 65, 67syl3anc 1372 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) = (1rโ€˜๐‘…))
6968oveq1d 7424 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = ((1rโ€˜๐‘…)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
7054sseli 3979 . . . . . . . . . 10 (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†’ ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
7170, 49sylan2 594 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…))
7212, 8, 66ringlidm 20086 . . . . . . . . 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 5249 . . . . . 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 7425 . . . 4 (๐œ‘ โ†’ (๐‘… ฮฃg ((๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โ†พ (pmEvenโ€˜๐‘))) = (๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
78 difss 4132 . . . . . . . 8 ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘))
79 resmpt 6038 . . . . . . . 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 21145 . . . . . . . . . . . 12 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) = ((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…)))
8681, 82, 83, 85syl3anc 1372 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ (((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘) = ((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…)))
8786oveq1d 7424 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) = (((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…))(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))
88 eldifi 4127 . . . . . . . . . . . 12 (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†’ ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
8988, 49sylan2 594 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…))
9012, 8, 66, 84, 81, 89ringnegl 20114 . . . . . . . . . 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 5249 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))โ€˜๐‘)(.rโ€˜๐‘…)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) = (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((invgโ€˜๐‘…)โ€˜((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))))
93 ringgrp 20061 . . . . . . . . . . 11 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Grp)
9416, 93syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘… โˆˆ Grp)
9512, 84grpinvf 18871 . . . . . . . . . 10 (๐‘… โˆˆ Grp โ†’ (invgโ€˜๐‘…):(Baseโ€˜๐‘…)โŸถ(Baseโ€˜๐‘…))
9694, 95syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (invgโ€˜๐‘…):(Baseโ€˜๐‘…)โŸถ(Baseโ€˜๐‘…))
9796, 89cofmpt 7130 . . . . . . . 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 7425 . . . . 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 20098 . . . . . . 7 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Abel)
10316, 102syl 17 . . . . . 6 (๐œ‘ โ†’ ๐‘… โˆˆ Abel)
104 difssd 4133 . . . . . . 7 (๐œ‘ โ†’ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘)))
10524, 104ssfid 9267 . . . . . 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 19815 . . . . 5 (๐œ‘ โ†’ (๐‘… ฮฃg ((invgโ€˜๐‘…) โˆ˜ (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))) = ((invgโ€˜๐‘…)โ€˜(๐‘… ฮฃg (๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))))))
10889ralrimiva 3147 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘))((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…))
109 mdetralt.i . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ผ โˆˆ ๐‘)
110 mdetralt.j . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ฝ โˆˆ ๐‘)
111109, 110prssd 4826 . . . . . . . . . . 11 (๐œ‘ โ†’ {๐ผ, ๐ฝ} โŠ† ๐‘)
112 mdetralt.ij . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ผ โ‰  ๐ฝ)
113 enpr2 9997 . . . . . . . . . . . 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 19325 . . . . . . . . . . 11 ((๐‘ โˆˆ Fin โˆง {๐ผ, ๐ฝ} โŠ† ๐‘ โˆง {๐ผ, ๐ฝ} โ‰ˆ 2o) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ran (pmTrspโ€˜๐‘))
11821, 111, 114, 117syl3anc 1372 . . . . . . . . . 10 (๐œ‘ โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ran (pmTrspโ€˜๐‘))
11922, 5, 116pmtrodpm 21150 . . . . . . . . . 10 ((๐‘ โˆˆ Fin โˆง ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ran (pmTrspโ€˜๐‘)) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
12021, 118, 119syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)))
12122, 5evpmodpmf1o 21149 . . . . . . . . 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 19836 . . . . . . 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 7417 . . . . . . . . . . . . 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 19268 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ Fin โ†’ (SymGrpโ€˜๐‘) โˆˆ Grp)
13021, 129syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (SymGrpโ€˜๐‘) โˆˆ Grp)
131130adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (SymGrpโ€˜๐‘) โˆˆ Grp)
132116, 22, 5symgtrf 19337 . . . . . . . . . . . . . 14 ran (pmTrspโ€˜๐‘) โŠ† (Baseโ€˜(SymGrpโ€˜๐‘))
133118adantr 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ran (pmTrspโ€˜๐‘))
134132, 133sselid 3981 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
13570adantl 483 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
136 eqid 2733 . . . . . . . . . . . . . 14 (+gโ€˜(SymGrpโ€˜๐‘)) = (+gโ€˜(SymGrpโ€˜๐‘))
1375, 136grpcl 18827 . . . . . . . . . . . . 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 21134 . . . . . . . . . . . . . . . 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 5433 . . . . . . . . . . . . . . . 16 {1, -1} โˆˆ V
144 eqid 2733 . . . . . . . . . . . . . . . . . 18 (mulGrpโ€˜โ„‚fld) = (mulGrpโ€˜โ„‚fld)
145 cnfldmul 20950 . . . . . . . . . . . . . . . . . 18 ยท = (.rโ€˜โ„‚fld)
146144, 145mgpplusg 19991 . . . . . . . . . . . . . . . . 17 ยท = (+gโ€˜(mulGrpโ€˜โ„‚fld))
147139, 146ressplusg 17235 . . . . . . . . . . . . . . . 16 ({1, -1} โˆˆ V โ†’ ยท = (+gโ€˜((mulGrpโ€˜โ„‚fld) โ†พs {1, -1})))
148143, 147ax-mp 5 . . . . . . . . . . . . . . 15 ยท = (+gโ€˜((mulGrpโ€˜โ„‚fld) โ†พs {1, -1}))
1495, 136, 148ghmlin 19097 . . . . . . . . . . . . . 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 19378 . . . . . . . . . . . . . . . 16 (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ ran (pmTrspโ€˜๐‘) โ†’ ((pmSgnโ€˜๐‘)โ€˜((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})) = -1)
152133, 151syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmSgnโ€˜๐‘)โ€˜((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})) = -1)
15322, 5, 7psgnevpm 21142 . . . . . . . . . . . . . . . 16 ((๐‘ โˆˆ Fin โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmSgnโ€˜๐‘)โ€˜๐‘) = 1)
15421, 153sylan 581 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((pmSgnโ€˜๐‘)โ€˜๐‘) = 1)
155152, 154oveq12d 7427 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (((pmSgnโ€˜๐‘)โ€˜((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})) ยท ((pmSgnโ€˜๐‘)โ€˜๐‘)) = (-1 ยท 1))
156 neg1cn 12326 . . . . . . . . . . . . . . 15 -1 โˆˆ โ„‚
157156mulridi 11218 . . . . . . . . . . . . . 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 21143 . . . . . . . . . . . 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 6891 . . . . . . . . . . . . 13 (๐‘ = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โ†’ (๐‘โ€˜๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘))
166165oveq1d 7424 . . . . . . . . . . . 12 (๐‘ = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โ†’ ((๐‘โ€˜๐‘)๐‘‹๐‘) = (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘))
167166mpteq2dv 5251 . . . . . . . . . . 11 (๐‘ = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)) = (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘)))
168167oveq2d 7425 . . . . . . . . . 10 (๐‘ = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘))))
169162, 163, 164, 168fmptco 7127 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ โˆˆ ((Baseโ€˜(SymGrpโ€˜๐‘)) โˆ– (pmEvenโ€˜๐‘)) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))) โˆ˜ (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž))) = (๐‘ž โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘)))))
170 oveq2 7417 . . . . . . . . . . . . . . 15 (๐‘ž = ๐‘ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘))
171170fveq1d 6894 . . . . . . . . . . . . . 14 (๐‘ž = ๐‘ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘))
172171oveq1d 7424 . . . . . . . . . . . . 13 (๐‘ž = ๐‘ โ†’ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘) = (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘))
173172mpteq2dv 5251 . . . . . . . . . . . 12 (๐‘ž = ๐‘ โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘)) = (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘)))
174173oveq2d 7425 . . . . . . . . . . 11 (๐‘ž = ๐‘ โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘ž)โ€˜๐‘)๐‘‹๐‘))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘))))
175174cbvmptv 5262 . . . . . . . . . 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 19251 . . . . . . . . . . . . . . . . 17 ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆง ๐‘ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ˜ ๐‘))
180177, 178, 179syl2anc 585 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ˜ ๐‘))
181180fveq1d 6894 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ˜ ๐‘)โ€˜๐‘))
18270, 44sylan2 594 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ๐‘:๐‘โŸถ๐‘)
183 fvco3 6991 . . . . . . . . . . . . . . . 16 ((๐‘:๐‘โŸถ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ˜ ๐‘)โ€˜๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)))
184182, 183sylan 581 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ˜ ๐‘)โ€˜๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)))
185181, 184eqtrd 2773 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)))
186185oveq1d 7424 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘))
187115pmtrprfv 19321 . . . . . . . . . . . . . . . . . . 19 ((๐‘ โˆˆ Fin โˆง (๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ โˆง ๐ผ โ‰  ๐ฝ)) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ) = ๐ฝ)
18821, 109, 110, 112, 187syl13anc 1373 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ) = ๐ฝ)
189188ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ) = ๐ฝ)
190189oveq1d 7424 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ)๐‘‹๐‘) = (๐ฝ๐‘‹๐‘))
191 oveq2 7417 . . . . . . . . . . . . . . . . . 18 (๐‘Ž = ๐‘ โ†’ (๐ผ๐‘‹๐‘Ž) = (๐ผ๐‘‹๐‘))
192 oveq2 7417 . . . . . . . . . . . . . . . . . 18 (๐‘Ž = ๐‘ โ†’ (๐ฝ๐‘‹๐‘Ž) = (๐ฝ๐‘‹๐‘))
193191, 192eqeq12d 2749 . . . . . . . . . . . . . . . . 17 (๐‘Ž = ๐‘ โ†’ ((๐ผ๐‘‹๐‘Ž) = (๐ฝ๐‘‹๐‘Ž) โ†” (๐ผ๐‘‹๐‘) = (๐ฝ๐‘‹๐‘)))
194 mdetralt.eq . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ ๐‘ (๐ผ๐‘‹๐‘Ž) = (๐ฝ๐‘‹๐‘Ž))
195194ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ โˆ€๐‘Ž โˆˆ ๐‘ (๐ผ๐‘‹๐‘Ž) = (๐ฝ๐‘‹๐‘Ž))
196 simpr 486 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ๐‘ โˆˆ ๐‘)
197193, 195, 196rspcdva 3614 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐ผ๐‘‹๐‘) = (๐ฝ๐‘‹๐‘))
198190, 197eqtr4d 2776 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ)๐‘‹๐‘) = (๐ผ๐‘‹๐‘))
199 fveq2 6892 . . . . . . . . . . . . . . . . 17 ((๐‘โ€˜๐‘) = ๐ผ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ))
200199oveq1d 7424 . . . . . . . . . . . . . . . 16 ((๐‘โ€˜๐‘) = ๐ผ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ)๐‘‹๐‘))
201 oveq1 7416 . . . . . . . . . . . . . . . 16 ((๐‘โ€˜๐‘) = ๐ผ โ†’ ((๐‘โ€˜๐‘)๐‘‹๐‘) = (๐ผ๐‘‹๐‘))
202200, 201eqeq12d 2749 . . . . . . . . . . . . . . 15 ((๐‘โ€˜๐‘) = ๐ผ โ†’ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘) โ†” ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ผ)๐‘‹๐‘) = (๐ผ๐‘‹๐‘)))
203198, 202syl5ibrcom 246 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) = ๐ผ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘)))
204 prcom 4737 . . . . . . . . . . . . . . . . . . . . . . 23 {๐ผ, ๐ฝ} = {๐ฝ, ๐ผ}
205204fveq2i 6895 . . . . . . . . . . . . . . . . . . . . . 22 ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) = ((pmTrspโ€˜๐‘)โ€˜{๐ฝ, ๐ผ})
206205fveq1i 6893 . . . . . . . . . . . . . . . . . . . . 21 (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ) = (((pmTrspโ€˜๐‘)โ€˜{๐ฝ, ๐ผ})โ€˜๐ฝ)
207112necomd 2997 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ๐ฝ โ‰  ๐ผ)
208115pmtrprfv 19321 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ โˆˆ Fin โˆง (๐ฝ โˆˆ ๐‘ โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โ‰  ๐ผ)) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ฝ, ๐ผ})โ€˜๐ฝ) = ๐ผ)
20921, 110, 109, 207, 208syl13anc 1373 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ฝ, ๐ผ})โ€˜๐ฝ) = ๐ผ)
210206, 209eqtrid 2785 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ) = ๐ผ)
211210oveq1d 7424 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ)๐‘‹๐‘) = (๐ผ๐‘‹๐‘))
212211ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ)๐‘‹๐‘) = (๐ผ๐‘‹๐‘))
213212, 197eqtrd 2773 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ)๐‘‹๐‘) = (๐ฝ๐‘‹๐‘))
214 fveq2 6892 . . . . . . . . . . . . . . . . . . 19 ((๐‘โ€˜๐‘) = ๐ฝ โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) = (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ))
215214oveq1d 7424 . . . . . . . . . . . . . . . . . 18 ((๐‘โ€˜๐‘) = ๐ฝ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ)๐‘‹๐‘))
216 oveq1 7416 . . . . . . . . . . . . . . . . . 18 ((๐‘โ€˜๐‘) = ๐ฝ โ†’ ((๐‘โ€˜๐‘)๐‘‹๐‘) = (๐ฝ๐‘‹๐‘))
217215, 216eqeq12d 2749 . . . . . . . . . . . . . . . . 17 ((๐‘โ€˜๐‘) = ๐ฝ โ†’ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘) โ†” ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜๐ฝ)๐‘‹๐‘) = (๐ฝ๐‘‹๐‘)))
218213, 217syl5ibrcom 246 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) = ๐ฝ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘)))
219218a1dd 50 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) = ๐ฝ โ†’ ((๐‘โ€˜๐‘) โ‰  ๐ผ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘))))
220 neanior 3036 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†” ยฌ ((๐‘โ€˜๐‘) = ๐ฝ โˆจ (๐‘โ€˜๐‘) = ๐ผ))
221 elpri 4651 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘โ€˜๐‘) โˆˆ {๐ผ, ๐ฝ} โ†’ ((๐‘โ€˜๐‘) = ๐ผ โˆจ (๐‘โ€˜๐‘) = ๐ฝ))
222221orcomd 870 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘โ€˜๐‘) โˆˆ {๐ผ, ๐ฝ} โ†’ ((๐‘โ€˜๐‘) = ๐ฝ โˆจ (๐‘โ€˜๐‘) = ๐ผ))
223222con3i 154 . . . . . . . . . . . . . . . . . . . . 21 (ยฌ ((๐‘โ€˜๐‘) = ๐ฝ โˆจ (๐‘โ€˜๐‘) = ๐ผ) โ†’ ยฌ (๐‘โ€˜๐‘) โˆˆ {๐ผ, ๐ฝ})
224220, 223sylbi 216 . . . . . . . . . . . . . . . . . . . 20 (((๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ ยฌ (๐‘โ€˜๐‘) โˆˆ {๐ผ, ๐ฝ})
2252243adant1 1131 . . . . . . . . . . . . . . . . . . 19 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ ยฌ (๐‘โ€˜๐‘) โˆˆ {๐ผ, ๐ฝ})
226115pmtrmvd 19324 . . . . . . . . . . . . . . . . . . . . . 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 19323 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ โˆˆ Fin โˆง {๐ผ, ๐ฝ} โŠ† ๐‘ โˆง {๐ผ, ๐ฝ} โ‰ˆ 2o) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}):๐‘โŸถ๐‘)
23221, 111, 114, 231syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}):๐‘โŸถ๐‘)
233232ffnd 6719 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) Fn ๐‘)
234233ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) Fn ๐‘)
235182ffvelcdmda 7087 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐‘โ€˜๐‘) โˆˆ ๐‘)
236 fnelnfp 7175 . . . . . . . . . . . . . . . . . . . . 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 2985 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) = (๐‘โ€˜๐‘) โ†” ยฌ (๐‘โ€˜๐‘) โˆˆ dom (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ}) โˆ– I )))
240230, 239mpbird 257 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ (((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘)) = (๐‘โ€˜๐‘))
241240oveq1d 7424 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โˆง (๐‘โ€˜๐‘) โ‰  ๐ฝ โˆง (๐‘โ€˜๐‘) โ‰  ๐ผ) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘))
2422413exp 1120 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) โ‰  ๐ฝ โ†’ ((๐‘โ€˜๐‘) โ‰  ๐ผ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘))))
243219, 242pm2.61dne 3029 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((๐‘โ€˜๐‘) โ‰  ๐ผ โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘)))
244203, 243pm2.61dne 3029 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ ((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})โ€˜(๐‘โ€˜๐‘))๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘))
245186, 244eqtrd 2773 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โˆง ๐‘ โˆˆ ๐‘) โ†’ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘) = ((๐‘โ€˜๐‘)๐‘‹๐‘))
246245mpteq2dva 5249 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘)) = (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘)))
247246oveq2d 7425 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ (pmEvenโ€˜๐‘)) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ (((((pmTrspโ€˜๐‘)โ€˜{๐ผ, ๐ฝ})(+gโ€˜(SymGrpโ€˜๐‘))๐‘)โ€˜๐‘)๐‘‹๐‘))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))
248247mpteq2dva 5249 . . . . . . . . 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 7425 . . . . . . 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 6896 . . . . 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 7427 . . 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 9267 . . . . 5 (๐œ‘ โ†’ (pmEvenโ€˜๐‘) โˆˆ Fin)
25771ralrimiva 3147 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘ โˆˆ (pmEvenโ€˜๐‘)((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))) โˆˆ (Baseโ€˜๐‘…))
25812, 18, 256, 257gsummptcl 19835 . . . 4 (๐œ‘ โ†’ (๐‘… ฮฃg (๐‘ โˆˆ (pmEvenโ€˜๐‘) โ†ฆ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘ โˆˆ ๐‘ โ†ฆ ((๐‘โ€˜๐‘)๐‘‹๐‘))))) โˆˆ (Baseโ€˜๐‘…))
25912, 13, 101, 84grprinv 18875 . . . 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 2941  โˆ€wral 3062  Vcvv 3475   โˆ– cdif 3946   โˆช cun 3947   โˆฉ cin 3948   โŠ† wss 3949  โˆ…c0 4323  {cpr 4631   class class class wbr 5149   โ†ฆ cmpt 5232   I cid 5574   ร— cxp 5675  dom cdm 5677  ran crn 5678   โ†พ cres 5679   โˆ˜ ccom 5681   Fn wfn 6539  โŸถwf 6540  โ€“1-1-ontoโ†’wf1o 6543  โ€˜cfv 6544  (class class class)co 7409  2oc2o 8460   โ†‘m cmap 8820   โ‰ˆ cen 8936  Fincfn 8939  1c1 11111   ยท cmul 11115  -cneg 11445  Basecbs 17144   โ†พs cress 17173  +gcplusg 17197  .rcmulr 17198  0gc0g 17385   ฮฃg cgsu 17386   MndHom cmhm 18669  Grpcgrp 18819  invgcminusg 18820   GrpHom cghm 19089  SymGrpcsymg 19234  pmTrspcpmtr 19309  pmSgncpsgn 19357  pmEvencevpm 19358  CMndccmn 19648  Abelcabl 19649  mulGrpcmgp 19987  1rcur 20004  Ringcrg 20056  CRingccrg 20057  โ„‚fldccnfld 20944  โ„คRHomczrh 21049   Mat cmat 21907   maDet cmdat 22086
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-addf 11189  ax-mulf 11190
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 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-ot 4638  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-tpos 8211  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-er 8703  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-sup 9437  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-xnn0 12545  df-z 12559  df-dec 12678  df-uz 12823  df-rp 12975  df-fz 13485  df-fzo 13628  df-seq 13967  df-exp 14028  df-hash 14291  df-word 14465  df-lsw 14513  df-concat 14521  df-s1 14546  df-substr 14591  df-pfx 14621  df-splice 14700  df-reverse 14709  df-s2 14799  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-starv 17212  df-sca 17213  df-vsca 17214  df-ip 17215  df-tset 17216  df-ple 17217  df-ds 17219  df-unif 17220  df-hom 17221  df-cco 17222  df-0g 17387  df-gsum 17388  df-prds 17393  df-pws 17395  df-mre 17530  df-mrc 17531  df-acs 17533  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-mhm 18671  df-submnd 18672  df-efmnd 18750  df-grp 18822  df-minusg 18823  df-mulg 18951  df-subg 19003  df-ghm 19090  df-gim 19133  df-cntz 19181  df-oppg 19210  df-symg 19235  df-pmtr 19310  df-psgn 19359  df-evpm 19360  df-cmn 19650  df-abl 19651  df-mgp 19988  df-ur 20005  df-ring 20058  df-cring 20059  df-oppr 20150  df-dvdsr 20171  df-unit 20172  df-invr 20202  df-dvr 20215  df-rnghom 20251  df-subrg 20317  df-drng 20359  df-sra 20785  df-rgmod 20786  df-cnfld 20945  df-zring 21018  df-zrh 21053  df-dsmm 21287  df-frlm 21302  df-mat 21908  df-mdet 22087
This theorem is referenced by:  mdetralt2  22111  mdetuni0  22123  mdetmul  22125
  Copyright terms: Public domain W3C validator