Description: A basis element has unit length. (Contributed by Mario Carneiro, 23-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | obsipid.h | |
|
obsipid.f | |
||
obsipid.u | |
||
Assertion | obsipid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | obsipid.h | |
|
2 | obsipid.f | |
|
3 | obsipid.u | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 4 1 2 3 5 | obsip | |
7 | 6 | 3anidm23 | |
8 | eqid | |
|
9 | 8 | iftruei | |
10 | 7 9 | eqtrdi | |