Metamath Proof Explorer

Theorem pmapjat2

Description: The projective map of the join of an atom with a lattice element. (Contributed by NM, 12-May-2012)

Ref Expression
Hypotheses pmapjat.b 
|- B = ( Base ` K )
pmapjat.j 
|- .\/ = ( join ` K )
pmapjat.a 
|- A = ( Atoms ` K )
pmapjat.m 
|- M = ( pmap ` K )
pmapjat.p 
|- .+ = ( +P ` K )
Assertion pmapjat2 
|- ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` ( Q .\/ X ) ) = ( ( M ` Q ) .+ ( M ` X ) ) )

Proof

Step Hyp Ref Expression
1 pmapjat.b 
 |-  B = ( Base ` K )
2 pmapjat.j 
 |-  .\/ = ( join ` K )
3 pmapjat.a 
 |-  A = ( Atoms ` K )
4 pmapjat.m 
 |-  M = ( pmap ` K )
5 pmapjat.p 
 |-  .+ = ( +P ` K )
6 1 2 3 4 5 pmapjat1 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` ( X .\/ Q ) ) = ( ( M ` X ) .+ ( M ` Q ) ) )
7 hllat 
 |-  ( K e. HL -> K e. Lat )
8 7 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> K e. Lat )
9 1 3 atbase 
 |-  ( Q e. A -> Q e. B )
10 9 3ad2ant3 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> Q e. B )
11 simp2 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> X e. B )
12 1 2 latjcom 
 |-  ( ( K e. Lat /\ Q e. B /\ X e. B ) -> ( Q .\/ X ) = ( X .\/ Q ) )
13 8 10 11 12 syl3anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( Q .\/ X ) = ( X .\/ Q ) )
14 13 fveq2d 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` ( Q .\/ X ) ) = ( M ` ( X .\/ Q ) ) )
15 simp1 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> K e. HL )
16 1 3 4 pmapssat 
 |-  ( ( K e. HL /\ Q e. B ) -> ( M ` Q ) C_ A )
17 15 10 16 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` Q ) C_ A )
18 1 3 4 pmapssat 
 |-  ( ( K e. HL /\ X e. B ) -> ( M ` X ) C_ A )
19 18 3adant3 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` X ) C_ A )
20 3 5 paddcom 
 |-  ( ( K e. Lat /\ ( M ` Q ) C_ A /\ ( M ` X ) C_ A ) -> ( ( M ` Q ) .+ ( M ` X ) ) = ( ( M ` X ) .+ ( M ` Q ) ) )
21 8 17 19 20 syl3anc 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( ( M ` Q ) .+ ( M ` X ) ) = ( ( M ` X ) .+ ( M ` Q ) ) )
22 6 14 21 3eqtr4d 
 |-  ( ( K e. HL /\ X e. B /\ Q e. A ) -> ( M ` ( Q .\/ X ) ) = ( ( M ` Q ) .+ ( M ` X ) ) )