Description: The subspace sum of two isomorphisms of lattice elements is less than the isomorphism of their lattice join. (Contributed by NM, 23-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dihsumssj.b | |
|
dihsumssj.h | |
||
dihsumssj.j | |
||
dihsumssj.u | |
||
dihsumssj.p | |
||
dihsumssj.i | |
||
dihsumssj.k | |
||
dihsumssj.x | |
||
dihsumssj.y | |
||
Assertion | dihsumssj | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihsumssj.b | |
|
2 | dihsumssj.h | |
|
3 | dihsumssj.j | |
|
4 | dihsumssj.u | |
|
5 | dihsumssj.p | |
|
6 | dihsumssj.i | |
|
7 | dihsumssj.k | |
|
8 | dihsumssj.x | |
|
9 | dihsumssj.y | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | 1 2 6 4 10 | dihss | |
13 | 7 8 12 | syl2anc | |
14 | 1 2 6 4 10 | dihss | |
15 | 7 9 14 | syl2anc | |
16 | 2 4 10 5 11 7 13 15 | djhsumss | |
17 | 1 3 2 6 11 | djhlj | |
18 | 7 8 9 17 | syl12anc | |
19 | 16 18 | sseqtrrd | |