Theorem dihcnv11

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

	Ref	Expression
Hypotheses	dihcnv11.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihcnv11.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihcnv11.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dihcnv11.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
	dihcnv11.y	⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
Assertion	dihcnv11	⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) = ( ◡ 𝐼 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		dihcnv11.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dihcnv11.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3		dihcnv11.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
4		dihcnv11.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
5		dihcnv11.y	⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
6		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7	6 1 2	dihcnvcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
8	3 4 7	syl2anc	⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
9	6 1 2	dihcnvcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
10	3 5 9	syl2anc	⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
11	6 1 2	dih11	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ↔ ( ◡ 𝐼 ‘ 𝑋 ) = ( ◡ 𝐼 ‘ 𝑌 ) ) )
12	3 8 10 11	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ↔ ( ◡ 𝐼 ‘ 𝑋 ) = ( ◡ 𝐼 ‘ 𝑌 ) ) )
13	1 2	dihcnvid2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
14	3 4 13	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
15	1 2	dihcnvid2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) = 𝑌 )
16	3 5 15	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) = 𝑌 )
17	14 16	eqeq12d	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ↔ 𝑋 = 𝑌 ) )
18	12 17	bitr3d	⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) = ( ◡ 𝐼 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )