Description: NOT NEEDED? TODO FIX COMMENT. r \/ g(s) = r \/ v_2 p. 115 last line. (Contributed by NM, 2-Apr-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemef46g.b | |
|
cdlemef46g.l | |
||
cdlemef46g.j | |
||
cdlemef46g.m | |
||
cdlemef46g.a | |
||
cdlemef46g.h | |
||
cdlemef46g.u | |
||
cdlemef46g.d | |
||
cdlemefs46g.e | |
||
cdlemef46g.f | |
||
cdlemef46.v | |
||
cdlemef46.n | |
||
cdlemefs46.o | |
||
cdlemef46.g | |
||
cdlemeg46.y | |
||
Assertion | cdlemeg46rjgN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemef46g.b | |
|
2 | cdlemef46g.l | |
|
3 | cdlemef46g.j | |
|
4 | cdlemef46g.m | |
|
5 | cdlemef46g.a | |
|
6 | cdlemef46g.h | |
|
7 | cdlemef46g.u | |
|
8 | cdlemef46g.d | |
|
9 | cdlemefs46g.e | |
|
10 | cdlemef46g.f | |
|
11 | cdlemef46.v | |
|
12 | cdlemef46.n | |
|
13 | cdlemefs46.o | |
|
14 | cdlemef46.g | |
|
15 | cdlemeg46.y | |
|
16 | eqid | |
|
17 | eqid | |
|
18 | eqid | |
|
19 | eqid | |
|
20 | eqid | |
|
21 | eqid | |
|
22 | eqid | |
|
23 | 1 2 3 4 5 6 7 11 16 17 18 19 20 21 22 | cdleme43cN | |
24 | 23 | 3adant3l | |
25 | simp1 | |
|
26 | simp21 | |
|
27 | simp23 | |
|
28 | simp3r | |
|
29 | 1 2 3 4 5 6 11 12 13 14 | cdlemeg47b | |
30 | 25 26 27 28 29 | syl121anc | |
31 | simp23l | |
|
32 | 12 18 | cdleme31sc | |
33 | 31 32 | syl | |
34 | 30 33 | eqtrd | |
35 | 34 | oveq2d | |
36 | 35 | oveq1d | |
37 | 15 36 | eqtrid | |
38 | 37 | oveq2d | |
39 | 24 35 38 | 3eqtr4d | |