$( <MM> <PROOF_ASST> THEOREM=z5_zkh  LOC_AFTER=?

h1::z5_zkh.1  |- Y = ( Z/nZ ` 5 )
h2::z5_zkh.2  |- I = ( invr ` Y )
h3::z5_zkh.3  |- R = ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) )

d1::eqid           |- ( Base ` Y ) = ( Base ` Y )
d11::eqid          |- ( RSpan ` ZZring ) = ( RSpan ` ZZring )
d2::eqid           |- ( .r ` Y ) = ( .r ` Y )
d3::eqid           |- ( 1r ` Y ) = ( 1r ` Y )
d4::eqid           |- ( Unit ` Y ) = ( Unit ` Y )
d28::eqid          |- ( ZRHom ` Y ) = ( ZRHom ` Y )
d34::eqid          |- ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
4::2z              |- 2 e. ZZ
5::3z              |- 3 e. ZZ
7::5nn0            |- 5 e. NN0
7a::1z             |- 1 e. ZZ
7b::6nn            |- 6 e. NN
7c:7b:nnzi         |- 6 e. ZZ
7d:7:nn0zi         |- 5 e. ZZ
8:1:zncrng         |- ( 5 e. NN0 -> Y e. CRing )
9::crngring        |- ( Y e. CRing -> Y e. Ring )
10:7,8,9:mp2b      |- Y e. Ring
d6:10:a1i          |- ( T. -> Y e. Ring )
**
11:d11,1,3:znbas   |- ( 5 e. NN0 -> ( ZZ /. R ) = ( Base ` Y ) )
20:7,11:ax-mp      |- ( ZZ /. R ) = ( Base ` Y )
21::ovex           |- ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) e. _V
d12:3,21:eqeltri   |- R e. _V
30:d12:ecelqsi     |- ( 2 e. ZZ -> [ 2 ] R e. ( ZZ /. R ) )
40:d12:ecelqsi     |- ( 3 e. ZZ -> [ 3 ] R e. ( ZZ /. R ) )
35:4,30:ax-mp      |- [ 2 ] R e. ( ZZ /. R )
45:5,40:ax-mp      |- [ 3 ] R e. ( ZZ /. R )
37:35,20:eleqtri   |- [ 2 ] R e. ( Base ` Y )
47:45,20:eleqtri   |- [ 3 ] R e. ( Base ` Y )
d7:47:a1i          |- ( T. -> [ 3 ] R e. ( Base ` Y ) )
d8:37:a1i          |- ( T. -> [ 2 ] R e. ( Base ` Y ) )
*
50:7,8:ax-mp       |- Y e. CRing

