This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlmod1i

Description: A version of the modular law pmod1i that holds in a Hilbert lattice. (Contributed by NM, 13-May-2012)

Ref Expression
Hypotheses hlmod.b 
|- B = ( Base ` K )
hlmod.l 
|- .<_ = ( le ` K )
hlmod.j 
|- .\/ = ( join ` K )
hlmod.m 
|- ./\ = ( meet ` K )
hlmod.f 
|- F = ( pmap ` K )
hlmod.p 
|- .+ = ( +P ` K )
Assertion hlmod1i 
|- ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) -> ( ( X .\/ Y ) ./\ Z ) = ( X .\/ ( Y ./\ Z ) ) ) )

Proof

Step Hyp Ref Expression
1 hlmod.b 
 |-  B = ( Base ` K )
2 hlmod.l 
 |-  .<_ = ( le ` K )
3 hlmod.j 
 |-  .\/ = ( join ` K )
4 hlmod.m 
 |-  ./\ = ( meet ` K )
5 hlmod.f 
 |-  F = ( pmap ` K )
6 hlmod.p 
 |-  .+ = ( +P ` K )
7 hllat 
 |-  ( K e. HL -> K e. Lat )
8 7 3ad2ant1 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> K e. Lat )
9 simp21 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> X e. B )
10 simp22 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> Y e. B )
11 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
12 8 9 10 11 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( X .\/ Y ) e. B )
13 simp23 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> Z e. B )
14 1 4 latmcl 
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ Z e. B ) -> ( ( X .\/ Y ) ./\ Z ) e. B )
15 8 12 13 14 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( ( X .\/ Y ) ./\ Z ) e. B )
16 1 4 latmcl 
 |-  ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> ( Y ./\ Z ) e. B )
17 8 10 13 16 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( Y ./\ Z ) e. B )
18 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ ( Y ./\ Z ) e. B ) -> ( X .\/ ( Y ./\ Z ) ) e. B )
19 8 9 17 18 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( X .\/ ( Y ./\ Z ) ) e. B )
20 simp1 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> K e. HL )
21 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
22 1 21 5 pmapssat 
 |-  ( ( K e. HL /\ X e. B ) -> ( F ` X ) C_ ( Atoms ` K ) )
23 20 9 22 syl2anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( F ` X ) C_ ( Atoms ` K ) )
24 1 21 5 pmapssat 
 |-  ( ( K e. HL /\ Y e. B ) -> ( F ` Y ) C_ ( Atoms ` K ) )
25 20 10 24 syl2anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( F ` Y ) C_ ( Atoms ` K ) )
26 eqid 
 |-  ( PSubSp ` K ) = ( PSubSp ` K )
27 1 26 5 pmapsub 
 |-  ( ( K e. Lat /\ Z e. B ) -> ( F ` Z ) e. ( PSubSp ` K ) )
28 8 13 27 syl2anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( F ` Z ) e. ( PSubSp ` K ) )
29 simp3l 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> X .<_ Z )
30 1 2 5 pmaple 
 |-  ( ( K e. HL /\ X e. B /\ Z e. B ) -> ( X .<_ Z <-> ( F ` X ) C_ ( F ` Z ) ) )
31 20 9 13 30 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( X .<_ Z <-> ( F ` X ) C_ ( F ` Z ) ) )
32 29 31 mpbid 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( F ` X ) C_ ( F ` Z ) )
33 21 26 6 pmod1i 
 |-  ( ( K e. HL /\ ( ( F ` X ) C_ ( Atoms ` K ) /\ ( F ` Y ) C_ ( Atoms ` K ) /\ ( F ` Z ) e. ( PSubSp ` K ) ) ) -> ( ( F ` X ) C_ ( F ` Z ) -> ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) = ( ( F ` X ) .+ ( ( F ` Y ) i^i ( F ` Z ) ) ) ) )
34 33 3impia 
 |-  ( ( K e. HL /\ ( ( F ` X ) C_ ( Atoms ` K ) /\ ( F ` Y ) C_ ( Atoms ` K ) /\ ( F ` Z ) e. ( PSubSp ` K ) ) /\ ( F ` X ) C_ ( F ` Z ) ) -> ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) = ( ( F ` X ) .+ ( ( F ` Y ) i^i ( F ` Z ) ) ) )
