Metamath Proof Explorer


Theorem cdlemk5auN

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 3-Jul-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemk1.b 𝐵 = ( Base ‘ 𝐾 )
cdlemk1.l = ( le ‘ 𝐾 )
cdlemk1.j = ( join ‘ 𝐾 )
cdlemk1.m = ( meet ‘ 𝐾 )
cdlemk1.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemk1.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemk1.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemk1.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemk1.s 𝑆 = ( 𝑓𝑇 ↦ ( 𝑖𝑇 ( 𝑖𝑃 ) = ( ( 𝑃 ( 𝑅𝑓 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑓 𝐹 ) ) ) ) ) )
cdlemk1.o 𝑂 = ( 𝑆𝐷 )
Assertion cdlemk5auN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐷𝑇𝐺𝑇𝑋𝑇 ) ∧ ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( ( ( 𝐷𝑃 ) ( 𝑅𝐷 ) ) ( ( 𝐷𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) ( ( 𝑋𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemk1.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemk1.l = ( le ‘ 𝐾 )
3 cdlemk1.j = ( join ‘ 𝐾 )
4 cdlemk1.m = ( meet ‘ 𝐾 )
5 cdlemk1.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemk1.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemk1.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemk1.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemk1.s 𝑆 = ( 𝑓𝑇 ↦ ( 𝑖𝑇 ( 𝑖𝑃 ) = ( ( 𝑃 ( 𝑅𝑓 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑓 𝐹 ) ) ) ) ) )
10 cdlemk1.o 𝑂 = ( 𝑆𝐷 )
11 1 2 3 5 6 7 8 4 cdlemk5a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐷𝑇𝐺𝑇𝑋𝑇 ) ∧ ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ∧ ( 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( ( ( 𝐷𝑃 ) ( 𝑅𝐷 ) ) ( ( 𝐷𝑃 ) ( 𝑅 ‘ ( 𝐺 𝐷 ) ) ) ) ( ( 𝑋𝑃 ) ( 𝑅 ‘ ( 𝑋 𝐷 ) ) ) )