d16::eqid          |- ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) ) = ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) )
60:d11,d16,1:znmul |- ( 5 e. NN0 -> ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) ) ) = ( .r ` Y ) )
61:7,60:ax-mp      |- ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) ) ) = ( .r ` Y )
62:61:oveqi        |- ( [ 3 ] R ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) ) ) [ 2 ] R ) = ( [ 3 ] R ( .r ` Y ) [ 2 ] R )
d32:3:a1i          |- ( T. -> R = ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) )
d25:d32:eqcomd     |- ( T. -> ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) = R )
d17:d25:oveq2d     |- ( T. -> ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) ) = ( ZZring /s R ) )
d26::zringbas      |- ZZ = ( Base ` ZZring )
149::zringring     |- ZZring e. Ring
d18:d26:a1i        |- ( T. -> ZZ = ( Base ` ZZring ) )
29:d26,3:eqger     |- ( ( ( RSpan ` ZZring ) ` { 5 } ) e. ( SubGrp ` ZZring ) -> R Er ZZ )
150:d11:znlidl     |- ( 5 e. ZZ -> ( ( RSpan ` ZZring ) ` { 5 } ) e. ( LIdeal ` ZZring ) )
151:7d,150:ax-mp   |- ( ( RSpan ` ZZring ) ` { 5 } ) e. ( LIdeal ` ZZring )
152:d34:lidlsubg   |- ( ( ZZring e. Ring /\ ( ( RSpan ` ZZring ) ` { 5 } ) e. ( LIdeal ` ZZring ) ) -> ( ( RSpan ` ZZring ) ` { 5 } ) e. ( SubGrp ` ZZring ) )
298:149,151,152:mp2an |- ( ( RSpan ` ZZring ) ` { 5 } ) e. ( SubGrp ` ZZring )
299:298,29:ax-mp   |- R Er ZZ
d19:299:a1i        |- ( T. -> R Er ZZ )
d20:149:a1i        |- ( T. -> ZZring e. Ring )
d24::eqid          |- ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) ) ) = ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { 5 } ) ) ) )
590:d28:zrhrhm     |- ( Y e. Ring -> ( ZRHom ` Y ) e. ( ZZring RingHom Y ) )
595:10,590:ax-mp   |- ( ZRHom ` Y ) e. ( ZZring RingHom Y )
d35::zringmulr     |- x. = ( .r ` ZZring )
600:d26,d35,d2:rhmmul |- ( ( ( ZRHom ` Y ) e. ( ZZring RingHom Y ) /\ 3 e. ZZ /\ 2 e. ZZ ) -> ( ( ZRHom ` Y ) ` ( 3 x. 2 ) ) = ( ( ( ZRHom ` Y ) ` 3 ) ( .r ` Y ) ( ( ZRHom ` Y ) ` 2 ) ) )
601:595,5,4,600:mp3an |- ( ( ZRHom ` Y ) ` ( 3 x. 2 ) ) = ( ( ( ZRHom ` Y ) ` 3 ) ( .r ` Y ) ( ( ZRHom ` Y ) ` 2 ) )
66::tru            |- T.

72::3t2e6          |- ( 3 x. 2 ) = 6
73::fveq2          |- ( ( 3 x. 2 ) = 6 -> ( ( ZRHom ` Y ) ` ( 3 x. 2 ) ) = ( ( ZRHom ` Y ) ` 6 ) )
75:72,73:ax-mp     |- ( ( ZRHom ` Y ) ` ( 3 x. 2 ) ) = ( ( ZRHom ` Y ) ` 6 )
80:1,d28:zndvds    |- ( ( 5 e. NN0 /\ 6 e. ZZ /\ 1 e. ZZ ) -> ( ( ( ZRHom ` Y ) ` 6 ) = ( ( ZRHom ` Y ) ` 1 ) <-> 5 || ( 6 - 1 ) ) )
81:7,7c,7a,80:mp3an |- ( ( ( ZRHom ` Y ) ` 6 ) = ( ( ZRHom ` Y ) ` 1 ) <-> 5 || ( 6 - 1 ) )
300::iddvds        |- ( 5 e. ZZ -> 5 || 5 )
310:7d,300:ax-mp   |- 5 || 5
d29::5cn           |- 5 e. CC
d30::ax1cn         |- 1 e. CC
d31::5p1e6         |- ( 5 + 1 ) = 6
311:d29,d30,d31:mvlraddi 
                   |- 5 = ( 6 - 1 )
320:311:eqcomi     |- ( 6 - 1 ) = 5
330:320:breq2i     |- ( 5 || ( 6 - 1 ) <-> 5 || 5 )
335:310,330:mpbir  |- 5 || ( 6 - 1 )
340:335,81:mpbir   |- ( ( ZRHom ` Y ) ` 6 ) = ( ( ZRHom ` Y ) ` 1 )
350:d11,3,1,d28:znzrhval |- ( ( 5 e. NN0 /\ 6 e. ZZ ) -> ( ( ZRHom ` Y ) ` 6 ) = [ 6 ] R )
390:d11,3,1,d28:znzrhval |- ( ( 5 e. NN0 /\ 3 e. ZZ ) -> ( ( ZRHom ` Y ) ` 3 ) = [ 3 ] R )
380:d11,3,1,d28:znzrhval |- ( ( 5 e. NN0 /\ 2 e. ZZ ) -> ( ( ZRHom ` Y ) ` 2 ) = [ 2 ] R )
200:d11,3,1,d28:znzrhval |- ( ( 5 e. NN0 /\ 1 e. ZZ ) -> ( ( ZRHom ` Y ) ` 1 ) = [ 1 ] R )
360:7,7c,350:mp2an |- ( ( ZRHom ` Y ) ` 6 ) = [ 6 ] R
361:7,5,390:mp2an  |- ( ( ZRHom ` Y ) ` 3 ) = [ 3 ] R
36:7,4,380:mp2an   |- ( ( ZRHom ` Y ) ` 2 ) = [ 2 ] R
370:7,7a,200:mp2an |- ( ( ZRHom ` Y ) ` 1 ) = [ 1 ] R
82:340,360,370:3eqtr3i |- [ 6 ] R = [ 1 ] R
201:7,7a,200:mp2an |-  ( ( ZRHom ` Y ) ` 1 ) = [ 1 ] R
210:d28,d3:zrh1    |- ( Y e. Ring -> ( ( ZRHom ` Y ) ` 1 ) = ( 1r ` Y ) )
215:10,210:ax-mp   |- ( ( ZRHom ` Y ) ` 1 ) = ( 1r ` Y )
220:215,201:eqtr3i |- ( 1r ` Y ) = [ 1 ] R
400:361,36:oveq12i |- ( ( ( ZRHom ` Y ) ` 3 ) ( .r ` Y ) ( ( ZRHom ` Y ) ` 2 ) ) = ( [ 3 ] R ( .r ` Y ) [ 2 ] R )

401:75,601,340:3eqtr3i |- ( ( ( ZRHom ` Y ) ` 3 ) ( .r ` Y ) ( ( ZRHom ` Y ) ` 2 ) ) = ( ( ZRHom ` Y ) ` 1 )
d13:401,400,215:3eqtr3i |- ( [ 3 ] R ( .r ` Y ) [ 2 ] R ) = ( 1r ` Y )
*
90:d1,d2:crngcom   |- ( ( Y e. CRing /\ [ 3 ] R e. ( Base ` Y ) /\ [ 2 ] R e. ( Base ` Y ) ) -> ( [ 3 ] R ( .r ` Y ) [ 2 ] R ) = ( [ 2 ] R ( .r ` Y ) [ 3 ] R ) )
95:50,47,37,90:mp3an |- ( [ 3 ] R ( .r ` Y ) [ 2 ] R ) = ( [ 2 ] R ( .r ` Y ) [ 3 ] R )
d14:95,d13:eqtr3i  |- ( [ 2 ] R ( .r ` Y ) [ 3 ] R ) = ( 1r ` Y )
d9:d13:a1i         |- ( T. -> ( [ 3 ] R ( .r ` Y ) [ 2 ] R ) = ( 1r ` Y ) )
d10:d14:a1i        |- ( T. -> ( [ 2 ] R ( .r ` Y ) [ 3 ] R ) = ( 1r ` Y ) )
100:d1,d2,d3,d4,2,d6,d7,d8,d9,d10:invrvald 
                   |- ( T. -> ( [ 3 ] R e. ( Unit ` Y ) /\ ( I ` [ 3 ] R ) = [ 2 ] R ) )
110:100:trud       |- ( [ 3 ] R e. ( Unit ` Y ) /\ ( I ` [ 3 ] R ) = [ 2 ] R )
qed:110:simpri     |- ( I ` [ 3 ] R ) = [ 2 ] R
$=  ( z5_zkh.1 c3 cfv wcel c2 wceq wtru eqid c5 5nn0 a1i cz zring co ax-mp c1
    c6 z5_zkh.2 z5_zkh.3 cec cui wa cbs cmulr cur crg ccrg zncrng crngring mp2b
    cn0 cqs 3z csn crsp cqg cvv ovex eqeltri ecelqsi znbas eleqtri 2z czrh cmul
    3t2e6 fveq2 crh zrhrhm zringbas zringmulr rhmmul mp3an cmin cdvds wbr nn0zi
    iddvds 5cn ax1cn 5p1e6 mvlraddi eqcomi breq2i mpbir 6nn nnzi zndvds 3eqtr3i
    wb 1z znzrhval mp2an oveq12i zrh1 crngcom eqtr3i invrvald trud simpri ) EAU
    CZCUDFZGZXDBFHAUCZIZXFXHUEJCUFFZCCUGFZXECUHFZBXDXGXIKZXJKZXKKZXEKUACUIGZJLU
    NGZCUJGZXOMLCDUKZCULUMZNXDXIGZJXDOAUOZXIEOGZXDYAGUPOEAAPLUQPURFZFZUSQUTUBPY
    DUSVAVBZVCRXPYAXIIMAYCLCYCKZDUBVDRZVEZNXGXIGZJXGYAXIHOGZXGYAGVFOHAYEVCRYGVE
    ZNXDXGXJQZXKIJECVGFZFZHYMFZXJQZSYMFZYLXKEHVHQZYMFZTYMFZYPYQYRTIYSYTIVIYRTYM
    VJRYMPCVKQGZYBYJYSYPIXOUUAXSCYMYMKZVLRUPVFEHPCVHXJYMOVMVNXMVOVPYTYQIZLTSVQQ
    ZVRVSZUUELLVRVSZLOGUUFLMVTLWARUUDLLVRLUUDLSTWBWCWDWEWFWGWHXPTOGSOGUUCUUEWMM
    TWIWJWNTSYMLCDUUBWKVPWHWLYNXDYOXGXJXPYBYNXDIMUPEAYCYMLCYFUBDUUBWOWPXPYJYOXG
    IMVFHAYCYMLCYFUBDUUBWOWPWQXOYQXKIXSCXKYMUUBXNWRRWLZNXGXDXJQZXKIJYLUUHXKXQXT
    YIYLUUHIXPXQMXRRYHYKXICXJXDXGXLXMWSVPUUGWTNXAXBXC $.
$)