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

Theorem m2detleib 22133
Description: Leibniz' Formula for 2x2-matrices. (Contributed by AV, 21-Dec-2018.) (Revised by AV, 26-Dec-2018.) (Proof shortened by AV, 23-Jul-2019.)
Hypotheses
Ref Expression
m2detleib.n ๐‘ = {1, 2}
m2detleib.d ๐ท = (๐‘ maDet ๐‘…)
m2detleib.a ๐ด = (๐‘ Mat ๐‘…)
m2detleib.b ๐ต = (Baseโ€˜๐ด)
m2detleib.m โˆ’ = (-gโ€˜๐‘…)
m2detleib.t ยท = (.rโ€˜๐‘…)
Assertion
Ref Expression
m2detleib ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐ทโ€˜๐‘€) = (((1๐‘€1) ยท (2๐‘€2)) โˆ’ ((2๐‘€1) ยท (1๐‘€2))))

Proof of Theorem m2detleib
Dummy variables ๐‘˜ ๐‘› are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 m2detleib.d . . . 4 ๐ท = (๐‘ maDet ๐‘…)
2 m2detleib.a . . . 4 ๐ด = (๐‘ Mat ๐‘…)
3 m2detleib.b . . . 4 ๐ต = (Baseโ€˜๐ด)
4 eqid 2733 . . . 4 (Baseโ€˜(SymGrpโ€˜๐‘)) = (Baseโ€˜(SymGrpโ€˜๐‘))
5 eqid 2733 . . . 4 (โ„คRHomโ€˜๐‘…) = (โ„คRHomโ€˜๐‘…)
6 eqid 2733 . . . 4 (pmSgnโ€˜๐‘) = (pmSgnโ€˜๐‘)
7 m2detleib.t . . . 4 ยท = (.rโ€˜๐‘…)
8 eqid 2733 . . . 4 (mulGrpโ€˜๐‘…) = (mulGrpโ€˜๐‘…)
91, 2, 3, 4, 5, 6, 7, 8mdetleib1 22093 . . 3 (๐‘€ โˆˆ ๐ต โ†’ (๐ทโ€˜๐‘€) = (๐‘… ฮฃg (๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))))))
109adantl 483 . 2 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐ทโ€˜๐‘€) = (๐‘… ฮฃg (๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))))))
11 eqid 2733 . . 3 (Baseโ€˜๐‘…) = (Baseโ€˜๐‘…)
12 eqid 2733 . . 3 (+gโ€˜๐‘…) = (+gโ€˜๐‘…)
13 ringcmn 20099 . . . 4 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ CMnd)
1413adantr 482 . . 3 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘… โˆˆ CMnd)
15 m2detleib.n . . . . . 6 ๐‘ = {1, 2}
16 prfi 9322 . . . . . 6 {1, 2} โˆˆ Fin
1715, 16eqeltri 2830 . . . . 5 ๐‘ โˆˆ Fin
18 eqid 2733 . . . . . 6 (SymGrpโ€˜๐‘) = (SymGrpโ€˜๐‘)
1918, 4symgbasfi 19246 . . . . 5 (๐‘ โˆˆ Fin โ†’ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆˆ Fin)
2017, 19ax-mp 5 . . . 4 (Baseโ€˜(SymGrpโ€˜๐‘)) โˆˆ Fin
2120a1i 11 . . 3 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆˆ Fin)
22 simpl 484 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘… โˆˆ Ring)
2322adantr 482 . . . 4 (((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ๐‘… โˆˆ Ring)
244, 6, 5zrhpsgnelbas 21147 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin โˆง ๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) โˆˆ (Baseโ€˜๐‘…))
2517, 24mp3an2 1450 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) โˆˆ (Baseโ€˜๐‘…))
2625adantlr 714 . . . 4 (((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) โˆˆ (Baseโ€˜๐‘…))
27 simpr 486 . . . . 5 (((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
28 simpr 486 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘€ โˆˆ ๐ต)
2928adantr 482 . . . . 5 (((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ๐‘€ โˆˆ ๐ต)
3015, 4, 2, 3, 8m2detleiblem2 22130 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))) โˆˆ (Baseโ€˜๐‘…))
3123, 27, 29, 30syl3anc 1372 . . . 4 (((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))) โˆˆ (Baseโ€˜๐‘…))
3211, 7ringcl 20073 . . . 4 ((๐‘… โˆˆ Ring โˆง ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) โˆˆ (Baseโ€˜๐‘…) โˆง ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))) โˆˆ (Baseโ€˜๐‘…)) โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))) โˆˆ (Baseโ€˜๐‘…))
3323, 26, 31, 32syl3anc 1372 . . 3 (((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โˆง ๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))) โˆˆ (Baseโ€˜๐‘…))
34 opex 5465 . . . . . . . 8 โŸจ1, 1โŸฉ โˆˆ V
35 opex 5465 . . . . . . . 8 โŸจ2, 2โŸฉ โˆˆ V
3634, 35pm3.2i 472 . . . . . . 7 (โŸจ1, 1โŸฉ โˆˆ V โˆง โŸจ2, 2โŸฉ โˆˆ V)
37 opex 5465 . . . . . . . 8 โŸจ1, 2โŸฉ โˆˆ V
38 opex 5465 . . . . . . . 8 โŸจ2, 1โŸฉ โˆˆ V
3937, 38pm3.2i 472 . . . . . . 7 (โŸจ1, 2โŸฉ โˆˆ V โˆง โŸจ2, 1โŸฉ โˆˆ V)
4036, 39pm3.2i 472 . . . . . 6 ((โŸจ1, 1โŸฉ โˆˆ V โˆง โŸจ2, 2โŸฉ โˆˆ V) โˆง (โŸจ1, 2โŸฉ โˆˆ V โˆง โŸจ2, 1โŸฉ โˆˆ V))
41 1ne2 12420 . . . . . . . . . 10 1 โ‰  2
4241olci 865 . . . . . . . . 9 (1 โ‰  1 โˆจ 1 โ‰  2)
43 1ex 11210 . . . . . . . . . 10 1 โˆˆ V
4443, 43opthne 5483 . . . . . . . . 9 (โŸจ1, 1โŸฉ โ‰  โŸจ1, 2โŸฉ โ†” (1 โ‰  1 โˆจ 1 โ‰  2))
4542, 44mpbir 230 . . . . . . . 8 โŸจ1, 1โŸฉ โ‰  โŸจ1, 2โŸฉ
4641orci 864 . . . . . . . . 9 (1 โ‰  2 โˆจ 1 โ‰  1)
4743, 43opthne 5483 . . . . . . . . 9 (โŸจ1, 1โŸฉ โ‰  โŸจ2, 1โŸฉ โ†” (1 โ‰  2 โˆจ 1 โ‰  1))
4846, 47mpbir 230 . . . . . . . 8 โŸจ1, 1โŸฉ โ‰  โŸจ2, 1โŸฉ
4945, 48pm3.2i 472 . . . . . . 7 (โŸจ1, 1โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ1, 1โŸฉ โ‰  โŸจ2, 1โŸฉ)
5049orci 864 . . . . . 6 ((โŸจ1, 1โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ1, 1โŸฉ โ‰  โŸจ2, 1โŸฉ) โˆจ (โŸจ2, 2โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ2, 2โŸฉ โ‰  โŸจ2, 1โŸฉ))
5140, 50pm3.2i 472 . . . . 5 (((โŸจ1, 1โŸฉ โˆˆ V โˆง โŸจ2, 2โŸฉ โˆˆ V) โˆง (โŸจ1, 2โŸฉ โˆˆ V โˆง โŸจ2, 1โŸฉ โˆˆ V)) โˆง ((โŸจ1, 1โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ1, 1โŸฉ โ‰  โŸจ2, 1โŸฉ) โˆจ (โŸจ2, 2โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ2, 2โŸฉ โ‰  โŸจ2, 1โŸฉ)))
5251a1i 11 . . . 4 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (((โŸจ1, 1โŸฉ โˆˆ V โˆง โŸจ2, 2โŸฉ โˆˆ V) โˆง (โŸจ1, 2โŸฉ โˆˆ V โˆง โŸจ2, 1โŸฉ โˆˆ V)) โˆง ((โŸจ1, 1โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ1, 1โŸฉ โ‰  โŸจ2, 1โŸฉ) โˆจ (โŸจ2, 2โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ2, 2โŸฉ โ‰  โŸจ2, 1โŸฉ))))
53 prneimg 4856 . . . . 5 (((โŸจ1, 1โŸฉ โˆˆ V โˆง โŸจ2, 2โŸฉ โˆˆ V) โˆง (โŸจ1, 2โŸฉ โˆˆ V โˆง โŸจ2, 1โŸฉ โˆˆ V)) โ†’ (((โŸจ1, 1โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ1, 1โŸฉ โ‰  โŸจ2, 1โŸฉ) โˆจ (โŸจ2, 2โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ2, 2โŸฉ โ‰  โŸจ2, 1โŸฉ)) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โ‰  {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}))
5453imp 408 . . . 4 ((((โŸจ1, 1โŸฉ โˆˆ V โˆง โŸจ2, 2โŸฉ โˆˆ V) โˆง (โŸจ1, 2โŸฉ โˆˆ V โˆง โŸจ2, 1โŸฉ โˆˆ V)) โˆง ((โŸจ1, 1โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ1, 1โŸฉ โ‰  โŸจ2, 1โŸฉ) โˆจ (โŸจ2, 2โŸฉ โ‰  โŸจ1, 2โŸฉ โˆง โŸจ2, 2โŸฉ โ‰  โŸจ2, 1โŸฉ))) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โ‰  {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})
55 disjsn2 4717 . . . 4 ({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โ‰  {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โ†’ ({{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}} โˆฉ {{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}}) = โˆ…)
5652, 54, 553syl 18 . . 3 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ({{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}} โˆฉ {{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}}) = โˆ…)
57 2nn 12285 . . . . . 6 2 โˆˆ โ„•
5818, 4, 15symg2bas 19260 . . . . . 6 ((1 โˆˆ V โˆง 2 โˆˆ โ„•) โ†’ (Baseโ€˜(SymGrpโ€˜๐‘)) = {{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}, {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}})
5943, 57, 58mp2an 691 . . . . 5 (Baseโ€˜(SymGrpโ€˜๐‘)) = {{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}, {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}}
60 df-pr 4632 . . . . 5 {{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}, {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}} = ({{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}} โˆช {{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}})
6159, 60eqtri 2761 . . . 4 (Baseโ€˜(SymGrpโ€˜๐‘)) = ({{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}} โˆช {{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}})
6261a1i 11 . . 3 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (Baseโ€˜(SymGrpโ€˜๐‘)) = ({{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}} โˆช {{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}}))
6311, 12, 14, 21, 33, 56, 62gsummptfidmsplit 19798 . 2 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))))) = ((๐‘… ฮฃg (๐‘˜ โˆˆ {{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}} โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))))))(+gโ€˜๐‘…)(๐‘… ฮฃg (๐‘˜ โˆˆ {{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}} โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))))))))
64 ringmnd 20066 . . . . . 6 (๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Mnd)
6564adantr 482 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘… โˆˆ Mnd)
66 prex 5433 . . . . . 6 {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โˆˆ V
6766a1i 11 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โˆˆ V)
6866prid1 4767 . . . . . . . . 9 {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โˆˆ {{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}, {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}}
6968, 59eleqtrri 2833 . . . . . . . 8 {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))
7069a1i 11 . . . . . . 7 (๐‘€ โˆˆ ๐ต โ†’ {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
714, 6, 5zrhpsgnelbas 21147 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin โˆง {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) โˆˆ (Baseโ€˜๐‘…))
7217, 71mp3an2 1450 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) โˆˆ (Baseโ€˜๐‘…))
7370, 72sylan2 594 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) โˆˆ (Baseโ€˜๐‘…))
7415, 4, 2, 3, 8m2detleiblem2 22130 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›))) โˆˆ (Baseโ€˜๐‘…))
7569, 74mp3an2 1450 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›))) โˆˆ (Baseโ€˜๐‘…))
7611, 7ringcl 20073 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) โˆˆ (Baseโ€˜๐‘…) โˆง ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›))) โˆˆ (Baseโ€˜๐‘…)) โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))) โˆˆ (Baseโ€˜๐‘…))
7722, 73, 75, 76syl3anc 1372 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))) โˆˆ (Baseโ€˜๐‘…))
78 2fveq3 6897 . . . . . . 7 (๐‘˜ = {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) = ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})))
79 fveq1 6891 . . . . . . . . . 10 (๐‘˜ = {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โ†’ (๐‘˜โ€˜๐‘›) = ({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›))
8079oveq1d 7424 . . . . . . . . 9 (๐‘˜ = {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โ†’ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›) = (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›))
8180mpteq2dv 5251 . . . . . . . 8 (๐‘˜ = {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โ†’ (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)) = (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))
8281oveq2d 7425 . . . . . . 7 (๐‘˜ = {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›))))
8378, 82oveq12d 7427 . . . . . 6 (๐‘˜ = {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))) = (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))))
8411, 83gsumsn 19822 . . . . 5 ((๐‘… โˆˆ Mnd โˆง {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โˆˆ V โˆง (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))) โˆˆ (Baseโ€˜๐‘…)) โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ {{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}} โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))))) = (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))))
8565, 67, 77, 84syl3anc 1372 . . . 4 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ {{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}} โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))))) = (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))))
86 prex 5433 . . . . . 6 {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โˆˆ V
8786a1i 11 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โˆˆ V)
8886prid2 4768 . . . . . . . . 9 {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โˆˆ {{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}, {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}}
8988, 59eleqtrri 2833 . . . . . . . 8 {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))
9089a1i 11 . . . . . . 7 (๐‘€ โˆˆ ๐ต โ†’ {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)))
914, 6, 5zrhpsgnelbas 21147 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ Fin โˆง {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) โˆˆ (Baseโ€˜๐‘…))
9217, 91mp3an2 1450 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘))) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) โˆˆ (Baseโ€˜๐‘…))
9390, 92sylan2 594 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) โˆˆ (Baseโ€˜๐‘…))
9415, 4, 2, 3, 8m2detleiblem2 22130 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โˆˆ (Baseโ€˜(SymGrpโ€˜๐‘)) โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›))) โˆˆ (Baseโ€˜๐‘…))
9589, 94mp3an2 1450 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›))) โˆˆ (Baseโ€˜๐‘…))
9611, 7ringcl 20073 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) โˆˆ (Baseโ€˜๐‘…) โˆง ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›))) โˆˆ (Baseโ€˜๐‘…)) โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))) โˆˆ (Baseโ€˜๐‘…))
9722, 93, 95, 96syl3anc 1372 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))) โˆˆ (Baseโ€˜๐‘…))
98 2fveq3 6897 . . . . . . 7 (๐‘˜ = {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) = ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})))
99 fveq1 6891 . . . . . . . . . 10 (๐‘˜ = {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐‘˜โ€˜๐‘›) = ({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›))
10099oveq1d 7424 . . . . . . . . 9 (๐‘˜ = {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โ†’ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›) = (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›))
101100mpteq2dv 5251 . . . . . . . 8 (๐‘˜ = {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โ†’ (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)) = (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))
102101oveq2d 7425 . . . . . . 7 (๐‘˜ = {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))) = ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›))))
10398, 102oveq12d 7427 . . . . . 6 (๐‘˜ = {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))) = (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))))
10411, 103gsumsn 19822 . . . . 5 ((๐‘… โˆˆ Mnd โˆง {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โˆˆ V โˆง (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))) โˆˆ (Baseโ€˜๐‘…)) โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ {{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}} โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))))) = (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))))
10565, 87, 97, 104syl3anc 1372 . . . 4 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ {{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}} โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›)))))) = (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))))
10685, 105oveq12d 7427 . . 3 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((๐‘… ฮฃg (๐‘˜ โˆˆ {{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}} โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))))))(+gโ€˜๐‘…)(๐‘… ฮฃg (๐‘˜ โˆˆ {{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}} โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))))))) = ((((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›))))(+gโ€˜๐‘…)(((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›))))))
107 eqidd 2734 . . . . . . 7 (๐‘€ โˆˆ ๐ต โ†’ {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} = {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})
108 eqid 2733 . . . . . . . 8 (1rโ€˜๐‘…) = (1rโ€˜๐‘…)
10915, 4, 5, 6, 108m2detleiblem5 22127 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} = {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) = (1rโ€˜๐‘…))
110107, 109sylan2 594 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) = (1rโ€˜๐‘…))
111 eqidd 2734 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} = {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})
1128, 7mgpplusg 19991 . . . . . . . 8 ยท = (+gโ€˜(mulGrpโ€˜๐‘…))
11315, 4, 2, 3, 8, 112m2detleiblem3 22131 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} = {โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ} โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›))) = ((1๐‘€1) ยท (2๐‘€2)))
11422, 111, 28, 113syl3anc 1372 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›))) = ((1๐‘€1) ยท (2๐‘€2)))
115110, 114oveq12d 7427 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))) = ((1rโ€˜๐‘…) ยท ((1๐‘€1) ยท (2๐‘€2))))
11643prid1 4767 . . . . . . . . . 10 1 โˆˆ {1, 2}
117116, 15eleqtrri 2833 . . . . . . . . 9 1 โˆˆ ๐‘
118117a1i 11 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ 1 โˆˆ ๐‘)
1193eleq2i 2826 . . . . . . . . . 10 (๐‘€ โˆˆ ๐ต โ†” ๐‘€ โˆˆ (Baseโ€˜๐ด))
120119biimpi 215 . . . . . . . . 9 (๐‘€ โˆˆ ๐ต โ†’ ๐‘€ โˆˆ (Baseโ€˜๐ด))
121120adantl 483 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ๐‘€ โˆˆ (Baseโ€˜๐ด))
1222, 11matecl 21927 . . . . . . . 8 ((1 โˆˆ ๐‘ โˆง 1 โˆˆ ๐‘ โˆง ๐‘€ โˆˆ (Baseโ€˜๐ด)) โ†’ (1๐‘€1) โˆˆ (Baseโ€˜๐‘…))
123118, 118, 121, 122syl3anc 1372 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (1๐‘€1) โˆˆ (Baseโ€˜๐‘…))
124 prid2g 4766 . . . . . . . . . . 11 (2 โˆˆ โ„• โ†’ 2 โˆˆ {1, 2})
12557, 124ax-mp 5 . . . . . . . . . 10 2 โˆˆ {1, 2}
126125, 15eleqtrri 2833 . . . . . . . . 9 2 โˆˆ ๐‘
127126a1i 11 . . . . . . . 8 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ 2 โˆˆ ๐‘)
1282, 11matecl 21927 . . . . . . . 8 ((2 โˆˆ ๐‘ โˆง 2 โˆˆ ๐‘ โˆง ๐‘€ โˆˆ (Baseโ€˜๐ด)) โ†’ (2๐‘€2) โˆˆ (Baseโ€˜๐‘…))
129127, 127, 121, 128syl3anc 1372 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (2๐‘€2) โˆˆ (Baseโ€˜๐‘…))
13011, 7ringcl 20073 . . . . . . 7 ((๐‘… โˆˆ Ring โˆง (1๐‘€1) โˆˆ (Baseโ€˜๐‘…) โˆง (2๐‘€2) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((1๐‘€1) ยท (2๐‘€2)) โˆˆ (Baseโ€˜๐‘…))
13122, 123, 129, 130syl3anc 1372 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((1๐‘€1) ยท (2๐‘€2)) โˆˆ (Baseโ€˜๐‘…))
13211, 7, 108ringlidm 20086 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ((1๐‘€1) ยท (2๐‘€2)) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((1rโ€˜๐‘…) ยท ((1๐‘€1) ยท (2๐‘€2))) = ((1๐‘€1) ยท (2๐‘€2)))
133131, 132syldan 592 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((1rโ€˜๐‘…) ยท ((1๐‘€1) ยท (2๐‘€2))) = ((1๐‘€1) ยท (2๐‘€2)))
134115, 133eqtrd 2773 . . . 4 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))) = ((1๐‘€1) ยท (2๐‘€2)))
135 eqidd 2734 . . . . . 6 (๐‘€ โˆˆ ๐ต โ†’ {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} = {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})
136 eqid 2733 . . . . . . 7 (invgโ€˜๐‘…) = (invgโ€˜๐‘…)
13715, 4, 5, 6, 108, 136m2detleiblem6 22128 . . . . . 6 ((๐‘… โˆˆ Ring โˆง {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} = {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) = ((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…)))
138135, 137sylan2 594 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) = ((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…)))
139 eqidd 2734 . . . . . 6 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} = {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})
14015, 4, 2, 3, 8, 112m2detleiblem4 22132 . . . . . 6 ((๐‘… โˆˆ Ring โˆง {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} = {โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ} โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›))) = ((2๐‘€1) ยท (1๐‘€2)))
14122, 139, 28, 140syl3anc 1372 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›))) = ((2๐‘€1) ยท (1๐‘€2)))
142138, 141oveq12d 7427 . . . 4 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›)))) = (((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…)) ยท ((2๐‘€1) ยท (1๐‘€2))))
143134, 142oveq12d 7427 . . 3 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}โ€˜๐‘›)๐‘€๐‘›))))(+gโ€˜๐‘…)(((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ})) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ (({โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}โ€˜๐‘›)๐‘€๐‘›))))) = (((1๐‘€1) ยท (2๐‘€2))(+gโ€˜๐‘…)(((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…)) ยท ((2๐‘€1) ยท (1๐‘€2)))))
1442, 11matecl 21927 . . . . . 6 ((2 โˆˆ ๐‘ โˆง 1 โˆˆ ๐‘ โˆง ๐‘€ โˆˆ (Baseโ€˜๐ด)) โ†’ (2๐‘€1) โˆˆ (Baseโ€˜๐‘…))
145127, 118, 121, 144syl3anc 1372 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (2๐‘€1) โˆˆ (Baseโ€˜๐‘…))
1462, 11matecl 21927 . . . . . 6 ((1 โˆˆ ๐‘ โˆง 2 โˆˆ ๐‘ โˆง ๐‘€ โˆˆ (Baseโ€˜๐ด)) โ†’ (1๐‘€2) โˆˆ (Baseโ€˜๐‘…))
147118, 127, 121, 146syl3anc 1372 . . . . 5 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (1๐‘€2) โˆˆ (Baseโ€˜๐‘…))
14811, 7ringcl 20073 . . . . 5 ((๐‘… โˆˆ Ring โˆง (2๐‘€1) โˆˆ (Baseโ€˜๐‘…) โˆง (1๐‘€2) โˆˆ (Baseโ€˜๐‘…)) โ†’ ((2๐‘€1) ยท (1๐‘€2)) โˆˆ (Baseโ€˜๐‘…))
14922, 145, 147, 148syl3anc 1372 . . . 4 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((2๐‘€1) ยท (1๐‘€2)) โˆˆ (Baseโ€˜๐‘…))
150 m2detleib.m . . . . 5 โˆ’ = (-gโ€˜๐‘…)
15115, 4, 5, 6, 108, 136, 7, 150m2detleiblem7 22129 . . . 4 ((๐‘… โˆˆ Ring โˆง ((1๐‘€1) ยท (2๐‘€2)) โˆˆ (Baseโ€˜๐‘…) โˆง ((2๐‘€1) ยท (1๐‘€2)) โˆˆ (Baseโ€˜๐‘…)) โ†’ (((1๐‘€1) ยท (2๐‘€2))(+gโ€˜๐‘…)(((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…)) ยท ((2๐‘€1) ยท (1๐‘€2)))) = (((1๐‘€1) ยท (2๐‘€2)) โˆ’ ((2๐‘€1) ยท (1๐‘€2))))
15222, 131, 149, 151syl3anc 1372 . . 3 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (((1๐‘€1) ยท (2๐‘€2))(+gโ€˜๐‘…)(((invgโ€˜๐‘…)โ€˜(1rโ€˜๐‘…)) ยท ((2๐‘€1) ยท (1๐‘€2)))) = (((1๐‘€1) ยท (2๐‘€2)) โˆ’ ((2๐‘€1) ยท (1๐‘€2))))
153106, 143, 1523eqtrd 2777 . 2 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ ((๐‘… ฮฃg (๐‘˜ โˆˆ {{โŸจ1, 1โŸฉ, โŸจ2, 2โŸฉ}} โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))))))(+gโ€˜๐‘…)(๐‘… ฮฃg (๐‘˜ โˆˆ {{โŸจ1, 2โŸฉ, โŸจ2, 1โŸฉ}} โ†ฆ (((โ„คRHomโ€˜๐‘…)โ€˜((pmSgnโ€˜๐‘)โ€˜๐‘˜)) ยท ((mulGrpโ€˜๐‘…) ฮฃg (๐‘› โˆˆ ๐‘ โ†ฆ ((๐‘˜โ€˜๐‘›)๐‘€๐‘›))))))) = (((1๐‘€1) ยท (2๐‘€2)) โˆ’ ((2๐‘€1) ยท (1๐‘€2))))
15410, 63, 1533eqtrd 2777 1 ((๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต) โ†’ (๐ทโ€˜๐‘€) = (((1๐‘€1) ยท (2๐‘€2)) โˆ’ ((2๐‘€1) ยท (1๐‘€2))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941  Vcvv 3475   โˆช cun 3947   โˆฉ cin 3948  โˆ…c0 4323  {csn 4629  {cpr 4631  โŸจcop 4635   โ†ฆ cmpt 5232  โ€˜cfv 6544  (class class class)co 7409  Fincfn 8939  1c1 11111  โ„•cn 12212  2c2 12267  Basecbs 17144  +gcplusg 17197  .rcmulr 17198   ฮฃg cgsu 17386  Mndcmnd 18625  invgcminusg 18820  -gcsg 18821  SymGrpcsymg 19234  pmSgncpsgn 19357  CMndccmn 19648  mulGrpcmgp 19987  1rcur 20004  Ringcrg 20056  โ„ค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-oadd 8470  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-dju 9896  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-fac 14234  df-bc 14263  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-sbg 18824  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-cmn 19650  df-abl 19651  df-mgp 19988  df-ur 20005  df-ring 20058  df-cring 20059  df-rnghom 20251  df-subrg 20317  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:  lmat22det  32802
  Copyright terms: Public domain W3C validator