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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑃 ) ∨ 𝑉 ) = ( 𝑃 ∨ 𝑉 ) )