Metamath Proof Explorer


Theorem cdlemg4b12

Description: TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013)

Ref Expression
Hypotheses cdlemg4.l = ( le ‘ 𝐾 )
cdlemg4.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemg4.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg4.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemg4.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemg4.j = ( join ‘ 𝐾 )
cdlemg4b.v 𝑉 = ( 𝑅𝐺 )
Assertion cdlemg4b12 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝐺𝑇 ) → ( ( 𝐺𝑃 ) 𝑉 ) = ( 𝑃 𝑉 ) )

Proof

Step Hyp Ref Expression
1 cdlemg4.l = ( le ‘ 𝐾 )
2 cdlemg4.a 𝐴 = ( Atoms ‘ 𝐾 )
3 cdlemg4.h 𝐻 = ( LHyp ‘ 𝐾 )
4 cdlemg4.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 cdlemg4.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6 cdlemg4.j = ( join ‘ 𝐾 )
7 cdlemg4b.v 𝑉 = ( 𝑅𝐺 )
8 1 2 3 4 5 6 7 cdlemg4b2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝐺𝑇 ) → ( ( 𝐺𝑃 ) 𝑉 ) = ( 𝑃 ( 𝐺𝑃 ) ) )
9 1 2 3 4 5 6 7 cdlemg4b1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝐺𝑇 ) → ( 𝑃 𝑉 ) = ( 𝑃 ( 𝐺𝑃 ) ) )
10 8 9 eqtr4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝐺𝑇 ) → ( ( 𝐺𝑃 ) 𝑉 ) = ( 𝑃 𝑉 ) )