Metamath Proof Explorer

Theorem dihjat6

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

Proof

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