Metamath Proof Explorer

Theorem dihjat5N

Description: Transfer lattice join with atom to subspace sum. (Contributed by NM, 25-Apr-2015) (New usage is discouraged.)

Ref Expression
Hypotheses dihjat5.b 
|- B = ( Base ` K )
dihjat5.h 
|- H = ( LHyp ` K )
dihjat5.j 
|- .\/ = ( join ` K )
dihjat5.a 
|- A = ( Atoms ` K )
dihjat5.u 
|- U = ( ( DVecH ` K ) ` W )
dihjat5.s 
|- .(+) = ( LSSum ` U )
dihjat5.i 
|- I = ( ( DIsoH ` K ) ` W )
dihjat5.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dihjat5.x 
|- ( ph -> X e. B )
dihjat5.p 
|- ( ph -> P e. A )
Assertion dihjat5N 
|- ( ph -> ( X .\/ P ) = ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) )

Proof

Step Hyp Ref Expression
1 dihjat5.b 
 |-  B = ( Base ` K )
2 dihjat5.h 
 |-  H = ( LHyp ` K )
3 dihjat5.j 
 |-  .\/ = ( join ` K )
4 dihjat5.a 
 |-  A = ( Atoms ` K )
5 dihjat5.u 
 |-  U = ( ( DVecH ` K ) ` W )
6 dihjat5.s 
 |-  .(+) = ( LSSum ` U )
7 dihjat5.i 
 |-  I = ( ( DIsoH ` K ) ` W )
8 dihjat5.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 dihjat5.x 
 |-  ( ph -> X e. B )
10 dihjat5.p 
 |-  ( ph -> P e. A )
11 1 2 3 4 5 6 7 8 9 10 dihjat3 
 |-  ( ph -> ( I ` ( X .\/ P ) ) = ( ( I ` X ) .(+) ( I ` P ) ) )
12 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
13 1 2 7 dihcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) e. ran I )
14 8 9 13 syl2anc 
 |-  ( ph -> ( I ` X ) e. ran I )
15 4 2 5 7 12 dihatlat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ P e. A ) -> ( I ` P ) e. ( LSAtoms ` U ) )
16 8 10 15 syl2anc 
 |-  ( ph -> ( I ` P ) e. ( LSAtoms ` U ) )
17 2 7 5 6 12 8 14 16 dihsmatrn 
 |-  ( ph -> ( ( I ` X ) .(+) ( I ` P ) ) e. ran I )
18 2 7 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( I ` X ) .(+) ( I ` P ) ) e. ran I ) -> ( I ` ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) ) = ( ( I ` X ) .(+) ( I ` P ) ) )
19 8 17 18 syl2anc 
 |-  ( ph -> ( I ` ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) ) = ( ( I ` X ) .(+) ( I ` P ) ) )
20 11 19 eqtr4d 
 |-  ( ph -> ( I ` ( X .\/ P ) ) = ( I ` ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) ) )
21 8 simpld 
 |-  ( ph -> K e. HL )
22 21 hllatd 
 |-  ( ph -> K e. Lat )
23 1 4 atbase 
 |-  ( P e. A -> P e. B )
24 10 23 syl 
 |-  ( ph -> P e. B )
25 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ P e. B ) -> ( X .\/ P ) e. B )
26 22 9 24 25 syl3anc 
 |-  ( ph -> ( X .\/ P ) e. B )
27 1 2 7 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( I ` X ) .(+) ( I ` P ) ) e. ran I ) -> ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) e. B )
28 8 17 27 syl2anc 
 |-  ( ph -> ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) e. B )
29 1 2 7 dih11 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X .\/ P ) e. B /\ ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) e. B ) -> ( ( I ` ( X .\/ P ) ) = ( I ` ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) ) <-> ( X .\/ P ) = ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) ) )
30 8 26 28 29 syl3anc 
 |-  ( ph -> ( ( I ` ( X .\/ P ) ) = ( I ` ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) ) <-> ( X .\/ P ) = ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) ) )
31 20 30 mpbid 
 |-  ( ph -> ( X .\/ P ) = ( `' I ` ( ( I ` X ) .(+) ( I ` P ) ) ) )