Metamath Proof Explorer

Theorem wilthlem2

Description: Lemma for wilth : induction step. The "hand proof" version of this theorem works by writing out the list of all numbers from 1 to P - 1 in pairs such that a number is paired with its inverse. Every number has a unique inverse different from itself except 1 and P - 1 , and so each pair multiplies to 1 , and 1 and P - 1 == -u 1 multiply to -u 1 , so the full product is equal to -u 1 . Here we make this precise by doing the product pair by pair.

The induction hypothesis says that every subset S of 1 ... ( P - 1 ) that is closed under inverse (i.e. all pairs are matched up) and contains P - 1 multiplies to -u 1 mod P . Given such a set, we take out one element z =/= P - 1 . If there are no such elements, then S = { P - 1 } which forms the base case. Otherwise, S \ { z , z ^ -u 1 } is also closed under inverse and contains P - 1 , so the induction hypothesis says that this equals -u 1 ; and the remaining two elements are either equal to each other, in which case wilthlem1 gives that z = 1 or P - 1 , and we've already excluded the second case, so the product gives 1 ; or z =/= z ^ -u 1 and their product is 1 . In either case the accumulated product is unaffected. (Contributed by Mario Carneiro, 24-Jan-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses wilthlem.t โŠข ๐‘‡ = ( mulGrp โ€˜ โ„‚fld )
wilthlem.a โŠข ๐ด = { ๐‘ฅ โˆˆ ๐’ซ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆฃ ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘ฅ โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘ฅ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘ฅ ) }
wilthlem2.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™ )
wilthlem2.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ ๐ด )
wilthlem2.r โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘  โˆˆ ๐ด ( ๐‘  โŠŠ ๐‘† โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘  ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
Assertion wilthlem2 ( ๐œ‘ โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )

Proof

Step Hyp Ref Expression
1 wilthlem.t โŠข ๐‘‡ = ( mulGrp โ€˜ โ„‚fld )
2 wilthlem.a โŠข ๐ด = { ๐‘ฅ โˆˆ ๐’ซ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆฃ ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘ฅ โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘ฅ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘ฅ ) }
3 wilthlem2.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™ )
4 wilthlem2.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ ๐ด )
5 wilthlem2.r โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘  โˆˆ ๐ด ( ๐‘  โŠŠ ๐‘† โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘  ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
6 simpr โŠข ( ( ๐œ‘ โˆง ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } )
7 eleq2 โŠข ( ๐‘ฅ = ๐‘† โ†’ ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘ฅ โ†” ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘† ) )
8 eleq2 โŠข ( ๐‘ฅ = ๐‘† โ†’ ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘ฅ โ†” ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† ) )
9 8 raleqbi1dv โŠข ( ๐‘ฅ = ๐‘† โ†’ ( โˆ€ ๐‘ฆ โˆˆ ๐‘ฅ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘ฅ โ†” โˆ€ ๐‘ฆ โˆˆ ๐‘† ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† ) )
10 7 9 anbi12d โŠข ( ๐‘ฅ = ๐‘† โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘ฅ โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘ฅ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘ฅ ) โ†” ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘† โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘† ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† ) ) )
11 10 2 elrab2 โŠข ( ๐‘† โˆˆ ๐ด โ†” ( ๐‘† โˆˆ ๐’ซ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘† โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘† ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† ) ) )
12 4 11 sylib โŠข ( ๐œ‘ โ†’ ( ๐‘† โˆˆ ๐’ซ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘† โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘† ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† ) ) )
13 12 simprd โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘† โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘† ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† ) )
14 13 simpld โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘† )
15 14 snssd โŠข ( ๐œ‘ โ†’ { ( ๐‘ƒ โˆ’ 1 ) } โŠ† ๐‘† )
16 15 adantr โŠข ( ( ๐œ‘ โˆง ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ { ( ๐‘ƒ โˆ’ 1 ) } โŠ† ๐‘† )
17 6 16 eqssd โŠข ( ( ๐œ‘ โˆง ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ ๐‘† = { ( ๐‘ƒ โˆ’ 1 ) } )
18 17 reseq2d โŠข ( ( ๐œ‘ โˆง ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ ( I โ†พ ๐‘† ) = ( I โ†พ { ( ๐‘ƒ โˆ’ 1 ) } ) )
19 mptresid โŠข ( I โ†พ { ( ๐‘ƒ โˆ’ 1 ) } ) = ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†ฆ ๐‘ง )
20 18 19 eqtrdi โŠข ( ( ๐œ‘ โˆง ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ ( I โ†พ ๐‘† ) = ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†ฆ ๐‘ง ) )
21 20 oveq2d โŠข ( ( ๐œ‘ โˆง ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) = ( ๐‘‡ ฮฃg ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†ฆ ๐‘ง ) ) )
22 21 oveq1d โŠข ( ( ๐œ‘ โˆง ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) mod ๐‘ƒ ) = ( ( ๐‘‡ ฮฃg ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†ฆ ๐‘ง ) ) mod ๐‘ƒ ) )
23 prmnn โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„• )
24 3 23 syl โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„• )
25 24 nncnd โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚ )
26 ax-1cn โŠข 1 โˆˆ โ„‚
27 negsub โŠข ( ( ๐‘ƒ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ ) โ†’ ( ๐‘ƒ + - 1 ) = ( ๐‘ƒ โˆ’ 1 ) )
28 25 26 27 sylancl โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ + - 1 ) = ( ๐‘ƒ โˆ’ 1 ) )
29 neg1cn โŠข - 1 โˆˆ โ„‚
30 addcom โŠข ( ( ๐‘ƒ โˆˆ โ„‚ โˆง - 1 โˆˆ โ„‚ ) โ†’ ( ๐‘ƒ + - 1 ) = ( - 1 + ๐‘ƒ ) )
31 25 29 30 sylancl โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ + - 1 ) = ( - 1 + ๐‘ƒ ) )
32 28 31 eqtr3d โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โˆ’ 1 ) = ( - 1 + ๐‘ƒ ) )
33 cnring โŠข โ„‚fld โˆˆ Ring
34 1 ringmgp โŠข ( โ„‚fld โˆˆ Ring โ†’ ๐‘‡ โˆˆ Mnd )
35 33 34 mp1i โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ Mnd )
36 nnm1nn0 โŠข ( ๐‘ƒ โˆˆ โ„• โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„•0 )
37 24 36 syl โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„•0 )
38 37 nn0cnd โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„‚ )
39 cnfldbas โŠข โ„‚ = ( Base โ€˜ โ„‚fld )
40 1 39 mgpbas โŠข โ„‚ = ( Base โ€˜ ๐‘‡ )
41 id โŠข ( ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) โ†’ ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) )
42 40 41 gsumsn โŠข ( ( ๐‘‡ โˆˆ Mnd โˆง ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„‚ โˆง ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„‚ ) โ†’ ( ๐‘‡ ฮฃg ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†ฆ ๐‘ง ) ) = ( ๐‘ƒ โˆ’ 1 ) )
43 35 38 38 42 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐‘‡ ฮฃg ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†ฆ ๐‘ง ) ) = ( ๐‘ƒ โˆ’ 1 ) )
44 25 mullidd โŠข ( ๐œ‘ โ†’ ( 1 ยท ๐‘ƒ ) = ๐‘ƒ )
45 44 oveq2d โŠข ( ๐œ‘ โ†’ ( - 1 + ( 1 ยท ๐‘ƒ ) ) = ( - 1 + ๐‘ƒ ) )
46 32 43 45 3eqtr4d โŠข ( ๐œ‘ โ†’ ( ๐‘‡ ฮฃg ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†ฆ ๐‘ง ) ) = ( - 1 + ( 1 ยท ๐‘ƒ ) ) )
47 46 oveq1d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ ฮฃg ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†ฆ ๐‘ง ) ) mod ๐‘ƒ ) = ( ( - 1 + ( 1 ยท ๐‘ƒ ) ) mod ๐‘ƒ ) )
48 neg1rr โŠข - 1 โˆˆ โ„
49 48 a1i โŠข ( ๐œ‘ โ†’ - 1 โˆˆ โ„ )
50 24 nnrpd โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„+ )
51 1zzd โŠข ( ๐œ‘ โ†’ 1 โˆˆ โ„ค )
52 modcyc โŠข ( ( - 1 โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ โˆง 1 โˆˆ โ„ค ) โ†’ ( ( - 1 + ( 1 ยท ๐‘ƒ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
53 49 50 51 52 syl3anc โŠข ( ๐œ‘ โ†’ ( ( - 1 + ( 1 ยท ๐‘ƒ ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
54 47 53 eqtrd โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ ฮฃg ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†ฆ ๐‘ง ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
55 54 adantr โŠข ( ( ๐œ‘ โˆง ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ ( ( ๐‘‡ ฮฃg ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†ฆ ๐‘ง ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
56 22 55 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
57 56 ex โŠข ( ๐œ‘ โ†’ ( ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
58 nss โŠข ( ยฌ ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } โ†” โˆƒ ๐‘ง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) )
59 cnfld1 โŠข 1 = ( 1r โ€˜ โ„‚fld )
60 1 59 ringidval โŠข 1 = ( 0g โ€˜ ๐‘‡ )
61 cnfldmul โŠข ยท = ( .r โ€˜ โ„‚fld )
62 1 61 mgpplusg โŠข ยท = ( +g โ€˜ ๐‘‡ )
63 cncrng โŠข โ„‚fld โˆˆ CRing
64 1 crngmgp โŠข ( โ„‚fld โˆˆ CRing โ†’ ๐‘‡ โˆˆ CMnd )
65 63 64 ax-mp โŠข ๐‘‡ โˆˆ CMnd
66 65 a1i โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘‡ โˆˆ CMnd )
67 4 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘† โˆˆ ๐ด )
68 f1oi โŠข ( I โ†พ ๐‘† ) : ๐‘† โ€“1-1-ontoโ†’ ๐‘†
69 f1of โŠข ( ( I โ†พ ๐‘† ) : ๐‘† โ€“1-1-ontoโ†’ ๐‘† โ†’ ( I โ†พ ๐‘† ) : ๐‘† โŸถ ๐‘† )
70 68 69 ax-mp โŠข ( I โ†พ ๐‘† ) : ๐‘† โŸถ ๐‘†
71 12 simpld โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ ๐’ซ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) )
72 71 elpwid โŠข ( ๐œ‘ โ†’ ๐‘† โŠ† ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) )
73 fzssz โŠข ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โŠ† โ„ค
74 72 73 sstrdi โŠข ( ๐œ‘ โ†’ ๐‘† โŠ† โ„ค )
75 zsscn โŠข โ„ค โŠ† โ„‚
76 74 75 sstrdi โŠข ( ๐œ‘ โ†’ ๐‘† โŠ† โ„‚ )
77 fss โŠข ( ( ( I โ†พ ๐‘† ) : ๐‘† โŸถ ๐‘† โˆง ๐‘† โŠ† โ„‚ ) โ†’ ( I โ†พ ๐‘† ) : ๐‘† โŸถ โ„‚ )
78 70 76 77 sylancr โŠข ( ๐œ‘ โ†’ ( I โ†พ ๐‘† ) : ๐‘† โŸถ โ„‚ )
79 78 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( I โ†พ ๐‘† ) : ๐‘† โŸถ โ„‚ )
80 fzfi โŠข ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆˆ Fin
81 ssfi โŠข ( ( ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆˆ Fin โˆง ๐‘† โŠ† ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ) โ†’ ๐‘† โˆˆ Fin )
82 80 72 81 sylancr โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ Fin )
83 1ex โŠข 1 โˆˆ V
84 83 a1i โŠข ( ๐œ‘ โ†’ 1 โˆˆ V )
85 78 82 84 fdmfifsupp โŠข ( ๐œ‘ โ†’ ( I โ†พ ๐‘† ) finSupp 1 )
86 85 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( I โ†พ ๐‘† ) finSupp 1 )
87 disjdif โŠข ( { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โˆฉ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = โˆ…
88 87 a1i โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โˆฉ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = โˆ… )
89 undif2 โŠข ( { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โˆช ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = ( { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โˆช ๐‘† )
90 simprl โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ง โˆˆ ๐‘† )
91 oveq1 โŠข ( ๐‘ฆ = ๐‘ง โ†’ ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) = ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) )
92 91 oveq1d โŠข ( ๐‘ฆ = ๐‘ง โ†’ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
93 92 eleq1d โŠข ( ๐‘ฆ = ๐‘ง โ†’ ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† โ†” ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† ) )
94 13 simprd โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฆ โˆˆ ๐‘† ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† )
95 94 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ โˆ€ ๐‘ฆ โˆˆ ๐‘† ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† )
96 93 95 90 rspcdva โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† )
97 90 96 prssd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โŠ† ๐‘† )
98 ssequn1 โŠข ( { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โŠ† ๐‘† โ†” ( { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โˆช ๐‘† ) = ๐‘† )
99 97 98 sylib โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โˆช ๐‘† ) = ๐‘† )
100 89 99 eqtr2id โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘† = ( { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โˆช ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) )
101 40 60 62 66 67 79 86 88 100 gsumsplit โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) = ( ( ๐‘‡ ฮฃg ( ( I โ†พ ๐‘† ) โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ยท ( ๐‘‡ ฮฃg ( ( I โ†พ ๐‘† ) โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) )
102 97 resabs1d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( I โ†พ ๐‘† ) โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) = ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
103 102 oveq2d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘‡ ฮฃg ( ( I โ†พ ๐‘† ) โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) )
104 difss โŠข ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠ† ๐‘†
105 resabs1 โŠข ( ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠ† ๐‘† โ†’ ( ( I โ†พ ๐‘† ) โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) )
106 104 105 ax-mp โŠข ( ( I โ†พ ๐‘† ) โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
107 106 oveq2i โŠข ( ๐‘‡ ฮฃg ( ( I โ†พ ๐‘† ) โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) = ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) )
108 107 a1i โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘‡ ฮฃg ( ( I โ†พ ๐‘† ) โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) = ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) )
109 103 108 oveq12d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘‡ ฮฃg ( ( I โ†พ ๐‘† ) โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ยท ( ๐‘‡ ฮฃg ( ( I โ†พ ๐‘† ) โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) = ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ยท ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) )
110 101 109 eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) = ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ยท ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) )
111 110 oveq1d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) mod ๐‘ƒ ) = ( ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ยท ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) mod ๐‘ƒ ) )
112 prfi โŠข { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โˆˆ Fin
113 112 a1i โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โˆˆ Fin )
114 zsubrg โŠข โ„ค โˆˆ ( SubRing โ€˜ โ„‚fld )
115 1 subrgsubm โŠข ( โ„ค โˆˆ ( SubRing โ€˜ โ„‚fld ) โ†’ โ„ค โˆˆ ( SubMnd โ€˜ ๐‘‡ ) )
116 114 115 mp1i โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ โ„ค โˆˆ ( SubMnd โ€˜ ๐‘‡ ) )
117 f1oi โŠข ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) : { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ€“1-1-ontoโ†’ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) }
118 f1of โŠข ( ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) : { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ€“1-1-ontoโ†’ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ†’ ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) : { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โŸถ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
119 117 118 ax-mp โŠข ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) : { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โŸถ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) }
120 74 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘† โŠ† โ„ค )
121 97 120 sstrd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โŠ† โ„ค )
122 fss โŠข ( ( ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) : { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โŸถ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โˆง { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โŠ† โ„ค ) โ†’ ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) : { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โŸถ โ„ค )
123 119 121 122 sylancr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) : { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โŸถ โ„ค )
124 83 a1i โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ 1 โˆˆ V )
125 123 113 124 fdmfifsupp โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) finSupp 1 )
126 60 66 113 116 123 125 gsumsubmcl โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) โˆˆ โ„ค )
127 126 zred โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) โˆˆ โ„ )
128 1red โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ 1 โˆˆ โ„ )
129 72 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘† โŠ† ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) )
130 129 ssdifssd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠ† ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) )
131 ssfi โŠข ( ( ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆˆ Fin โˆง ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠ† ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ) โ†’ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆˆ Fin )
132 80 130 131 sylancr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆˆ Fin )
133 f1oi โŠข ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) : ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ€“1-1-ontoโ†’ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
134 f1of โŠข ( ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) : ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ€“1-1-ontoโ†’ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) : ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŸถ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
135 133 134 ax-mp โŠข ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) : ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŸถ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
136 120 ssdifssd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠ† โ„ค )
137 fss โŠข ( ( ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) : ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŸถ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆง ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠ† โ„ค ) โ†’ ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) : ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŸถ โ„ค )
138 135 136 137 sylancr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) : ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŸถ โ„ค )
139 138 132 124 fdmfifsupp โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) finSupp 1 )
140 60 66 132 116 138 139 gsumsubmcl โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) โˆˆ โ„ค )
141 50 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ƒ โˆˆ โ„+ )
142 35 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘‡ โˆˆ Mnd )
143 76 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘† โŠ† โ„‚ )
144 143 90 sseldd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ง โˆˆ โ„‚ )
145 id โŠข ( ๐‘ค = ๐‘ง โ†’ ๐‘ค = ๐‘ง )
146 40 145 gsumsn โŠข ( ( ๐‘‡ โˆˆ Mnd โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ ) โ†’ ( ๐‘‡ ฮฃg ( ๐‘ค โˆˆ { ๐‘ง } โ†ฆ ๐‘ค ) ) = ๐‘ง )
147 142 144 144 146 syl3anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘‡ ฮฃg ( ๐‘ค โˆˆ { ๐‘ง } โ†ฆ ๐‘ค ) ) = ๐‘ง )
148 147 adantr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ ( ๐‘‡ ฮฃg ( ๐‘ค โˆˆ { ๐‘ง } โ†ฆ ๐‘ค ) ) = ๐‘ง )
149 mptresid โŠข ( I โ†พ { ๐‘ง } ) = ( ๐‘ค โˆˆ { ๐‘ง } โ†ฆ ๐‘ค )
150 dfsn2 โŠข { ๐‘ง } = { ๐‘ง , ๐‘ง }
151 animorrl โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ ( ๐‘ง = 1 โˆจ ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) ) )
152 3 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ƒ โˆˆ โ„™ )
153 129 90 sseldd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ง โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) )
154 wilthlem1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ง โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ) โ†’ ( ๐‘ง = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†” ( ๐‘ง = 1 โˆจ ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) ) ) )
155 152 153 154 syl2anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ง = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†” ( ๐‘ง = 1 โˆจ ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) ) ) )
156 155 biimpar โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ( ๐‘ง = 1 โˆจ ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) ) ) โ†’ ๐‘ง = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
157 151 156 syldan โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ ๐‘ง = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
158 157 preq2d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ { ๐‘ง , ๐‘ง } = { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
159 150 158 eqtrid โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ { ๐‘ง } = { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
160 159 reseq2d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ ( I โ†พ { ๐‘ง } ) = ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
161 149 160 eqtr3id โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ ( ๐‘ค โˆˆ { ๐‘ง } โ†ฆ ๐‘ค ) = ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
162 161 oveq2d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ ( ๐‘‡ ฮฃg ( ๐‘ค โˆˆ { ๐‘ง } โ†ฆ ๐‘ค ) ) = ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) )
163 simpr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ ๐‘ง = 1 )
164 148 162 163 3eqtr3d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = 1 )
165 164 oveq1d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง = 1 ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) mod ๐‘ƒ ) = ( 1 mod ๐‘ƒ ) )
166 df-pr โŠข { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } = ( { ๐‘ง } โˆช { ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
167 166 reseq2i โŠข ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) = ( I โ†พ ( { ๐‘ง } โˆช { ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
168 mptresid โŠข ( I โ†พ ( { ๐‘ง } โˆช { ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = ( ๐‘ค โˆˆ ( { ๐‘ง } โˆช { ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†ฆ ๐‘ค )
169 167 168 eqtri โŠข ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) = ( ๐‘ค โˆˆ ( { ๐‘ง } โˆช { ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†ฆ ๐‘ค )
170 169 oveq2i โŠข ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = ( ๐‘‡ ฮฃg ( ๐‘ค โˆˆ ( { ๐‘ง } โˆช { ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†ฆ ๐‘ค ) )
171 65 a1i โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ๐‘‡ โˆˆ CMnd )
172 snfi โŠข { ๐‘ง } โˆˆ Fin
173 172 a1i โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ { ๐‘ง } โˆˆ Fin )
174 elsni โŠข ( ๐‘ค โˆˆ { ๐‘ง } โ†’ ๐‘ค = ๐‘ง )
175 174 adantl โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ค โˆˆ { ๐‘ง } ) โ†’ ๐‘ค = ๐‘ง )
176 144 adantr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ค โˆˆ { ๐‘ง } ) โ†’ ๐‘ง โˆˆ โ„‚ )
177 175 176 eqeltrd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ค โˆˆ { ๐‘ง } ) โ†’ ๐‘ค โˆˆ โ„‚ )
178 177 adantlr โŠข ( ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โˆง ๐‘ค โˆˆ { ๐‘ง } ) โ†’ ๐‘ค โˆˆ โ„‚ )
179 143 96 sseldd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ โ„‚ )
180 179 adantr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ โ„‚ )
181 simprr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } )
182 velsn โŠข ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†” ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) )
183 181 182 sylnib โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ยฌ ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) )
184 biorf โŠข ( ยฌ ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) โ†’ ( ๐‘ง = 1 โ†” ( ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) โˆจ ๐‘ง = 1 ) ) )
185 183 184 syl โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ง = 1 โ†” ( ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) โˆจ ๐‘ง = 1 ) ) )
186 ovex โŠข ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ V
187 186 elsn โŠข ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง } โ†” ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ๐‘ง )
188 eqcom โŠข ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ๐‘ง โ†” ๐‘ง = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
189 187 188 bitri โŠข ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง } โ†” ๐‘ง = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
190 orcom โŠข ( ( ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) โˆจ ๐‘ง = 1 ) โ†” ( ๐‘ง = 1 โˆจ ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) ) )
191 155 189 190 3bitr4g โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง } โ†” ( ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) โˆจ ๐‘ง = 1 ) ) )
192 185 191 bitr4d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ง = 1 โ†” ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง } ) )
193 192 necon3abid โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ง โ‰  1 โ†” ยฌ ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง } ) )
194 193 biimpa โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ยฌ ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง } )
195 id โŠข ( ๐‘ค = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†’ ๐‘ค = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
196 40 62 171 173 178 180 194 180 195 gsumunsn โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ( ๐‘‡ ฮฃg ( ๐‘ค โˆˆ ( { ๐‘ง } โˆช { ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†ฆ ๐‘ค ) ) = ( ( ๐‘‡ ฮฃg ( ๐‘ค โˆˆ { ๐‘ง } โ†ฆ ๐‘ค ) ) ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
197 170 196 eqtrid โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = ( ( ๐‘‡ ฮฃg ( ๐‘ค โˆˆ { ๐‘ง } โ†ฆ ๐‘ค ) ) ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
198 147 adantr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ( ๐‘‡ ฮฃg ( ๐‘ค โˆˆ { ๐‘ง } โ†ฆ ๐‘ค ) ) = ๐‘ง )
199 198 oveq1d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ( ( ๐‘‡ ฮฃg ( ๐‘ค โˆˆ { ๐‘ง } โ†ฆ ๐‘ค ) ) ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) = ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
200 197 199 eqtrd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) = ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
201 200 oveq1d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) mod ๐‘ƒ ) = ( ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) )
202 153 elfzelzd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ง โˆˆ โ„ค )
203 24 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ƒ โˆˆ โ„• )
204 fzm1ndvds โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐‘ง โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ๐‘ง )
205 203 153 204 syl2anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ๐‘ง )
206 eqid โŠข ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ )
207 206 prmdiv โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ง โˆˆ โ„ค โˆง ยฌ ๐‘ƒ โˆฅ ๐‘ง ) โ†’ ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ๐‘ƒ โˆฅ ( ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โˆ’ 1 ) ) )
208 152 202 205 207 syl3anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ๐‘ƒ โˆฅ ( ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โˆ’ 1 ) ) )
209 208 simprd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ƒ โˆฅ ( ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โˆ’ 1 ) )
210 elfznn โŠข ( ๐‘ง โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ๐‘ง โˆˆ โ„• )
211 153 210 syl โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ง โˆˆ โ„• )
212 129 96 sseldd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) )
213 elfznn โŠข ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ โ„• )
214 212 213 syl โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ โ„• )
215 211 214 nnmulcld โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โˆˆ โ„• )
216 215 nnzd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โˆˆ โ„ค )
217 1zzd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ 1 โˆˆ โ„ค )
218 moddvds โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค ) โ†’ ( ( ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( 1 mod ๐‘ƒ ) โ†” ๐‘ƒ โˆฅ ( ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โˆ’ 1 ) ) )
219 203 216 217 218 syl3anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( 1 mod ๐‘ƒ ) โ†” ๐‘ƒ โˆฅ ( ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โˆ’ 1 ) ) )
220 209 219 mpbird โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( 1 mod ๐‘ƒ ) )
221 220 adantr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ( ( ๐‘ง ยท ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( 1 mod ๐‘ƒ ) )
222 201 221 eqtrd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ง โ‰  1 ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) mod ๐‘ƒ ) = ( 1 mod ๐‘ƒ ) )
223 165 222 pm2.61dane โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) mod ๐‘ƒ ) = ( 1 mod ๐‘ƒ ) )
224 modmul1 โŠข ( ( ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) โˆˆ โ„ โˆง 1 โˆˆ โ„ ) โˆง ( ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„+ ) โˆง ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) mod ๐‘ƒ ) = ( 1 mod ๐‘ƒ ) ) โ†’ ( ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ยท ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) mod ๐‘ƒ ) = ( ( 1 ยท ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) mod ๐‘ƒ ) )
225 127 128 140 141 223 224 syl221anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ( ๐‘‡ ฮฃg ( I โ†พ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ยท ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) mod ๐‘ƒ ) = ( ( 1 ยท ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) mod ๐‘ƒ ) )
226 140 zcnd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) โˆˆ โ„‚ )
227 226 mullidd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( 1 ยท ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) = ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) )
228 227 oveq1d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( 1 ยท ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) mod ๐‘ƒ ) = ( ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) mod ๐‘ƒ ) )
229 sseqin2 โŠข ( { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โŠ† ๐‘† โ†” ( ๐‘† โˆฉ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) = { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
230 97 229 sylib โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘† โˆฉ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) = { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
231 vex โŠข ๐‘ง โˆˆ V
232 231 prnz โŠข { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ‰  โˆ…
233 232 a1i โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ‰  โˆ… )
234 230 233 eqnetrd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘† โˆฉ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ‰  โˆ… )
235 disj4 โŠข ( ( ๐‘† โˆฉ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) = โˆ… โ†” ยฌ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠŠ ๐‘† )
236 235 necon2abii โŠข ( ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠŠ ๐‘† โ†” ( ๐‘† โˆฉ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ‰  โˆ… )
237 234 236 sylibr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠŠ ๐‘† )
238 psseq1 โŠข ( ๐‘  = ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( ๐‘  โŠŠ ๐‘† โ†” ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠŠ ๐‘† ) )
239 reseq2 โŠข ( ๐‘  = ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( I โ†พ ๐‘  ) = ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) )
240 239 oveq2d โŠข ( ๐‘  = ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( ๐‘‡ ฮฃg ( I โ†พ ๐‘  ) ) = ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) )
241 240 oveq1d โŠข ( ๐‘  = ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘  ) ) mod ๐‘ƒ ) = ( ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) mod ๐‘ƒ ) )
242 241 eqeq1d โŠข ( ๐‘  = ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘  ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) โ†” ( ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
243 238 242 imbi12d โŠข ( ๐‘  = ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( ( ๐‘  โŠŠ ๐‘† โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘  ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) โ†” ( ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠŠ ๐‘† โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) ) )
244 5 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ โˆ€ ๐‘  โˆˆ ๐ด ( ๐‘  โŠŠ ๐‘† โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘  ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
245 ovex โŠข ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆˆ V
246 245 elpw2 โŠข ( ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆˆ ๐’ซ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โ†” ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠ† ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) )
247 130 246 sylibr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆˆ ๐’ซ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) )
248 14 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘† )
249 eqcom โŠข ( ๐‘ง = ( ๐‘ƒ โˆ’ 1 ) โ†” ( ๐‘ƒ โˆ’ 1 ) = ๐‘ง )
250 182 249 bitri โŠข ( ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } โ†” ( ๐‘ƒ โˆ’ 1 ) = ๐‘ง )
251 181 250 sylnib โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ยฌ ( ๐‘ƒ โˆ’ 1 ) = ๐‘ง )
252 oveq1 โŠข ( ( ๐‘ƒ โˆ’ 1 ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) = ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) )
253 252 oveq1d โŠข ( ( ๐‘ƒ โˆ’ 1 ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
254 203 36 syl โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„•0 )
255 nn0uz โŠข โ„•0 = ( โ„คโ‰ฅ โ€˜ 0 )
256 254 255 eleqtrdi โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 0 ) )
257 eluzfz2 โŠข ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ 0 ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( 0 ... ( ๐‘ƒ โˆ’ 1 ) ) )
258 256 257 syl โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( 0 ... ( ๐‘ƒ โˆ’ 1 ) ) )
259 prmz โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค )
260 152 259 syl โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ƒ โˆˆ โ„ค )
261 120 248 sseldd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„ค )
262 1z โŠข 1 โˆˆ โ„ค
263 zsubcl โŠข ( ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) โˆˆ โ„ค )
264 261 262 263 sylancl โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) โˆˆ โ„ค )
265 dvdsmul1 โŠข ( ( ๐‘ƒ โˆˆ โ„ค โˆง ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) โˆˆ โ„ค ) โ†’ ๐‘ƒ โˆฅ ( ๐‘ƒ ยท ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) ) )
266 260 264 265 syl2anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ƒ โˆฅ ( ๐‘ƒ ยท ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) ) )
267 203 nncnd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ƒ โˆˆ โ„‚ )
268 264 zcnd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) โˆˆ โ„‚ )
269 267 268 mulcld โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ ยท ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) ) โˆˆ โ„‚ )
270 1cnd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ 1 โˆˆ โ„‚ )
271 254 nn0cnd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„‚ )
272 267 270 271 subdird โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) ยท ( ๐‘ƒ โˆ’ 1 ) ) = ( ( ๐‘ƒ ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ ( 1 ยท ( ๐‘ƒ โˆ’ 1 ) ) ) )
273 267 271 mulcld โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆˆ โ„‚ )
274 273 267 270 subsubd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ ( ๐‘ƒ โˆ’ 1 ) ) = ( ( ( ๐‘ƒ ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ ๐‘ƒ ) + 1 ) )
275 271 mullidd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( 1 ยท ( ๐‘ƒ โˆ’ 1 ) ) = ( ๐‘ƒ โˆ’ 1 ) )
276 275 oveq2d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ ( 1 ยท ( ๐‘ƒ โˆ’ 1 ) ) ) = ( ( ๐‘ƒ ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ ( ๐‘ƒ โˆ’ 1 ) ) )
277 267 271 muls1d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ ยท ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) ) = ( ( ๐‘ƒ ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ ๐‘ƒ ) )
278 277 oveq1d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ ยท ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) ) + 1 ) = ( ( ( ๐‘ƒ ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ ๐‘ƒ ) + 1 ) )
279 274 276 278 3eqtr4d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ ( 1 ยท ( ๐‘ƒ โˆ’ 1 ) ) ) = ( ( ๐‘ƒ ยท ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) ) + 1 ) )
280 272 279 eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) ยท ( ๐‘ƒ โˆ’ 1 ) ) = ( ( ๐‘ƒ ยท ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) ) + 1 ) )
281 269 270 280 mvrraddd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ 1 ) = ( ๐‘ƒ ยท ( ( ๐‘ƒ โˆ’ 1 ) โˆ’ 1 ) ) )
282 266 281 breqtrrd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ƒ โˆฅ ( ( ( ๐‘ƒ โˆ’ 1 ) ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ 1 ) )
283 129 248 sseldd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) )
284 fzm1ndvds โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ƒ โˆ’ 1 ) )
285 203 283 284 syl2anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ƒ โˆ’ 1 ) )
286 eqid โŠข ( ( ( ๐‘ƒ โˆ’ 1 ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ( ๐‘ƒ โˆ’ 1 ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ )
287 286 prmdiveq โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„ค โˆง ยฌ ๐‘ƒ โˆฅ ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( 0 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ๐‘ƒ โˆฅ ( ( ( ๐‘ƒ โˆ’ 1 ) ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ 1 ) ) โ†” ( ๐‘ƒ โˆ’ 1 ) = ( ( ( ๐‘ƒ โˆ’ 1 ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
288 152 261 285 287 syl3anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( 0 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ๐‘ƒ โˆฅ ( ( ( ๐‘ƒ โˆ’ 1 ) ยท ( ๐‘ƒ โˆ’ 1 ) ) โˆ’ 1 ) ) โ†” ( ๐‘ƒ โˆ’ 1 ) = ( ( ( ๐‘ƒ โˆ’ 1 ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
289 258 282 288 mpbi2and โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ โˆ’ 1 ) = ( ( ( ๐‘ƒ โˆ’ 1 ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
290 206 prmdivdiv โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ง โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ) โ†’ ๐‘ง = ( ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
291 152 153 290 syl2anc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ๐‘ง = ( ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
292 289 291 eqeq12d โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) = ๐‘ง โ†” ( ( ( ๐‘ƒ โˆ’ 1 ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
293 253 292 imbitrrid โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†’ ( ๐‘ƒ โˆ’ 1 ) = ๐‘ง ) )
294 251 293 mtod โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ยฌ ( ๐‘ƒ โˆ’ 1 ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
295 ioran โŠข ( ยฌ ( ( ๐‘ƒ โˆ’ 1 ) = ๐‘ง โˆจ ( ๐‘ƒ โˆ’ 1 ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โ†” ( ยฌ ( ๐‘ƒ โˆ’ 1 ) = ๐‘ง โˆง ยฌ ( ๐‘ƒ โˆ’ 1 ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
296 251 294 295 sylanbrc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ยฌ ( ( ๐‘ƒ โˆ’ 1 ) = ๐‘ง โˆจ ( ๐‘ƒ โˆ’ 1 ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
297 ovex โŠข ( ๐‘ƒ โˆ’ 1 ) โˆˆ V
298 297 elpr โŠข ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ†” ( ( ๐‘ƒ โˆ’ 1 ) = ๐‘ง โˆจ ( ๐‘ƒ โˆ’ 1 ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
299 296 298 sylnibr โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ยฌ ( ๐‘ƒ โˆ’ 1 ) โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
300 248 299 eldifd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
301 eldifi โŠข ( ๐‘ฆ โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ๐‘ฆ โˆˆ ๐‘† )
302 95 r19.21bi โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† )
303 301 302 sylan2 โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) โ†’ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘† )
304 eldif โŠข ( ๐‘ฆ โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†” ( ๐‘ฆ โˆˆ ๐‘† โˆง ยฌ ๐‘ฆ โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
305 152 adantr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ๐‘ƒ โˆˆ โ„™ )
306 129 sselda โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ๐‘ฆ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) )
307 eqid โŠข ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ )
308 307 prmdivdiv โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ฆ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ) โ†’ ๐‘ฆ = ( ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
309 305 306 308 syl2anc โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ๐‘ฆ = ( ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
310 oveq1 โŠข ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ๐‘ง โ†’ ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) = ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) )
311 310 oveq1d โŠข ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ๐‘ง โ†’ ( ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
312 311 eqeq2d โŠข ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ๐‘ง โ†’ ( ๐‘ฆ = ( ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†” ๐‘ฆ = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
313 309 312 syl5ibcom โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ๐‘ง โ†’ ๐‘ฆ = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
314 oveq1 โŠข ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†’ ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) = ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) )
315 314 oveq1d โŠข ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†’ ( ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
316 291 adantr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ๐‘ง = ( ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) )
317 309 316 eqeq12d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ( ๐‘ฆ = ๐‘ง โ†” ( ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
318 315 317 imbitrrid โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โ†’ ๐‘ฆ = ๐‘ง ) )
319 313 318 orim12d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ( ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ๐‘ง โˆจ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โ†’ ( ๐‘ฆ = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆจ ๐‘ฆ = ๐‘ง ) ) )
320 ovex โŠข ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ V
321 320 elpr โŠข ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ†” ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ๐‘ง โˆจ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
322 vex โŠข ๐‘ฆ โˆˆ V
323 322 elpr โŠข ( ๐‘ฆ โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ†” ( ๐‘ฆ = ๐‘ง โˆจ ๐‘ฆ = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) )
324 orcom โŠข ( ( ๐‘ฆ = ๐‘ง โˆจ ๐‘ฆ = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) ) โ†” ( ๐‘ฆ = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆจ ๐‘ฆ = ๐‘ง ) )
325 323 324 bitri โŠข ( ๐‘ฆ โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ†” ( ๐‘ฆ = ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆจ ๐‘ฆ = ๐‘ง ) )
326 319 321 325 3imtr4g โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ†’ ๐‘ฆ โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
327 326 con3d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ( ยฌ ๐‘ฆ โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } โ†’ ยฌ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
328 327 impr โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ( ๐‘ฆ โˆˆ ๐‘† โˆง ยฌ ๐‘ฆ โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) โ†’ ยฌ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
329 304 328 sylan2b โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) โ†’ ยฌ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } )
330 303 329 eldifd โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โˆง ๐‘ฆ โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) โ†’ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
331 330 ralrimiva โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ โˆ€ ๐‘ฆ โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) )
332 300 331 jca โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆง โˆ€ ๐‘ฆ โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) )
333 eleq2 โŠข ( ๐‘ฅ = ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘ฅ โ†” ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) )
334 eleq2 โŠข ( ๐‘ฅ = ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘ฅ โ†” ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) )
335 334 raleqbi1dv โŠข ( ๐‘ฅ = ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( โˆ€ ๐‘ฆ โˆˆ ๐‘ฅ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘ฅ โ†” โˆ€ ๐‘ฆ โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) )
336 333 335 anbi12d โŠข ( ๐‘ฅ = ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โ†’ ( ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ๐‘ฅ โˆง โˆ€ ๐‘ฆ โˆˆ ๐‘ฅ ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ๐‘ฅ ) โ†” ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆง โˆ€ ๐‘ฆ โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) )
337 336 2 elrab2 โŠข ( ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆˆ ๐ด โ†” ( ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆˆ ๐’ซ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ƒ โˆ’ 1 ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆง โˆ€ ๐‘ฆ โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ( ( ๐‘ฆ โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) โˆˆ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) )
338 247 332 337 sylanbrc โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โˆˆ ๐ด )
339 243 244 338 rspcdva โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) โŠŠ ๐‘† โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
340 237 339 mpd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
341 228 340 eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( 1 ยท ( ๐‘‡ ฮฃg ( I โ†พ ( ๐‘† โˆ– { ๐‘ง , ( ( ๐‘ง โ†‘ ( ๐‘ƒ โˆ’ 2 ) ) mod ๐‘ƒ ) } ) ) ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
342 111 225 341 3eqtrd โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )
343 342 ex โŠข ( ๐œ‘ โ†’ ( ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
344 343 exlimdv โŠข ( ๐œ‘ โ†’ ( โˆƒ ๐‘ง ( ๐‘ง โˆˆ ๐‘† โˆง ยฌ ๐‘ง โˆˆ { ( ๐‘ƒ โˆ’ 1 ) } ) โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
345 58 344 biimtrid โŠข ( ๐œ‘ โ†’ ( ยฌ ๐‘† โŠ† { ( ๐‘ƒ โˆ’ 1 ) } โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) ) )
346 57 345 pm2.61d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ ฮฃg ( I โ†พ ๐‘† ) ) mod ๐‘ƒ ) = ( - 1 mod ๐‘ƒ ) )