Metamath Proof Explorer

Theorem atmod1i1m

Description: Version of modular law pmod1i that holds in a Hilbert lattice, when an element meets an atom. (Contributed by NM, 2-Sep-2012) (Revised by Mario Carneiro, 10-May-2013)

Ref Expression
Hypotheses atmod.b 
|- B = ( Base ` K )
atmod.l 
|- .<_ = ( le ` K )
atmod.j 
|- .\/ = ( join ` K )
atmod.m 
|- ./\ = ( meet ` K )
atmod.a 
|- A = ( Atoms ` K )
Assertion atmod1i1m 
|- ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) -> ( ( X ./\ P ) .\/ ( Y ./\ Z ) ) = ( ( ( X ./\ P ) .\/ Y ) ./\ Z ) )

Proof

Step Hyp Ref Expression
1 atmod.b 
 |-  B = ( Base ` K )
2 atmod.l 
 |-  .<_ = ( le ` K )
3 atmod.j 
 |-  .\/ = ( join ` K )
4 atmod.m 
 |-  ./\ = ( meet ` K )
5 atmod.a 
 |-  A = ( Atoms ` K )
6 simpl1l 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) e. A ) -> K e. HL )
7 simpr 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) e. A ) -> ( X ./\ P ) e. A )
8 simpl22 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) e. A ) -> Y e. B )
9 simpl23 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) e. A ) -> Z e. B )
10 simpl3 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) e. A ) -> ( X ./\ P ) .<_ Z )
11 1 2 3 4 5 atmod1i1 
 |-  ( ( K e. HL /\ ( ( X ./\ P ) e. A /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) -> ( ( X ./\ P ) .\/ ( Y ./\ Z ) ) = ( ( ( X ./\ P ) .\/ Y ) ./\ Z ) )
12 6 7 8 9 10 11 syl131anc 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) e. A ) -> ( ( X ./\ P ) .\/ ( Y ./\ Z ) ) = ( ( ( X ./\ P ) .\/ Y ) ./\ Z ) )
13 simp1l 
 |-  ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) -> K e. HL )
14 hlol 
 |-  ( K e. HL -> K e. OL )
15 13 14 syl 
 |-  ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) -> K e. OL )
16 15 adantr 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> K e. OL )
17 13 hllatd 
 |-  ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) -> K e. Lat )
18 17 adantr 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> K e. Lat )
19 simpl22 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> Y e. B )
20 simpl23 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> Z e. B )
21 1 4 latmcl 
 |-  ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> ( Y ./\ Z ) e. B )
22 18 19 20 21 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> ( Y ./\ Z ) e. B )
23 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
24 1 3 23 olj02 
 |-  ( ( K e. OL /\ ( Y ./\ Z ) e. B ) -> ( ( 0. ` K ) .\/ ( Y ./\ Z ) ) = ( Y ./\ Z ) )
25 16 22 24 syl2anc 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> ( ( 0. ` K ) .\/ ( Y ./\ Z ) ) = ( Y ./\ Z ) )
26 oveq1 
 |-  ( ( X ./\ P ) = ( 0. ` K ) -> ( ( X ./\ P ) .\/ ( Y ./\ Z ) ) = ( ( 0. ` K ) .\/ ( Y ./\ Z ) ) )
27 26 adantl 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> ( ( X ./\ P ) .\/ ( Y ./\ Z ) ) = ( ( 0. ` K ) .\/ ( Y ./\ Z ) ) )
28 oveq1 
 |-  ( ( X ./\ P ) = ( 0. ` K ) -> ( ( X ./\ P ) .\/ Y ) = ( ( 0. ` K ) .\/ Y ) )
29 28 adantl 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> ( ( X ./\ P ) .\/ Y ) = ( ( 0. ` K ) .\/ Y ) )
30 1 3 23 olj02 
 |-  ( ( K e. OL /\ Y e. B ) -> ( ( 0. ` K ) .\/ Y ) = Y )
31 16 19 30 syl2anc 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> ( ( 0. ` K ) .\/ Y ) = Y )
32 29 31 eqtrd 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> ( ( X ./\ P ) .\/ Y ) = Y )
33 32 oveq1d 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> ( ( ( X ./\ P ) .\/ Y ) ./\ Z ) = ( Y ./\ Z ) )
34 25 27 33 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) /\ ( X ./\ P ) = ( 0. ` K ) ) -> ( ( X ./\ P ) .\/ ( Y ./\ Z ) ) = ( ( ( X ./\ P ) .\/ Y ) ./\ Z ) )
35 simp21 
 |-  ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) -> X e. B )
36 simp1r 
 |-  ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) -> P e. A )
37 1 4 23 5 meetat2 
 |-  ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) e. A \/ ( X ./\ P ) = ( 0. ` K ) ) )
38 15 35 36 37 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) -> ( ( X ./\ P ) e. A \/ ( X ./\ P ) = ( 0. ` K ) ) )
39 12 34 38 mpjaodan 
 |-  ( ( ( K e. HL /\ P e. A ) /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X ./\ P ) .<_ Z ) -> ( ( X ./\ P ) .\/ ( Y ./\ Z ) ) = ( ( ( X ./\ P ) .\/ Y ) ./\ Z ) )