Metamath Proof Explorer


Theorem efgmnvl

Description: The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypothesis efgmval.m M = y I , z 2 𝑜 y 1 𝑜 z
Assertion efgmnvl A I × 2 𝑜 M M A = A

Proof

Step Hyp Ref Expression
1 efgmval.m M = y I , z 2 𝑜 y 1 𝑜 z
2 elxp2 A I × 2 𝑜 a I b 2 𝑜 A = a b
3 1 efgmval a I b 2 𝑜 a M b = a 1 𝑜 b
4 3 fveq2d a I b 2 𝑜 M a M b = M a 1 𝑜 b
5 df-ov a M 1 𝑜 b = M a 1 𝑜 b
6 4 5 eqtr4di a I b 2 𝑜 M a M b = a M 1 𝑜 b
7 2oconcl b 2 𝑜 1 𝑜 b 2 𝑜
8 1 efgmval a I 1 𝑜 b 2 𝑜 a M 1 𝑜 b = a 1 𝑜 1 𝑜 b
9 7 8 sylan2 a I b 2 𝑜 a M 1 𝑜 b = a 1 𝑜 1 𝑜 b
10 1on 1 𝑜 On
11 10 onordi Ord 1 𝑜
12 ordtr Ord 1 𝑜 Tr 1 𝑜
13 trsucss Tr 1 𝑜 b suc 1 𝑜 b 1 𝑜
14 11 12 13 mp2b b suc 1 𝑜 b 1 𝑜
15 df-2o 2 𝑜 = suc 1 𝑜
16 14 15 eleq2s b 2 𝑜 b 1 𝑜
17 16 adantl a I b 2 𝑜 b 1 𝑜
18 dfss4 b 1 𝑜 1 𝑜 1 𝑜 b = b
19 17 18 sylib a I b 2 𝑜 1 𝑜 1 𝑜 b = b
20 19 opeq2d a I b 2 𝑜 a 1 𝑜 1 𝑜 b = a b
21 6 9 20 3eqtrd a I b 2 𝑜 M a M b = a b
22 fveq2 A = a b M A = M a b
23 df-ov a M b = M a b
24 22 23 eqtr4di A = a b M A = a M b
25 24 fveq2d A = a b M M A = M a M b
26 id A = a b A = a b
27 25 26 eqeq12d A = a b M M A = A M a M b = a b
28 21 27 syl5ibrcom a I b 2 𝑜 A = a b M M A = A
29 28 rexlimivv a I b 2 𝑜 A = a b M M A = A
30 2 29 sylbi A I × 2 𝑜 M M A = A