Theorem cdlemk21N

Description: Part of proof of Lemma K of Crawley p. 118. Lines 26-27, p. 119 for i=0 and j=1. (Contributed by NM, 5-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	⊢ 𝑂 = ( 𝑆 ‘ 𝐷 )
	cdlemk1.u	⊢ 𝑈 = ( 𝑒 ∈ 𝑇 ↦ ( ℩ 𝑗 ∈ 𝑇 ( 𝑗 ‘ 𝑃 ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝑒 ) ) ∧ ( ( 𝑂 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑒 ∘ ◡ 𝐷 ) ) ) ) ) )
Assertion	cdlemk21N	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( 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		cdlemk1.u	⊢ 𝑈 = ( 𝑒 ∈ 𝑇 ↦ ( ℩ 𝑗 ∈ 𝑇 ( 𝑗 ‘ 𝑃 ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝑒 ) ) ∧ ( ( 𝑂 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑒 ∘ ◡ 𝐷 ) ) ) ) ) )
12		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		simp21r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → 𝐺 ∈ 𝑇 )
14		simp22	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
15	2 3 5 6 7 8	trljat1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) = ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) )
16	12 13 14 15	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) = ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) )
17	10	fveq1i	⊢ ( 𝑂 ‘ 𝑃 ) = ( ( 𝑆 ‘ 𝐷 ) ‘ 𝑃 )
18	17	a1i	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝑂 ‘ 𝑃 ) = ( ( 𝑆 ‘ 𝐷 ) ‘ 𝑃 ) )
19		simp13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → 𝐷 ∈ 𝑇 )
20	6 7 8	trlcocnv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = ( 𝑅 ‘ ( 𝐷 ∘ ◡ 𝐺 ) ) )
21	12 13 19 20	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) = ( 𝑅 ‘ ( 𝐷 ∘ ◡ 𝐺 ) ) )
22	18 21	oveq12d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( ( 𝑂 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) = ( ( ( 𝑆 ‘ 𝐷 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐷 ∘ ◡ 𝐺 ) ) ) )
23	16 22	oveq12d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝑂 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ ( ( ( 𝑆 ‘ 𝐷 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐷 ∘ ◡ 𝐺 ) ) ) ) )
24		simp23	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) )
25		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → 𝐹 ∈ 𝑇 )
26		simp21l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → 𝑁 ∈ 𝑇 )
27		simp3r1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) )
28		simp3r2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) )
29	28	necomd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐺 ) )
30	27 29	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐺 ) ) )
31		simp3l1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
32		simp3l3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
33		simp3l2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → 𝐷 ≠ ( I ↾ 𝐵 ) )
34	31 32 33	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) )
35	1 2 3 4 5 6 7 8 9 10 11	cdlemkuv2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝑂 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) )
36	12 24 13 25 19 26 30 34 14 35	syl333anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝑂 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) )
37	26 19	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝑁 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) )
38		simp3r3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) )
39	38 27	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ) )
40	1 2 3 5 6 7 8 4 9	cdlemk12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) → ( ( 𝑆 ‘ 𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ ( ( ( 𝑆 ‘ 𝐷 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐷 ∘ ◡ 𝐺 ) ) ) ) )
41	12 25 13 37 14 24 34 39 28 40	syl333anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( ( 𝑆 ‘ 𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ ( ( ( 𝑆 ‘ 𝐷 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐷 ∘ ◡ 𝐺 ) ) ) ) )
42	23 36 41	3eqtr4rd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) ) → ( ( 𝑆 ‘ 𝐺 ) ‘ 𝑃 ) = ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) )