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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
hlmod.l ⊢ ≤ = ( le ‘ 𝐾 )
hlmod.j ⊢ ∨ = ( join ‘ 𝐾 )
hlmod.m ⊢ ∧ = ( meet ‘ 𝐾 )
hlmod.f ⊢ 𝐹 = ( pmap ‘ 𝐾 )
hlmod.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion hlmod1i ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) = ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ) )

Proof

Step Hyp Ref Expression
1 hlmod.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 hlmod.l ⊢ ≤ = ( le ‘ 𝐾 )
3 hlmod.j ⊢ ∨ = ( join ‘ 𝐾 )
4 hlmod.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 hlmod.f ⊢ 𝐹 = ( pmap ‘ 𝐾 )
6 hlmod.p ⊢ + = ( +𝑃 ‘ 𝐾 )
7 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
8 7 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → 𝐾 ∈ Lat )
9 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → 𝑋 ∈ 𝐵 )
10 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → 𝑌 ∈ 𝐵 )
11 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
12 8 9 10 11 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
13 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → 𝑍 ∈ 𝐵 )
14 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 )
15 8 12 13 14 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 )
16 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑍 ) ∈ 𝐵 )
17 8 10 13 16 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝑌 ∧ 𝑍 ) ∈ 𝐵 )
18 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑍 ) ∈ 𝐵 ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ∈ 𝐵 )
19 8 9 17 18 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ∈ 𝐵 )
20 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → 𝐾 ∈ HL )
21 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
22 1 21 5 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
23 20 9 22 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
24 1 21 5 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
25 20 10 24 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
26 eqid ⊢ ( PSubSp ‘ 𝐾 ) = ( PSubSp ‘ 𝐾 )
27 1 26 5 pmapsub ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑍 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑍 ) ∈ ( PSubSp ‘ 𝐾 ) )
28 8 13 27 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ 𝑍 ) ∈ ( PSubSp ‘ 𝐾 ) )
29 simp3l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → 𝑋 ≤ 𝑍 )
30 1 2 5 pmaple ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑍 ↔ ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐹 ‘ 𝑍 ) ) )
31 20 9 13 30 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝑋 ≤ 𝑍 ↔ ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐹 ‘ 𝑍 ) ) )
32 29 31 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐹 ‘ 𝑍 ) )
33 21 26 6 pmod1i ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝐹 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑍 ) ∈ ( PSubSp ‘ 𝐾 ) ) ) → ( ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐹 ‘ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( ( 𝐹 ‘ 𝑌 ) ∩ ( 𝐹 ‘ 𝑍 ) ) ) ) )
34 33 3impia ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝐹 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑍 ) ∈ ( PSubSp ‘ 𝐾 ) ) ∧ ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐹 ‘ 𝑍 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( ( 𝐹 ‘ 𝑌 ) ∩ ( 𝐹 ‘ 𝑍 ) ) ) )
35 20 23 25 28 32 34 syl131anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( ( 𝐹 ‘ 𝑌 ) ∩ ( 𝐹 ‘ 𝑍 ) ) ) )
36 1 4 21 5 pmapmeet ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) = ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) )
37 20 12 13 36 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) = ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) )
38 simp3r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) )
39 38 ineq1d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) = ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) )
40 37 39 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) = ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) )
41 1 4 21 5 pmapmeet ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝐹 ‘ 𝑌 ) ∩ ( 𝐹 ‘ 𝑍 ) ) )
42 20 10 13 41 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝐹 ‘ 𝑌 ) ∩ ( 𝐹 ‘ 𝑍 ) ) )
43 42 oveq2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ ( 𝑌 ∧ 𝑍 ) ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( ( 𝐹 ‘ 𝑌 ) ∩ ( 𝐹 ‘ 𝑍 ) ) ) )
44 35 40 43 3eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ ( 𝑌 ∧ 𝑍 ) ) ) )
45 1 3 5 6 pmapjoin ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑍 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ ( 𝑌 ∧ 𝑍 ) ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ) )
46 8 9 17 45 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ ( 𝑌 ∧ 𝑍 ) ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ) )
47 44 46 eqsstrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ) )
48 1 2 5 pmaple ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 ∧ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ∈ 𝐵 ) → ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ≤ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ↔ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ) ) )
49 20 15 19 48 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ≤ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ↔ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ) ) )
50 47 49 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ≤ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) )
51 1 2 3 4 mod1ile ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑍 → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) )
52 51 3impia ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑍 ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) )
53 8 9 10 13 29 52 syl131anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) )
54 1 2 8 15 19 50 53 latasymd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) = ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) )
55 54 3expia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑍 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) = ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ) )