Metamath Proof Explorer

Theorem cdleme39a

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one on P .\/ Q line. TODO: FIX COMMENT. E , Y , G , Z serve as f(t), f(u), f_t( R ), f_t( S ). Put hypotheses of cdleme38n in convention of cdleme32sn1awN . TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013)

Ref Expression
Hypotheses cdleme39.l
cdleme39.j
cdleme39.m
cdleme39.a $⊢ A = Atoms ⁡ K$
cdleme39.h $⊢ H = LHyp ⁡ K$
cdleme39.u
cdleme39.e
cdleme39.g
cdleme39a.v
Assertion cdleme39a

Proof

Step Hyp Ref Expression
1 cdleme39.l
2 cdleme39.j
3 cdleme39.m
4 cdleme39.a $⊢ A = Atoms ⁡ K$
5 cdleme39.h $⊢ H = LHyp ⁡ K$
6 cdleme39.u
7 cdleme39.e
8 cdleme39.g
9 cdleme39a.v
10 simp11
11 simp12
12 simp13
13 simp2
14 simp3l
15 1 2 3 4 5 6 cdleme4
16 10 11 12 13 14 15 syl131anc
17 simp3r
18 1 2 3 4 5 6 7 cdleme2
19 10 11 12 17 18 syl13anc
20 9 19 syl5eq
21 20 oveq2d
22 16 21 eqtr4d
23 simp11l
24 simp2l
25 simp3rl
26 2 4 hlatjcom
27 23 24 25 26 syl3anc
28 27 oveq1d
29 28 oveq2d
30 22 29 oveq12d
31 8 30 syl5eq