Metamath Proof Explorer


Theorem dihcnvid1

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

Ref Expression
Hypotheses dihcnvid1.b 𝐵 = ( Base ‘ 𝐾 )
dihcnvid1.h 𝐻 = ( LHyp ‘ 𝐾 )
dihcnvid1.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihcnvid1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ) → ( 𝐼 ‘ ( 𝐼𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 dihcnvid1.b 𝐵 = ( Base ‘ 𝐾 )
2 dihcnvid1.h 𝐻 = ( LHyp ‘ 𝐾 )
3 dihcnvid1.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
6 1 2 3 4 5 dihf11 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐼 : 𝐵1-1→ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
7 f1f1orn ( 𝐼 : 𝐵1-1→ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝐼 : 𝐵1-1-onto→ ran 𝐼 )
8 6 7 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐼 : 𝐵1-1-onto→ ran 𝐼 )
9 f1ocnvfv1 ( ( 𝐼 : 𝐵1-1-onto→ ran 𝐼𝑋𝐵 ) → ( 𝐼 ‘ ( 𝐼𝑋 ) ) = 𝑋 )
10 8 9 sylan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵 ) → ( 𝐼 ‘ ( 𝐼𝑋 ) ) = 𝑋 )