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

Metamath Proof Explorer

Theorem dihcnvid1

Description: The converse isomorphism of an isomorphism. (Contributed by NM, 5-Aug-2014)

Ref Expression
Hypotheses dihcnvid1.b ⊢ B = Base K
dihcnvid1.h ⊢ H = LHyp ⁡ K
dihcnvid1.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihcnvid1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I -1 ⁡ I ⁡ X = X

Proof

Step Hyp Ref Expression
1 dihcnvid1.b ⊢ B = Base K
2 dihcnvid1.h ⊢ H = LHyp ⁡ K
3 dihcnvid1.i ⊢ I = DIsoH ⁡ K ⁡ W
4 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
5 eqid ⊢ LSubSp ⁡ DVecH ⁡ K ⁡ W = LSubSp ⁡ DVecH ⁡ K ⁡ W
6 1 2 3 4 5 dihf11 ⊢ K ∈ HL ∧ W ∈ H → I : B ⟶ 1-1 LSubSp ⁡ DVecH ⁡ K ⁡ W
7 f1f1orn ⊢ I : B ⟶ 1-1 LSubSp ⁡ DVecH ⁡ K ⁡ W → I : B ⟶ 1-1 onto ran ⁡ I
8 6 7 syl ⊢ K ∈ HL ∧ W ∈ H → I : B ⟶ 1-1 onto ran ⁡ I
9 f1ocnvfv1 ⊢ I : B ⟶ 1-1 onto ran ⁡ I ∧ X ∈ B → I -1 ⁡ I ⁡ X = X
10 8 9 sylan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I -1 ⁡ I ⁡ X = X