Metamath Proof Explorer


Theorem znleval

Description: The ordering of the Z/nZ structure. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses znle2.y Y = /N
znle2.f F = ℤRHom Y W
znle2.w W = if N = 0 0 ..^ N
znle2.l ˙ = Y
znleval.x X = Base Y
Assertion znleval N 0 A ˙ B A X B X F -1 A F -1 B

Proof

Step Hyp Ref Expression
1 znle2.y Y = /N
2 znle2.f F = ℤRHom Y W
3 znle2.w W = if N = 0 0 ..^ N
4 znle2.l ˙ = Y
5 znleval.x X = Base Y
6 1 2 3 4 znle2 N 0 ˙ = F F -1
7 relco Rel F F -1
8 relssdmrn Rel F F -1 F F -1 dom F F -1 × ran F F -1
9 7 8 ax-mp F F -1 dom F F -1 × ran F F -1
10 dmcoss dom F F -1 dom F -1
11 df-rn ran F = dom F -1
12 1 5 2 3 znf1o N 0 F : W 1-1 onto X
13 f1ofo F : W 1-1 onto X F : W onto X
14 forn F : W onto X ran F = X
15 12 13 14 3syl N 0 ran F = X
16 11 15 eqtr3id N 0 dom F -1 = X
17 10 16 sseqtrid N 0 dom F F -1 X
18 rncoss ran F F -1 ran F
19 rncoss ran F ran F
20 19 15 sseqtrid N 0 ran F X
21 18 20 sstrid N 0 ran F F -1 X
22 xpss12 dom F F -1 X ran F F -1 X dom F F -1 × ran F F -1 X × X
23 17 21 22 syl2anc N 0 dom F F -1 × ran F F -1 X × X
24 9 23 sstrid N 0 F F -1 X × X
25 6 24 eqsstrd N 0 ˙ X × X
26 25 ssbrd N 0 A ˙ B A X × X B
27 brxp A X × X B A X B X
28 26 27 syl6ib N 0 A ˙ B A X B X
29 28 pm4.71rd N 0 A ˙ B A X B X A ˙ B
30 6 adantr N 0 A X B X ˙ = F F -1
31 30 breqd N 0 A X B X A ˙ B A F F -1 B
32 brcog A X B X A F F -1 B x A F -1 x x F B
33 32 adantl N 0 A X B X A F F -1 B x A F -1 x x F B
34 eqcom x = F -1 A F -1 A = x
35 12 adantr N 0 A X B X F : W 1-1 onto X
36 f1ocnv F : W 1-1 onto X F -1 : X 1-1 onto W
37 f1ofn F -1 : X 1-1 onto W F -1 Fn X
38 35 36 37 3syl N 0 A X B X F -1 Fn X
39 simprl N 0 A X B X A X
40 fnbrfvb F -1 Fn X A X F -1 A = x A F -1 x
41 38 39 40 syl2anc N 0 A X B X F -1 A = x A F -1 x
42 34 41 bitr2id N 0 A X B X A F -1 x x = F -1 A
43 42 anbi1d N 0 A X B X A F -1 x x F B x = F -1 A x F B
44 43 exbidv N 0 A X B X x A F -1 x x F B x x = F -1 A x F B
45 33 44 bitrd N 0 A X B X A F F -1 B x x = F -1 A x F B
46 fvex F -1 A V
47 breq1 x = F -1 A x F B F -1 A F B
48 46 47 ceqsexv x x = F -1 A x F B F -1 A F B
49 simprr N 0 A X B X B X
50 brcog F -1 A V B X F -1 A F B x F -1 A x x F B
51 46 49 50 sylancr N 0 A X B X F -1 A F B x F -1 A x x F B
52 fvex F -1 B V
53 breq2 x = F -1 B F -1 A x F -1 A F -1 B
54 52 53 ceqsexv x x = F -1 B F -1 A x F -1 A F -1 B
55 eqcom x = F -1 B F -1 B = x
56 fnbrfvb F -1 Fn X B X F -1 B = x B F -1 x
57 38 49 56 syl2anc N 0 A X B X F -1 B = x B F -1 x
58 55 57 syl5bb N 0 A X B X x = F -1 B B F -1 x
59 vex x V
60 brcnvg B X x V B F -1 x x F B
61 49 59 60 sylancl N 0 A X B X B F -1 x x F B
62 58 61 bitrd N 0 A X B X x = F -1 B x F B
63 62 anbi1d N 0 A X B X x = F -1 B F -1 A x x F B F -1 A x
64 63 biancomd N 0 A X B X x = F -1 B F -1 A x F -1 A x x F B
65 64 exbidv N 0 A X B X x x = F -1 B F -1 A x x F -1 A x x F B
66 54 65 bitr3id N 0 A X B X F -1 A F -1 B x F -1 A x x F B
67 51 66 bitr4d N 0 A X B X F -1 A F B F -1 A F -1 B
68 48 67 syl5bb N 0 A X B X x x = F -1 A x F B F -1 A F -1 B
69 31 45 68 3bitrd N 0 A X B X A ˙ B F -1 A F -1 B
70 69 pm5.32da N 0 A X B X A ˙ B A X B X F -1 A F -1 B
71 df-3an A X B X F -1 A F -1 B A X B X F -1 A F -1 B
72 70 71 bitr4di N 0 A X B X A ˙ B A X B X F -1 A F -1 B
73 29 72 bitrd N 0 A ˙ B A X B X F -1 A F -1 B