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