Description: The composition of two translations is a translation. Part of proof of Lemma G of Crawley p. 116, line 15 on p. 117. (Contributed by NM, 31-May-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ltrnco.h | |
|
ltrnco.t | |
||
Assertion | ltrnco | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltrnco.h | |
|
2 | ltrnco.t | |
|
3 | simp1 | |
|
4 | eqid | |
|
5 | 1 4 2 | ltrnldil | |
6 | 5 | 3adant3 | |
7 | 1 4 2 | ltrnldil | |
8 | 7 | 3adant2 | |
9 | 1 4 | ldilco | |
10 | 3 6 8 9 | syl3anc | |
11 | simp11 | |
|
12 | simp2l | |
|
13 | simp3l | |
|
14 | 12 13 | jca | |
15 | simp2r | |
|
16 | simp3r | |
|
17 | 15 16 | jca | |
18 | simp12 | |
|
19 | simp13 | |
|
20 | eqid | |
|
21 | eqid | |
|
22 | eqid | |
|
23 | eqid | |
|
24 | 20 21 22 23 1 2 | cdlemg41 | |
25 | 11 14 17 18 19 24 | syl122anc | |
26 | 25 | 3exp | |
27 | 26 | ralrimivv | |
28 | 20 21 22 23 1 4 2 | isltrn | |
29 | 28 | 3ad2ant1 | |
30 | 10 27 29 | mpbir2and | |