This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
Assertion efgmnvl ( 𝐴 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 efgmval.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
2 elxp2 ⊢ ( 𝐴 ∈ ( 𝐼 × 2o ) ↔ ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 2o 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ )
3 1 efgmval ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑎 𝑀 𝑏 ) = ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ )
4 3 fveq2d ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑀 ‘ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ) )
5 df-ov ⊢ ( 𝑎 𝑀 ( 1o ∖ 𝑏 ) ) = ( 𝑀 ‘ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ )
6 4 5 eqtr4di ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑎 𝑀 ( 1o ∖ 𝑏 ) ) )
7 2oconcl ⊢ ( 𝑏 ∈ 2o → ( 1o ∖ 𝑏 ) ∈ 2o )
8 1 efgmval ⊢ ( ( 𝑎 ∈ 𝐼 ∧ ( 1o ∖ 𝑏 ) ∈ 2o ) → ( 𝑎 𝑀 ( 1o ∖ 𝑏 ) ) = ⟨ 𝑎 , ( 1o ∖ ( 1o ∖ 𝑏 ) ) ⟩ )
9 7 8 sylan2 ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑎 𝑀 ( 1o ∖ 𝑏 ) ) = ⟨ 𝑎 , ( 1o ∖ ( 1o ∖ 𝑏 ) ) ⟩ )
10 1on ⊢ 1o ∈ On
11 10 onordi ⊢ Ord 1o
12 ordtr ⊢ ( Ord 1o → Tr 1o )
13 trsucss ⊢ ( Tr 1o → ( 𝑏 ∈ suc 1o → 𝑏 ⊆ 1o ) )
14 11 12 13 mp2b ⊢ ( 𝑏 ∈ suc 1o → 𝑏 ⊆ 1o )
15 df-2o ⊢ 2o = suc 1o
16 14 15 eleq2s ⊢ ( 𝑏 ∈ 2o → 𝑏 ⊆ 1o )
17 16 adantl ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → 𝑏 ⊆ 1o )
18 dfss4 ⊢ ( 𝑏 ⊆ 1o ↔ ( 1o ∖ ( 1o ∖ 𝑏 ) ) = 𝑏 )
19 17 18 sylib ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 1o ∖ ( 1o ∖ 𝑏 ) ) = 𝑏 )
20 19 opeq2d ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ⟨ 𝑎 , ( 1o ∖ ( 1o ∖ 𝑏 ) ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
21 6 9 20 3eqtrd ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = ⟨ 𝑎 , 𝑏 ⟩ )
22 fveq2 ⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
23 df-ov ⊢ ( 𝑎 𝑀 𝑏 ) = ( 𝑀 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
24 22 23 eqtr4di ⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ 𝐴 ) = ( 𝑎 𝑀 𝑏 ) )
25 24 fveq2d ⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) )
26 id ⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ )
27 25 26 eqeq12d ⊢ ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ↔ ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = ⟨ 𝑎 , 𝑏 ⟩ ) )
28 21 27 syl5ibrcom ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) )
29 28 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 2o 𝐴 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 )
30 2 29 sylbi ⊢ ( 𝐴 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 )