Metamath Proof Explorer


Theorem dihmeetlem6

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014)

Ref Expression
Hypotheses dihmeetlem6.b 𝐵 = ( Base ‘ 𝐾 )
dihmeetlem6.l = ( le ‘ 𝐾 )
dihmeetlem6.h 𝐻 = ( LHyp ‘ 𝐾 )
dihmeetlem6.j = ( join ‘ 𝐾 )
dihmeetlem6.m = ( meet ‘ 𝐾 )
dihmeetlem6.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion dihmeetlem6 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → ¬ ( 𝑋 ( 𝑌 𝑄 ) ) 𝑊 )

Proof

Step Hyp Ref Expression
1 dihmeetlem6.b 𝐵 = ( Base ‘ 𝐾 )
2 dihmeetlem6.l = ( le ‘ 𝐾 )
3 dihmeetlem6.h 𝐻 = ( LHyp ‘ 𝐾 )
4 dihmeetlem6.j = ( join ‘ 𝐾 )
5 dihmeetlem6.m = ( meet ‘ 𝐾 )
6 dihmeetlem6.a 𝐴 = ( Atoms ‘ 𝐾 )
7 simprlr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → ¬ 𝑄 𝑊 )
8 simpl1l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → 𝐾 ∈ HL )
9 8 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → 𝐾 ∈ Lat )
10 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → 𝑋𝐵 )
11 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → 𝑌𝐵 )
12 1 5 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
13 9 10 11 12 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
14 simprll ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → 𝑄𝐴 )
15 1 6 atbase ( 𝑄𝐴𝑄𝐵 )
16 14 15 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → 𝑄𝐵 )
17 simpl1r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → 𝑊𝐻 )
18 1 3 lhpbase ( 𝑊𝐻𝑊𝐵 )
19 17 18 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → 𝑊𝐵 )
20 1 2 4 latjle12 ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 𝑌 ) ∈ 𝐵𝑄𝐵𝑊𝐵 ) ) → ( ( ( 𝑋 𝑌 ) 𝑊𝑄 𝑊 ) ↔ ( ( 𝑋 𝑌 ) 𝑄 ) 𝑊 ) )
21 9 13 16 19 20 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → ( ( ( 𝑋 𝑌 ) 𝑊𝑄 𝑊 ) ↔ ( ( 𝑋 𝑌 ) 𝑄 ) 𝑊 ) )
22 simpr ( ( ( 𝑋 𝑌 ) 𝑊𝑄 𝑊 ) → 𝑄 𝑊 )
23 21 22 syl6bir ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → ( ( ( 𝑋 𝑌 ) 𝑄 ) 𝑊𝑄 𝑊 ) )
24 7 23 mtod ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → ¬ ( ( 𝑋 𝑌 ) 𝑄 ) 𝑊 )
25 simprr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → 𝑄 𝑋 )
26 1 2 4 5 6 dihmeetlem5 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑄𝐴𝑄 𝑋 ) ) → ( 𝑋 ( 𝑌 𝑄 ) ) = ( ( 𝑋 𝑌 ) 𝑄 ) )
27 8 10 11 14 25 26 syl32anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → ( 𝑋 ( 𝑌 𝑄 ) ) = ( ( 𝑋 𝑌 ) 𝑄 ) )
28 27 breq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → ( ( 𝑋 ( 𝑌 𝑄 ) ) 𝑊 ↔ ( ( 𝑋 𝑌 ) 𝑄 ) 𝑊 ) )
29 24 28 mtbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝑄 𝑋 ) ) → ¬ ( 𝑋 ( 𝑌 𝑄 ) ) 𝑊 )