Metamath Proof Explorer


Theorem cdlemg6a

Description: TODO: FIX COMMENT. TODO: replace with cdlemg4 . (Contributed by NM, 27-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 cdlemg6a ( ( ( 𝐾 ∈ 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 cdlemg4 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑟𝐴 ∧ ¬ 𝑟 𝑊 ) ∧ 𝐹𝑇 ) ∧ ( 𝐺𝑇 ∧ ¬ 𝑟 ( 𝑃 𝑉 ) ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) = 𝑃 ) ) → ( 𝐹 ‘ ( 𝐺𝑟 ) ) = 𝑟 )