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 = ( Base ` K )
dihsumssj.h 
|- H = ( LHyp ` K )
dihsumssj.j 
|- .\/ = ( join ` K )
dihsumssj.u 
|- U = ( ( DVecH ` K ) ` W )
dihsumssj.p 
|- .(+) = ( LSSum ` U )
dihsumssj.i 
|- I = ( ( DIsoH ` K ) ` W )
dihsumssj.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dihsumssj.x 
|- ( ph -> X e. B )
dihsumssj.y 
|- ( ph -> Y e. B )
Assertion dihsumssj 
|- ( ph -> ( ( I ` X ) .(+) ( I ` Y ) ) C_ ( I ` ( X .\/ Y ) ) )

Proof

Step Hyp Ref Expression
1 dihsumssj.b 
 |-  B = ( Base ` K )
2 dihsumssj.h 
 |-  H = ( LHyp ` K )
3 dihsumssj.j 
 |-  .\/ = ( join ` K )
4 dihsumssj.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dihsumssj.p 
 |-  .(+) = ( LSSum ` U )
6 dihsumssj.i 
 |-  I = ( ( DIsoH ` K ) ` W )
7 dihsumssj.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 dihsumssj.x 
 |-  ( ph -> X e. B )
9 dihsumssj.y 
 |-  ( ph -> Y e. B )
10 eqid 
 |-  ( Base ` U ) = ( Base ` U )
11 eqid 
 |-  ( ( joinH ` K ) ` W ) = ( ( joinH ` K ) ` W )
12 1 2 6 4 10 dihss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) C_ ( Base ` U ) )
13 7 8 12 syl2anc 
 |-  ( ph -> ( I ` X ) C_ ( Base ` U ) )
14 1 2 6 4 10 dihss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. B ) -> ( I ` Y ) C_ ( Base ` U ) )
15 7 9 14 syl2anc 
 |-  ( ph -> ( I ` Y ) C_ ( Base ` U ) )
16 2 4 10 5 11 7 13 15 djhsumss 
 |-  ( ph -> ( ( I ` X ) .(+) ( I ` Y ) ) C_ ( ( I ` X ) ( ( joinH ` K ) ` W ) ( I ` Y ) ) )
17 1 3 2 6 11 djhlj 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) ) -> ( I ` ( X .\/ Y ) ) = ( ( I ` X ) ( ( joinH ` K ) ` W ) ( I ` Y ) ) )
18 7 8 9 17 syl12anc 
 |-  ( ph -> ( I ` ( X .\/ Y ) ) = ( ( I ` X ) ( ( joinH ` K ) ` W ) ( I ` Y ) ) )
19 16 18 sseqtrrd 
 |-  ( ph -> ( ( I ` X ) .(+) ( I ` Y ) ) C_ ( I ` ( X .\/ Y ) ) )