Metamath Proof Explorer


Theorem dihmeetlem5

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 6-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 dihmeetlem5.b 𝐵 = ( Base ‘ 𝐾 )
2 dihmeetlem5.l = ( le ‘ 𝐾 )
3 dihmeetlem5.j = ( join ‘ 𝐾 )
4 dihmeetlem5.m = ( meet ‘ 𝐾 )
5 dihmeetlem5.a 𝐴 = ( Atoms ‘ 𝐾 )
6 simpl1 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑄𝐴𝑄 𝑋 ) ) → 𝐾 ∈ HL )
7 simprl ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑄𝐴𝑄 𝑋 ) ) → 𝑄𝐴 )
8 simpl2 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑄𝐴𝑄 𝑋 ) ) → 𝑋𝐵 )
9 simpl3 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑄𝐴𝑄 𝑋 ) ) → 𝑌𝐵 )
10 simprr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑄𝐴𝑄 𝑋 ) ) → 𝑄 𝑋 )
11 1 2 3 4 5 atmod2i1 ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴𝑋𝐵𝑌𝐵 ) ∧ 𝑄 𝑋 ) → ( ( 𝑋 𝑌 ) 𝑄 ) = ( 𝑋 ( 𝑌 𝑄 ) ) )
12 6 7 8 9 10 11 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑄𝐴𝑄 𝑋 ) ) → ( ( 𝑋 𝑌 ) 𝑄 ) = ( 𝑋 ( 𝑌 𝑄 ) ) )
13 12 eqcomd ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑄𝐴𝑄 𝑋 ) ) → ( 𝑋 ( 𝑌 𝑄 ) ) = ( ( 𝑋 𝑌 ) 𝑄 ) )