Metamath Proof Explorer


Theorem metakunt14

Description: A is a primitive permutation that moves the I-th element to the end and C is its inverse that moves the last element back to the I-th position. (Contributed by metakunt, 25-May-2024)

Ref Expression
Hypotheses metakunt14.1 φ M
metakunt14.2 φ I
metakunt14.3 φ I M
metakunt14.4 A = x 1 M if x = I M if x < I x x 1
metakunt14.5 C = y 1 M if y = M I if y < I y y + 1
Assertion metakunt14 φ A : 1 M 1-1 onto 1 M A -1 = C

Proof

Step Hyp Ref Expression
1 metakunt14.1 φ M
2 metakunt14.2 φ I
3 metakunt14.3 φ I M
4 metakunt14.4 A = x 1 M if x = I M if x < I x x 1
5 metakunt14.5 C = y 1 M if y = M I if y < I y y + 1
6 1 2 3 4 metakunt1 φ A : 1 M 1 M
7 1 2 3 5 metakunt2 φ C : 1 M 1 M
8 1 adantr φ a 1 M M
9 2 adantr φ a 1 M I
10 3 adantr φ a 1 M I M
11 simpr φ a 1 M a 1 M
12 8 9 10 4 5 11 metakunt9 φ a 1 M C A a = a
13 12 ralrimiva φ a 1 M C A a = a
14 1 adantr φ b 1 M M
15 2 adantr φ b 1 M I
16 3 adantr φ b 1 M I M
17 simpr φ b 1 M b 1 M
18 14 15 16 4 5 17 metakunt13 φ b 1 M A C b = b
19 18 ralrimiva φ b 1 M A C b = b
20 6 7 13 19 2fvidf1od φ A : 1 M 1-1 onto 1 M
21 6 7 13 19 2fvidinvd φ A -1 = C
22 20 21 jca φ A : 1 M 1-1 onto 1 M A -1 = C