Theorem cdlemc

Description: Lemma C in Crawley p. 113. (Contributed by NM, 26-May-2012)

	Ref	Expression
Hypotheses	cdlemc3.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemc3.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemc3.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemc3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemc3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemc3.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemc3.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	cdlemc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝐹 ‘ 𝑄 ) = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemc3.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemc3.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdlemc3.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdlemc3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdlemc3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdlemc3.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		cdlemc3.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		simpl2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
10		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ‘ 𝑃 ) = 𝑃 )
11	1 2 3 4 5 6 7	cdlemc6	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ‘ 𝑄 ) = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )
12	8 9 10 11	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ‘ 𝑄 ) = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )
13		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14		simpl2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
15		simpl3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
16		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 )
17	1 2 3 4 5 6 7	cdlemc5	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝐹 ‘ 𝑄 ) = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )
18	13 14 15 16 17	syl112anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝐹 ‘ 𝑄 ) = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )
19	12 18	pm2.61dane	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ¬ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) → ( 𝐹 ‘ 𝑄 ) = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) ) )