Metamath Proof Explorer


Theorem cdlemg10b

Description: TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? (Contributed by NM, 4-May-2013)

Ref Expression
Hypotheses cdlemg8.l = ( le ‘ 𝐾 )
cdlemg8.j = ( join ‘ 𝐾 )
cdlemg8.m = ( meet ‘ 𝐾 )
cdlemg8.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemg8.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg8.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemg10b ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝐹𝑇 ) → ( ( ( 𝐹𝑃 ) ( 𝐹𝑄 ) ) 𝑊 ) = ( ( 𝑃 𝑄 ) 𝑊 ) )

Proof

Step Hyp Ref Expression
1 cdlemg8.l = ( le ‘ 𝐾 )
2 cdlemg8.j = ( join ‘ 𝐾 )
3 cdlemg8.m = ( meet ‘ 𝐾 )
4 cdlemg8.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdlemg8.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdlemg8.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 eqid ( ( 𝑃 𝑄 ) 𝑊 ) = ( ( 𝑃 𝑄 ) 𝑊 )
8 5 6 1 2 4 3 7 cdlemg2m ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝐹𝑇 ) → ( ( ( 𝐹𝑃 ) ( 𝐹𝑄 ) ) 𝑊 ) = ( ( 𝑃 𝑄 ) 𝑊 ) )