Metamath Proof Explorer

Theorem dihcnv11

Description: The converse of isomorphism H is one-to-one. (Contributed by NM, 17-Aug-2014)

Ref Expression
Hypotheses dihcnv11.h ⊢ H = LHyp ⁡ K
dihcnv11.i ⊢ I = DIsoH ⁡ K ⁡ W
dihcnv11.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihcnv11.x ⊢ φ → X ∈ ran ⁡ I
dihcnv11.y ⊢ φ → Y ∈ ran ⁡ I
Assertion dihcnv11 ⊢ φ → I -1 ⁡ X = I -1 ⁡ Y ↔ X = Y

Proof

Step Hyp Ref Expression
1 dihcnv11.h ⊢ H = LHyp ⁡ K
2 dihcnv11.i ⊢ I = DIsoH ⁡ K ⁡ W
3 dihcnv11.k ⊢ φ → K ∈ HL ∧ W ∈ H
4 dihcnv11.x ⊢ φ → X ∈ ran ⁡ I
5 dihcnv11.y ⊢ φ → Y ∈ ran ⁡ I
6 eqid ⊢ Base K = Base K
7 6 1 2 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ Base K
8 3 4 7 syl2anc ⊢ φ → I -1 ⁡ X ∈ Base K
9 6 1 2 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → I -1 ⁡ Y ∈ Base K
10 3 5 9 syl2anc ⊢ φ → I -1 ⁡ Y ∈ Base K
11 6 1 2 dih11 ⊢ K ∈ HL ∧ W ∈ H ∧ I -1 ⁡ X ∈ Base K ∧ I -1 ⁡ Y ∈ Base K → I ⁡ I -1 ⁡ X = I ⁡ I -1 ⁡ Y ↔ I -1 ⁡ X = I -1 ⁡ Y
12 3 8 10 11 syl3anc ⊢ φ → I ⁡ I -1 ⁡ X = I ⁡ I -1 ⁡ Y ↔ I -1 ⁡ X = I -1 ⁡ Y
13 1 2 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I ⁡ I -1 ⁡ X = X
14 3 4 13 syl2anc ⊢ φ → I ⁡ I -1 ⁡ X = X
15 1 2 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ Y = Y
16 3 5 15 syl2anc ⊢ φ → I ⁡ I -1 ⁡ Y = Y
17 14 16 eqeq12d ⊢ φ → I ⁡ I -1 ⁡ X = I ⁡ I -1 ⁡ Y ↔ X = Y
18 12 17 bitr3d ⊢ φ → I -1 ⁡ X = I -1 ⁡ Y ↔ X = Y