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

Metamath Proof Explorer

Theorem pmtrfcnv

Description: A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
pmtrrn.r ⊢ 𝑅 = ran 𝑇
Assertion pmtrfcnv ( 𝐹 ∈ 𝑅 → ◡ 𝐹 = 𝐹 )

Proof

Step Hyp Ref Expression
1 pmtrrn.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 pmtrrn.r ⊢ 𝑅 = ran 𝑇
3 eqid ⊢ dom ( 𝐹 ∖ I ) = dom ( 𝐹 ∖ I )
4 1 2 3 pmtrfrn ⊢ ( 𝐹 ∈ 𝑅 → ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ) )
5 4 simpld ⊢ ( 𝐹 ∈ 𝑅 → ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) )
6 1 pmtrf ⊢ ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷 ⟶ 𝐷 )
7 5 6 syl ⊢ ( 𝐹 ∈ 𝑅 → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷 ⟶ 𝐷 )
8 4 simprd ⊢ ( 𝐹 ∈ 𝑅 → 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) )
9 8 feq1d ⊢ ( 𝐹 ∈ 𝑅 → ( 𝐹 : 𝐷 ⟶ 𝐷 ↔ ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷 ⟶ 𝐷 ) )
10 7 9 mpbird ⊢ ( 𝐹 ∈ 𝑅 → 𝐹 : 𝐷 ⟶ 𝐷 )
11 1 2 pmtrfinv ⊢ ( 𝐹 ∈ 𝑅 → ( 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐷 ) )
12 10 10 11 11 2fcoidinvd ⊢ ( 𝐹 ∈ 𝑅 → ◡ 𝐹 = 𝐹 )