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

Theorem mdetleib2 22441
Description: Leibniz' formula can also be expanded by rows. (Contributed by Stefan O'Rear, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)
Hypotheses
Ref Expression
mdetfval.d ๐ท = (๐‘ maDet ๐‘…)
mdetfval.a ๐ด = (๐‘ Mat ๐‘…)
mdetfval.b ๐ต = (Baseโ€˜๐ด)
mdetfval.p ๐‘ƒ = (Baseโ€˜(SymGrpโ€˜๐‘))
mdetfval.y ๐‘Œ = (โ„คRHomโ€˜๐‘…)
mdetfval.s ๐‘† = (pmSgnโ€˜๐‘)
mdetfval.t ยท = (.rโ€˜๐‘…)
mdetfval.u ๐‘ˆ = (mulGrpโ€˜๐‘…)
Assertion
Ref Expression
mdetleib2 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐ทโ€˜๐‘€) = (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘) ยท (๐‘ˆ ฮฃg (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ))))))))
Distinct variable groups:   ๐‘ฅ,๐‘,๐‘€   ๐‘,๐‘,๐‘ฅ   ๐‘…,๐‘,๐‘ฅ   ๐ต,๐‘,๐‘ฅ   ๐‘ƒ,๐‘,๐‘ฅ   ๐‘†,๐‘   ๐‘ˆ,๐‘   ๐‘Œ,๐‘   ยท ,๐‘
Allowed substitution hints:   ๐ด(๐‘ฅ,๐‘)   ๐ท(๐‘ฅ,๐‘)   ๐‘†(๐‘ฅ)   ยท (๐‘ฅ)   ๐‘ˆ(๐‘ฅ)   ๐‘Œ(๐‘ฅ)