35 20 23 25 28 32 34 syl131anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) = ( ( F ` X ) .+ ( ( F ` Y ) i^i ( F ` Z ) ) ) )
36 1 4 21 5 pmapmeet 
 |-  ( ( K e. HL /\ ( X .\/ Y ) e. B /\ Z e. B ) -> ( F ` ( ( X .\/ Y ) ./\ Z ) ) = ( ( F ` ( X .\/ Y ) ) i^i ( F ` Z ) ) )
37 20 12 13 36 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( F ` ( ( X .\/ Y ) ./\ Z ) ) = ( ( F ` ( X .\/ Y ) ) i^i ( F ` Z ) ) )
38 simp3r 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) )
39 38 ineq1d 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( ( F ` ( X .\/ Y ) ) i^i ( F ` Z ) ) = ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) )
40 37 39 eqtrd 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( F ` ( ( X .\/ Y ) ./\ Z ) ) = ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) )
41 1 4 21 5 pmapmeet 
 |-  ( ( K e. HL /\ Y e. B /\ Z e. B ) -> ( F ` ( Y ./\ Z ) ) = ( ( F ` Y ) i^i ( F ` Z ) ) )
42 20 10 13 41 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( F ` ( Y ./\ Z ) ) = ( ( F ` Y ) i^i ( F ` Z ) ) )
43 42 oveq2d 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( ( F ` X ) .+ ( F ` ( Y ./\ Z ) ) ) = ( ( F ` X ) .+ ( ( F ` Y ) i^i ( F ` Z ) ) ) )
44 35 40 43 3eqtr4d 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( F ` ( ( X .\/ Y ) ./\ Z ) ) = ( ( F ` X ) .+ ( F ` ( Y ./\ Z ) ) ) )
45 1 3 5 6 pmapjoin 
 |-  ( ( K e. Lat /\ X e. B /\ ( Y ./\ Z ) e. B ) -> ( ( F ` X ) .+ ( F ` ( Y ./\ Z ) ) ) C_ ( F ` ( X .\/ ( Y ./\ Z ) ) ) )
46 8 9 17 45 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( ( F ` X ) .+ ( F ` ( Y ./\ Z ) ) ) C_ ( F ` ( X .\/ ( Y ./\ Z ) ) ) )
47 44 46 eqsstrd 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( F ` ( ( X .\/ Y ) ./\ Z ) ) C_ ( F ` ( X .\/ ( Y ./\ Z ) ) ) )
48 1 2 5 pmaple 
 |-  ( ( K e. HL /\ ( ( X .\/ Y ) ./\ Z ) e. B /\ ( X .\/ ( Y ./\ Z ) ) e. B ) -> ( ( ( X .\/ Y ) ./\ Z ) .<_ ( X .\/ ( Y ./\ Z ) ) <-> ( F ` ( ( X .\/ Y ) ./\ Z ) ) C_ ( F ` ( X .\/ ( Y ./\ Z ) ) ) ) )
49 20 15 19 48 syl3anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( ( ( X .\/ Y ) ./\ Z ) .<_ ( X .\/ ( Y ./\ Z ) ) <-> ( F ` ( ( X .\/ Y ) ./\ Z ) ) C_ ( F ` ( X .\/ ( Y ./\ Z ) ) ) ) )
50 47 49 mpbird 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( ( X .\/ Y ) ./\ Z ) .<_ ( X .\/ ( Y ./\ Z ) ) )
51 1 2 3 4 mod1ile 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Z -> ( X .\/ ( Y ./\ Z ) ) .<_ ( ( X .\/ Y ) ./\ Z ) ) )
52 51 3impia 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X .<_ Z ) -> ( X .\/ ( Y ./\ Z ) ) .<_ ( ( X .\/ Y ) ./\ Z ) )
53 8 9 10 13 29 52 syl131anc 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( X .\/ ( Y ./\ Z ) ) .<_ ( ( X .\/ Y ) ./\ Z ) )
54 1 2 8 15 19 50 53 latasymd 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) ) -> ( ( X .\/ Y ) ./\ Z ) = ( X .\/ ( Y ./\ Z ) ) )
55 54 3expia 
 |-  ( ( K e. HL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Z /\ ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) ) -> ( ( X .\/ Y ) ./\ Z ) = ( X .\/ ( Y ./\ Z ) ) ) )