Metamath Proof Explorer


Theorem cdlemg4g

Description: TODO: FIX COMMENT. (Contributed by NM, 25-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 𝑉 = ( 𝑅𝐺 )
cdlemg4.m = ( meet ‘ 𝐾 )
Assertion cdlemg4g ( ( ( 𝐾 ∈ 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 cdlemg4.m = ( meet ‘ 𝐾 )
9 1 2 3 4 5 6 7 8 cdlemg4f ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝐹𝑇 ) ∧ ( 𝐺𝑇 ∧ ¬ 𝑄 ( 𝑃 𝑉 ) ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) = 𝑃 ) ) → ( 𝐹 ‘ ( 𝐺𝑄 ) ) = ( ( 𝑄 𝑉 ) ( 𝑃 ( ( 𝑃 𝑄 ) 𝑊 ) ) ) )
10 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝐹𝑇 ) ∧ ( 𝐺𝑇 ∧ ¬ 𝑄 ( 𝑃 𝑉 ) ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) = 𝑃 ) ) → 𝐾 ∈ HL )
11 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝐹𝑇 ) ∧ ( 𝐺𝑇 ∧ ¬ 𝑄 ( 𝑃 𝑉 ) ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) = 𝑃 ) ) → 𝑊𝐻 )
12 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝐹𝑇 ) ∧ ( 𝐺𝑇 ∧ ¬ 𝑄 ( 𝑃 𝑉 ) ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) = 𝑃 ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
13 simp22l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝐹𝑇 ) ∧ ( 𝐺𝑇 ∧ ¬ 𝑄 ( 𝑃 𝑉 ) ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) = 𝑃 ) ) → 𝑄𝐴 )
14 eqid ( ( 𝑃 𝑄 ) 𝑊 ) = ( ( 𝑃 𝑄 ) 𝑊 )
15 1 6 8 2 3 14 cdleme0cp ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ) ) → ( 𝑃 ( ( 𝑃 𝑄 ) 𝑊 ) ) = ( 𝑃 𝑄 ) )
16 10 11 12 13 15 syl22anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝐹𝑇 ) ∧ ( 𝐺𝑇 ∧ ¬ 𝑄 ( 𝑃 𝑉 ) ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) = 𝑃 ) ) → ( 𝑃 ( ( 𝑃 𝑄 ) 𝑊 ) ) = ( 𝑃 𝑄 ) )
17 16 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝐹𝑇 ) ∧ ( 𝐺𝑇 ∧ ¬ 𝑄 ( 𝑃 𝑉 ) ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) = 𝑃 ) ) → ( ( 𝑄 𝑉 ) ( 𝑃 ( ( 𝑃 𝑄 ) 𝑊 ) ) ) = ( ( 𝑄 𝑉 ) ( 𝑃 𝑄 ) ) )
18 9 17 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ 𝐹𝑇 ) ∧ ( 𝐺𝑇 ∧ ¬ 𝑄 ( 𝑃 𝑉 ) ∧ ( 𝐹 ‘ ( 𝐺𝑃 ) ) = 𝑃 ) ) → ( 𝐹 ‘ ( 𝐺𝑄 ) ) = ( ( 𝑄 𝑉 ) ( 𝑃 𝑄 ) ) )