Metamath Proof Explorer

Theorem dihcnvid2

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

Ref Expression
Hypotheses dihcnvid2.h ⊢ H = LHyp ⁡ K
dihcnvid2.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I ⁡ I -1 ⁡ X = X

Proof

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