Metamath Proof Explorer

Theorem dihjat4

Description: Transfer the subspace sum of a closed subspace and an atom back to lattice join. (Contributed by NM, 25-Apr-2015)

Ref Expression
Hypotheses dihjat4.j 
|- .\/ = ( join ` K )
dihjat4.h 
|- H = ( LHyp ` K )
dihjat4.i 
|- I = ( ( DIsoH ` K ) ` W )
dihjat4.u 
|- U = ( ( DVecH ` K ) ` W )
dihjat4.s 
|- .(+) = ( LSSum ` U )
dihjat4.a 
|- A = ( LSAtoms ` U )
dihjat4.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dihjat4.x 
|- ( ph -> X e. ran I )
dihjat4.q 
|- ( ph -> Q e. A )
Assertion dihjat4 
|- ( ph -> ( X .(+) Q ) = ( I ` ( ( `' I ` X ) .\/ ( `' I ` Q ) ) ) )

Proof

Step Hyp Ref Expression
1 dihjat4.j 
 |-  .\/ = ( join ` K )
2 dihjat4.h 
 |-  H = ( LHyp ` K )
3 dihjat4.i 
 |-  I = ( ( DIsoH ` K ) ` W )
4 dihjat4.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dihjat4.s 
 |-  .(+) = ( LSSum ` U )
6 dihjat4.a 
 |-  A = ( LSAtoms ` U )
7 dihjat4.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 dihjat4.x 
 |-  ( ph -> X e. ran I )
9 dihjat4.q 
 |-  ( ph -> Q e. A )
10 eqid 
 |-  ( Base ` K ) = ( Base ` K )
11 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
12 10 2 3 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. ( Base ` K ) )
13 7 8 12 syl2anc 
 |-  ( ph -> ( `' I ` X ) e. ( Base ` K ) )
14 11 2 4 3 6 dihlatat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) -> ( `' I ` Q ) e. ( Atoms ` K ) )
15 7 9 14 syl2anc 
 |-  ( ph -> ( `' I ` Q ) e. ( Atoms ` K ) )
16 10 2 1 11 4 5 3 7 13 15 dihjat3 
 |-  ( ph -> ( I ` ( ( `' I ` X ) .\/ ( `' I ` Q ) ) ) = ( ( I ` ( `' I ` X ) ) .(+) ( I ` ( `' I ` Q ) ) ) )
17 2 3 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X )
18 7 8 17 syl2anc 
 |-  ( ph -> ( I ` ( `' I ` X ) ) = X )
19 2 4 3 6 dih1dimat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) -> Q e. ran I )
20 7 9 19 syl2anc 
 |-  ( ph -> Q e. ran I )
21 2 3 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. ran I ) -> ( I ` ( `' I ` Q ) ) = Q )
22 7 20 21 syl2anc 
 |-  ( ph -> ( I ` ( `' I ` Q ) ) = Q )
23 18 22 oveq12d 
 |-  ( ph -> ( ( I ` ( `' I ` X ) ) .(+) ( I ` ( `' I ` Q ) ) ) = ( X .(+) Q ) )
24 16 23 eqtr2d 
 |-  ( ph -> ( X .(+) Q ) = ( I ` ( ( `' I ` X ) .\/ ( `' I ` Q ) ) ) )