Metamath Proof Explorer


Theorem dih11

Description: The isomorphism H is one-to-one. Part of proof after Lemma N of Crawley p. 122 line 6. (Contributed by NM, 7-Mar-2014)

Ref Expression
Hypotheses dih11.b B = Base K
dih11.h H = LHyp K
dih11.i I = DIsoH K W
Assertion dih11 K HL W H X B Y B I X = I Y X = Y

Proof

Step Hyp Ref Expression
1 dih11.b B = Base K
2 dih11.h H = LHyp K
3 dih11.i I = DIsoH K W
4 eqss I X = I Y I X I Y I Y I X
5 eqid K = K
6 1 5 2 3 dihord K HL W H X B Y B I X I Y X K Y
7 1 5 2 3 dihord K HL W H Y B X B I Y I X Y K X
8 7 3com23 K HL W H X B Y B I Y I X Y K X
9 6 8 anbi12d K HL W H X B Y B I X I Y I Y I X X K Y Y K X
10 simp1l K HL W H X B Y B K HL
11 10 hllatd K HL W H X B Y B K Lat
12 1 5 latasymb K Lat X B Y B X K Y Y K X X = Y
13 11 12 syld3an1 K HL W H X B Y B X K Y Y K X X = Y
14 9 13 bitrd K HL W H X B Y B I X I Y I Y I X X = Y
15 4 14 syl5bb K HL W H X B Y B I X = I Y X = Y