Metamath Proof Explorer


Theorem dihsumssj

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 B=BaseK
dihsumssj.h H=LHypK
dihsumssj.j ˙=joinK
dihsumssj.u U=DVecHKW
dihsumssj.p ˙=LSSumU
dihsumssj.i I=DIsoHKW
dihsumssj.k φKHLWH
dihsumssj.x φXB
dihsumssj.y φYB
Assertion dihsumssj φIX˙IYIX˙Y

Proof

Step Hyp Ref Expression
1 dihsumssj.b B=BaseK
2 dihsumssj.h H=LHypK
3 dihsumssj.j ˙=joinK
4 dihsumssj.u U=DVecHKW
5 dihsumssj.p ˙=LSSumU
6 dihsumssj.i I=DIsoHKW
7 dihsumssj.k φKHLWH
8 dihsumssj.x φXB
9 dihsumssj.y φYB
10 eqid BaseU=BaseU
11 eqid joinHKW=joinHKW
12 1 2 6 4 10 dihss KHLWHXBIXBaseU
13 7 8 12 syl2anc φIXBaseU
14 1 2 6 4 10 dihss KHLWHYBIYBaseU
15 7 9 14 syl2anc φIYBaseU
16 2 4 10 5 11 7 13 15 djhsumss φIX˙IYIXjoinHKWIY
17 1 3 2 6 11 djhlj KHLWHXBYBIX˙Y=IXjoinHKWIY
18 7 8 9 17 syl12anc φIX˙Y=IXjoinHKWIY
19 16 18 sseqtrrd φIX˙IYIX˙Y