Proof of Theorem mdetleib2
Dummy variables ๐‘ฆ ๐‘ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetfval.d . . . 4 ๐ท = (๐‘ maDet ๐‘…)
2 mdetfval.a . . . 4 ๐ด = (๐‘ Mat ๐‘…)
3 mdetfval.b . . . 4 ๐ต = (Baseโ€˜๐ด)
4 mdetfval.p . . . 4 ๐‘ƒ = (Baseโ€˜(SymGrpโ€˜๐‘))
5 mdetfval.y . . . 4 ๐‘Œ = (โ„คRHomโ€˜๐‘…)
6 mdetfval.s . . . 4 ๐‘† = (pmSgnโ€˜๐‘)
7 mdetfval.t . . . 4 ยท = (.rโ€˜๐‘…)
8 mdetfval.u . . . 4 ๐‘ˆ = (mulGrpโ€˜๐‘…)
91, 2, 3, 4, 5, 6, 7, 8mdetleib 22440 . . 3 (๐‘€ โˆˆ ๐ต โ†’ (๐ทโ€˜๐‘€) = (๐‘… ฮฃg (๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ)))))))
109adantl 481 . 2 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐ทโ€˜๐‘€) = (๐‘… ฮฃg (๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ)))))))
11 eqid 2726 . . 3 (Baseโ€˜๐‘…) = (Baseโ€˜๐‘…)
12 crngring 20148 . . . . 5 (๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring)
13 ringcmn 20179 . . . . 5 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ CMnd)
1412, 13syl 17 . . . 4 (๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ CMnd)
1514adantr 480 . . 3 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘… โˆˆ CMnd)
162, 3matrcl 22263 . . . . . 6 (๐‘€ โˆˆ ๐ต โ†’ (๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ V))
1716adantl 481 . . . . 5 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ V))
1817simpld 494 . . . 4 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘ โˆˆ Fin)
19 eqid 2726 . . . . 5 (SymGrpโ€˜๐‘) = (SymGrpโ€˜๐‘)
2019, 4symgbasfi 19296 . . . 4 (๐‘ โˆˆ Fin โ†’ ๐‘ƒ โˆˆ Fin)
2118, 20syl 17 . . 3 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘ƒ โˆˆ Fin)
2212ad2antrr 723 . . . . 5 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โ†’ ๐‘… โˆˆ Ring)
235, 6coeq12i 5856 . . . . . . . . 9 (๐‘Œ โˆ˜ ๐‘†) = ((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘))
24 zrhpsgnmhm 21473 . . . . . . . . 9 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin) โ†’ ((โ„คRHomโ€˜๐‘…) โˆ˜ (pmSgnโ€˜๐‘)) โˆˆ ((SymGrpโ€˜๐‘) MndHom (mulGrpโ€˜๐‘…)))
2523, 24eqeltrid 2831 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin) โ†’ (๐‘Œ โˆ˜ ๐‘†) โˆˆ ((SymGrpโ€˜๐‘) MndHom (mulGrpโ€˜๐‘…)))
2612, 18, 25syl2an2r 682 . . . . . . 7 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐‘Œ โˆ˜ ๐‘†) โˆˆ ((SymGrpโ€˜๐‘) MndHom (mulGrpโ€˜๐‘…)))
27 eqid 2726 . . . . . . . . 9 (mulGrpโ€˜๐‘…) = (mulGrpโ€˜๐‘…)
2827, 11mgpbas 20043 . . . . . . . 8 (Baseโ€˜๐‘…) = (Baseโ€˜(mulGrpโ€˜๐‘…))
294, 28mhmf 18717 . . . . . . 7 ((๐‘Œ โˆ˜ ๐‘†) โˆˆ ((SymGrpโ€˜๐‘) MndHom (mulGrpโ€˜๐‘…)) โ†’ (๐‘Œ โˆ˜ ๐‘†):๐‘ƒโŸถ(Baseโ€˜๐‘…))
3026, 29syl 17 . . . . . 6 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐‘Œ โˆ˜ ๐‘†):๐‘ƒโŸถ(Baseโ€˜๐‘…))
3130ffvelcdmda 7079 . . . . 5 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โ†’ ((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) โˆˆ (Baseโ€˜๐‘…))
328, 11mgpbas 20043 . . . . . 6 (Baseโ€˜๐‘…) = (Baseโ€˜๐‘ˆ)
338crngmgp 20144 . . . . . . 7 (๐‘… โˆˆ CRing โ†’ ๐‘ˆ โˆˆ CMnd)
3433ad2antrr 723 . . . . . 6 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โ†’ ๐‘ˆ โˆˆ CMnd)
3518adantr 480 . . . . . 6 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โ†’ ๐‘ โˆˆ Fin)
36 simpr 484 . . . . . . . . . 10 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘€ โˆˆ ๐ต)
372, 11, 3matbas2i 22275 . . . . . . . . . 10 (๐‘€ โˆˆ ๐ต โ†’ ๐‘€ โˆˆ ((Baseโ€˜๐‘…) โ†‘m (๐‘ ร— ๐‘)))
38 elmapi 8842 . . . . . . . . . 10 (๐‘€ โˆˆ ((Baseโ€˜๐‘…) โ†‘m (๐‘ ร— ๐‘)) โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘…))
3936, 37, 383syl 18 . . . . . . . . 9 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘…))
4039ad2antrr 723 . . . . . . . 8 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘…))
4119, 4symgbasf1o 19292 . . . . . . . . . . 11 (๐‘ž โˆˆ ๐‘ƒ โ†’ ๐‘ž:๐‘โ€“1-1-ontoโ†’๐‘)
4241adantl 481 . . . . . . . . . 10 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โ†’ ๐‘ž:๐‘โ€“1-1-ontoโ†’๐‘)
43 f1of 6826 . . . . . . . . . 10 (๐‘ž:๐‘โ€“1-1-ontoโ†’๐‘ โ†’ ๐‘ž:๐‘โŸถ๐‘)
4442, 43syl 17 . . . . . . . . 9 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โ†’ ๐‘ž:๐‘โŸถ๐‘)
4544ffvelcdmda 7079 . . . . . . . 8 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ (๐‘žโ€˜๐‘ฆ) โˆˆ ๐‘)
46 simpr 484 . . . . . . . 8 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ ๐‘ฆ โˆˆ ๐‘)
4740, 45, 46fovcdmd 7575 . . . . . . 7 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ) โˆˆ (Baseโ€˜๐‘…))
4847ralrimiva 3140 . . . . . 6 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ) โˆˆ (Baseโ€˜๐‘…))
4932, 34, 35, 48gsummptcl 19885 . . . . 5 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โ†’ (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ))) โˆˆ (Baseโ€˜๐‘…))
5011, 7ringcl 20153 . . . . 5 ((๐‘… โˆˆ Ring โˆง ((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) โˆˆ (Baseโ€˜๐‘…) โˆง (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ))) โˆˆ (Baseโ€˜๐‘…)) โ†’ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ)))) โˆˆ (Baseโ€˜๐‘…))
5122, 31, 49, 50syl3anc 1368 . . . 4 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐‘ƒ) โ†’ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ)))) โˆˆ (Baseโ€˜๐‘…))
5251ralrimiva 3140 . . 3 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ โˆ€๐‘ž โˆˆ ๐‘ƒ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ)))) โˆˆ (Baseโ€˜๐‘…))
53 eqid 2726 . . 3 (๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ))))) = (๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ)))))
54 eqid 2726 . . . 4 (invgโ€˜(SymGrpโ€˜๐‘)) = (invgโ€˜(SymGrpโ€˜๐‘))
5519symggrp 19318 . . . . 5 (๐‘ โˆˆ Fin โ†’ (SymGrpโ€˜๐‘) โˆˆ Grp)
5618, 55syl 17 . . . 4 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (SymGrpโ€˜๐‘) โˆˆ Grp)
574, 54, 56grpinvf1o 18936 . . 3 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (invgโ€˜(SymGrpโ€˜๐‘)):๐‘ƒโ€“1-1-ontoโ†’๐‘ƒ)
5811, 15, 21, 52, 53, 57gsummptfif1o 19886 . 2 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐‘… ฮฃg (๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ)))))) = (๐‘… ฮฃg ((๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ))))) โˆ˜ (invgโ€˜(SymGrpโ€˜๐‘)))))
59 f1of 6826 . . . . . . 7 ((invgโ€˜(SymGrpโ€˜๐‘)):๐‘ƒโ€“1-1-ontoโ†’๐‘ƒ โ†’ (invgโ€˜(SymGrpโ€˜๐‘)):๐‘ƒโŸถ๐‘ƒ)
6057, 59syl 17 . . . . . 6 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (invgโ€˜(SymGrpโ€˜๐‘)):๐‘ƒโŸถ๐‘ƒ)
6160ffvelcdmda 7079 . . . . 5 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) โˆˆ ๐‘ƒ)
6260feqmptd 6953 . . . . 5 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (invgโ€˜(SymGrpโ€˜๐‘)) = (๐‘ โˆˆ ๐‘ƒ โ†ฆ ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)))
63 eqidd 2727 . . . . 5 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ))))) = (๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ))))))
64 fveq2 6884 . . . . . 6 (๐‘ž = ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) โ†’ ((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) = ((๐‘Œ โˆ˜ ๐‘†)โ€˜((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)))
65 fveq1 6883 . . . . . . . . 9 (๐‘ž = ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) โ†’ (๐‘žโ€˜๐‘ฆ) = (((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ))
6665oveq1d 7419 . . . . . . . 8 (๐‘ž = ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) โ†’ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ) = ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ))
6766mpteq2dv 5243 . . . . . . 7 (๐‘ž = ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) โ†’ (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ)) = (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ)))
6867oveq2d 7420 . . . . . 6 (๐‘ž = ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) โ†’ (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ))) = (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ))))
6964, 68oveq12d 7422 . . . . 5 (๐‘ž = ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) โ†’ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ)))) = (((๐‘Œ โˆ˜ ๐‘†)โ€˜((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ)))))
7061, 62, 63, 69fmptco 7122 . . . 4 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ))))) โˆ˜ (invgโ€˜(SymGrpโ€˜๐‘))) = (๐‘ โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ))))))
7119, 4, 54symginv 19320 . . . . . . . . 9 (๐‘ โˆˆ ๐‘ƒ โ†’ ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) = โ—ก๐‘)
7271adantl 481 . . . . . . . 8 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) = โ—ก๐‘)
7372fveq2d 6888 . . . . . . 7 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ((๐‘Œ โˆ˜ ๐‘†)โ€˜((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)) = ((๐‘Œ โˆ˜ ๐‘†)โ€˜โ—ก๐‘))
7412ad2antrr 723 . . . . . . . 8 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ๐‘… โˆˆ Ring)
7518adantr 480 . . . . . . . 8 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ๐‘ โˆˆ Fin)
76 simpr 484 . . . . . . . 8 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ๐‘ โˆˆ ๐‘ƒ)
774, 5, 6zrhpsgninv 21474 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ((๐‘Œ โˆ˜ ๐‘†)โ€˜โ—ก๐‘) = ((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘))
7874, 75, 76, 77syl3anc 1368 . . . . . . 7 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ((๐‘Œ โˆ˜ ๐‘†)โ€˜โ—ก๐‘) = ((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘))
7973, 78eqtrd 2766 . . . . . 6 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ((๐‘Œ โˆ˜ ๐‘†)โ€˜((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)) = ((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘))
80 eqid 2726 . . . . . . . 8 (Baseโ€˜๐‘ˆ) = (Baseโ€˜๐‘ˆ)
8133ad2antrr 723 . . . . . . . 8 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ๐‘ˆ โˆˆ CMnd)
8239ad2antrr 723 . . . . . . . . . . 11 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ ๐‘€:(๐‘ ร— ๐‘)โŸถ(Baseโ€˜๐‘…))
8371ad2antlr 724 . . . . . . . . . . . . 13 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) = โ—ก๐‘)
8483fveq1d 6886 . . . . . . . . . . . 12 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ (((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ) = (โ—ก๐‘โ€˜๐‘ฆ))
8519, 4symgbasf1o 19292 . . . . . . . . . . . . . . 15 (๐‘ โˆˆ ๐‘ƒ โ†’ ๐‘:๐‘โ€“1-1-ontoโ†’๐‘)
8685adantl 481 . . . . . . . . . . . . . 14 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ๐‘:๐‘โ€“1-1-ontoโ†’๐‘)
87 f1ocnv 6838 . . . . . . . . . . . . . 14 (๐‘:๐‘โ€“1-1-ontoโ†’๐‘ โ†’ โ—ก๐‘:๐‘โ€“1-1-ontoโ†’๐‘)
88 f1of 6826 . . . . . . . . . . . . . 14 (โ—ก๐‘:๐‘โ€“1-1-ontoโ†’๐‘ โ†’ โ—ก๐‘:๐‘โŸถ๐‘)
8986, 87, 883syl 18 . . . . . . . . . . . . 13 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ โ—ก๐‘:๐‘โŸถ๐‘)
9089ffvelcdmda 7079 . . . . . . . . . . . 12 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ (โ—ก๐‘โ€˜๐‘ฆ) โˆˆ ๐‘)
9184, 90eqeltrd 2827 . . . . . . . . . . 11 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ (((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ) โˆˆ ๐‘)
92 simpr 484 . . . . . . . . . . 11 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ ๐‘ฆ โˆˆ ๐‘)
9382, 91, 92fovcdmd 7575 . . . . . . . . . 10 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ) โˆˆ (Baseโ€˜๐‘…))
9493, 32eleqtrdi 2837 . . . . . . . . 9 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ ๐‘) โ†’ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ) โˆˆ (Baseโ€˜๐‘ˆ))
9594ralrimiva 3140 . . . . . . . 8 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ) โˆˆ (Baseโ€˜๐‘ˆ))
96 eqid 2726 . . . . . . . 8 (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ)) = (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ))
9780, 81, 75, 95, 96, 86gsummptfif1o 19886 . . . . . . 7 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ))) = (๐‘ˆ ฮฃg ((๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ)) โˆ˜ ๐‘)))
98 f1of 6826 . . . . . . . . . . . 12 (๐‘:๐‘โ€“1-1-ontoโ†’๐‘ โ†’ ๐‘:๐‘โŸถ๐‘)
9986, 98syl 17 . . . . . . . . . . 11 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ๐‘:๐‘โŸถ๐‘)
10099ffvelcdmda 7079 . . . . . . . . . 10 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ ๐‘) โ†’ (๐‘โ€˜๐‘ฅ) โˆˆ ๐‘)
10199feqmptd 6953 . . . . . . . . . 10 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ๐‘ = (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘โ€˜๐‘ฅ)))
102 eqidd 2727 . . . . . . . . . 10 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ)) = (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ)))
103 fveq2 6884 . . . . . . . . . . 11 (๐‘ฆ = (๐‘โ€˜๐‘ฅ) โ†’ (((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ) = (((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜(๐‘โ€˜๐‘ฅ)))
104 id 22 . . . . . . . . . . 11 (๐‘ฆ = (๐‘โ€˜๐‘ฅ) โ†’ ๐‘ฆ = (๐‘โ€˜๐‘ฅ))
105103, 104oveq12d 7422 . . . . . . . . . 10 (๐‘ฆ = (๐‘โ€˜๐‘ฅ) โ†’ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ) = ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜(๐‘โ€˜๐‘ฅ))๐‘€(๐‘โ€˜๐‘ฅ)))
106100, 101, 102, 105fmptco 7122 . . . . . . . . 9 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ((๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ)) โˆ˜ ๐‘) = (๐‘ฅ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜(๐‘โ€˜๐‘ฅ))๐‘€(๐‘โ€˜๐‘ฅ))))
10771ad2antlr 724 . . . . . . . . . . . . 13 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ ๐‘) โ†’ ((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘) = โ—ก๐‘)
108107fveq1d 6886 . . . . . . . . . . . 12 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ ๐‘) โ†’ (((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜(๐‘โ€˜๐‘ฅ)) = (โ—ก๐‘โ€˜(๐‘โ€˜๐‘ฅ)))
109 f1ocnvfv1 7269 . . . . . . . . . . . . 13 ((๐‘:๐‘โ€“1-1-ontoโ†’๐‘ โˆง ๐‘ฅ โˆˆ ๐‘) โ†’ (โ—ก๐‘โ€˜(๐‘โ€˜๐‘ฅ)) = ๐‘ฅ)
11086, 109sylan 579 . . . . . . . . . . . 12 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ ๐‘) โ†’ (โ—ก๐‘โ€˜(๐‘โ€˜๐‘ฅ)) = ๐‘ฅ)
111108, 110eqtrd 2766 . . . . . . . . . . 11 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ ๐‘) โ†’ (((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜(๐‘โ€˜๐‘ฅ)) = ๐‘ฅ)
112111oveq1d 7419 . . . . . . . . . 10 ((((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ ๐‘) โ†’ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜(๐‘โ€˜๐‘ฅ))๐‘€(๐‘โ€˜๐‘ฅ)) = (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ)))
113112mpteq2dva 5241 . . . . . . . . 9 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ (๐‘ฅ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜(๐‘โ€˜๐‘ฅ))๐‘€(๐‘โ€˜๐‘ฅ))) = (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ))))
114106, 113eqtrd 2766 . . . . . . . 8 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ ((๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ)) โˆ˜ ๐‘) = (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ))))
115114oveq2d 7420 . . . . . . 7 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ (๐‘ˆ ฮฃg ((๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ)) โˆ˜ ๐‘)) = (๐‘ˆ ฮฃg (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ)))))
11697, 115eqtrd 2766 . . . . . 6 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ))) = (๐‘ˆ ฮฃg (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ)))))
11779, 116oveq12d 7422 . . . . 5 (((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘ โˆˆ ๐‘ƒ) โ†’ (((๐‘Œ โˆ˜ ๐‘†)โ€˜((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ)))) = (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘) ยท (๐‘ˆ ฮฃg (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ))))))
118117mpteq2dva 5241 . . . 4 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐‘ โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((((invgโ€˜(SymGrpโ€˜๐‘))โ€˜๐‘)โ€˜๐‘ฆ)๐‘€๐‘ฆ))))) = (๐‘ โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘) ยท (๐‘ˆ ฮฃg (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ)))))))
11970, 118eqtrd 2766 . . 3 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ))))) โˆ˜ (invgโ€˜(SymGrpโ€˜๐‘))) = (๐‘ โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘) ยท (๐‘ˆ ฮฃg (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ)))))))
120119oveq2d 7420 . 2 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐‘… ฮฃg ((๐‘ž โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘ž) ยท (๐‘ˆ ฮฃg (๐‘ฆ โˆˆ ๐‘ โ†ฆ ((๐‘žโ€˜๐‘ฆ)๐‘€๐‘ฆ))))) โˆ˜ (invgโ€˜(SymGrpโ€˜๐‘)))) = (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘) ยท (๐‘ˆ ฮฃg (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ))))))))
12110, 58, 1203eqtrd 2770 1 ((๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐ทโ€˜๐‘€) = (๐‘… ฮฃg (๐‘ โˆˆ ๐‘ƒ โ†ฆ (((๐‘Œ โˆ˜ ๐‘†)โ€˜๐‘) ยท (๐‘ˆ ฮฃg (๐‘ฅ โˆˆ ๐‘ โ†ฆ (๐‘ฅ๐‘€(๐‘โ€˜๐‘ฅ))))))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   = wceq 1533   โˆˆ wcel 2098  Vcvv 3468   โ†ฆ cmpt 5224   ร— cxp 5667  โ—กccnv 5668   โˆ˜ ccom 5673  โŸถwf 6532  โ€“1-1-ontoโ†’wf1o 6535  โ€˜cfv 6536  (class class class)co 7404   โ†‘m cmap 8819  Fincfn 8938  Basecbs 17151  .rcmulr 17205   ฮฃg cgsu 17393   MndHom cmhm 18709  Grpcgrp 18861  invgcminusg 18862  SymGrpcsymg 19284  pmSgncpsgn 19407  CMndccmn 19698  mulGrpcmgp 20037  Ringcrg 20136  CRingccrg 20137  โ„คRHomczrh 21382   Mat cmat 22258   maDet cmdat 22437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-addf 11188  ax-mulf 11189
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-xor 1505  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-ot 4632  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8144  df-tpos 8209  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-2o 8465  df-er 8702  df-map 8821  df-pm 8822  df-ixp 8891  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-sup 9436  df-oi 9504  df-card 9933  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11447  df-neg 11448  df-div 11873  df-nn 12214  df-2 12276  df-3 12277  df-4 12278  df-5 12279  df-6 12280  df-7 12281  df-8 12282  df-9 12283  df-n0 12474  df-xnn0 12546  df-z 12560  df-dec 12679  df-uz 12824  df-rp 12978  df-fz 13488  df-fzo 13631  df-seq 13970  df-exp 14031  df-hash 14294  df-word 14469  df-lsw 14517  df-concat 14525  df-s1 14550  df-substr 14595  df-pfx 14625  df-splice 14704  df-reverse 14713  df-s2 14803  df-struct 17087  df-sets 17104  df-slot 17122  df-ndx 17134  df-base 17152  df-ress 17181  df-plusg 17217  df-mulr 17218  df-starv 17219  df-sca 17220  df-vsca 17221  df-ip 17222  df-tset 17223  df-ple 17224  df-ds 17226  df-unif 17227  df-hom 17228  df-cco 17229  df-0g 17394  df-gsum 17395  df-prds 17400  df-pws 17402  df-mre 17537  df-mrc 17538  df-acs 17540  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-mhm 18711  df-submnd 18712  df-efmnd 18792  df-grp 18864  df-minusg 18865  df-mulg 18994  df-subg 19048  df-ghm 19137  df-gim 19182  df-cntz 19231  df-oppg 19260  df-symg 19285  df-pmtr 19360  df-psgn 19409  df-cmn 19700  df-abl 19701  df-mgp 20038  df-rng 20056  df-ur 20085  df-ring 20138  df-cring 20139  df-oppr 20234  df-dvdsr 20257  df-unit 20258  df-invr 20288  df-dvr 20301  df-rhm 20372  df-subrng 20444  df-subrg 20469  df-drng 20587  df-sra 21019  df-rgmod 21020  df-cnfld 21237  df-zring 21330  df-zrh 21386  df-dsmm 21623  df-frlm 21638  df-mat 22259  df-mdet 22438
This theorem is referenced by:  mdetrlin  22455  mdetrsca  22456  mdettpos  22464  smadiadet  22523
  Copyright terms: Public domain W3C validator