cdlemg31d

Description: Eliminate ( FP ) =/= P from cdlemg31c . TODO: Prove directly. TODO: do we need to eliminate ( FP ) =/= P ? It might be better to do this all at once at the end. See also cdlemg29 versus cdlemg28 . (Contributed by NM, 29-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemg12.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdlemg12.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdlemg12.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdlemg12.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdlemg12.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		cdlemg12b.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		cdlemg31.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑣 ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
9		simp22r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) → ¬ 𝑄 ≤ 𝑊 )
10	9	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ¬ 𝑄 ≤ 𝑊 )
11		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		simp21l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
13	12	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝑃 ∈ 𝐴 )
14		simp22l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
15	14	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝑄 ∈ 𝐴 )
16		simp23l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) → 𝑣 ∈ 𝐴 )
17	16	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝑣 ∈ 𝐴 )
18		simpl31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝐹 ∈ 𝑇 )
19	1 2 3 4 5 6 7 8	cdlemg31b	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝐹 ∈ 𝑇 ) ) → 𝑁 ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
20	11 13 15 17 18 19	syl122anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝑁 ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) )
21		simpl21	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
22		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ‘ 𝑃 ) = 𝑃 )
23		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
24	1 23 4 5 6 7	trl0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) )
25	11 21 18 22 24	syl112anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) )
26	25	oveq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑄 ∨ ( 0. ‘ 𝐾 ) ) )
27		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
28		hlol	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
29	27 28	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) → 𝐾 ∈ OL )
30	29	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝐾 ∈ OL )
31		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
32	31 4	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
33	15 32	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
34	31 2 23	olj01	⊢ ( ( 𝐾 ∈ OL ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ ( 0. ‘ 𝐾 ) ) = 𝑄 )
35	30 33 34	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝑄 ∨ ( 0. ‘ 𝐾 ) ) = 𝑄 )
36	26 35	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) = 𝑄 )
37	20 36	breqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝑁 ≤ 𝑄 )
38		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
39	27 38	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) → 𝐾 ∈ AtLat )
40	39	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝐾 ∈ AtLat )
41		simpl33	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝑁 ∈ 𝐴 )
42	1 4	atcmp	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑁 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑁 ≤ 𝑄 ↔ 𝑁 = 𝑄 ) )
43	40 41 15 42	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝑁 ≤ 𝑄 ↔ 𝑁 = 𝑄 ) )
44	37 43	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝑁 = 𝑄 )
45	44	breq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝑁 ≤ 𝑊 ↔ 𝑄 ≤ 𝑊 ) )
46	10 45	mtbird	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ¬ 𝑁 ≤ 𝑊 )
47		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
48		simpl21	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
49		simpl22	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
50		simpl23	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) )
51		simpl31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → 𝐹 ∈ 𝑇 )
52		simpl32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) )
53		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 )
54		simpl33	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → 𝑁 ∈ 𝐴 )
55	1 2 3 4 5 6 7 8	cdlemg31c	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ 𝑁 ∈ 𝐴 ) ) → ¬ 𝑁 ≤ 𝑊 )
56	47 48 49 50 51 52 53 54 55	syl323anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ¬ 𝑁 ≤ 𝑊 )
57	46 56	pm2.61dane	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑁 ∈ 𝐴 ) ) → ¬ 𝑁 ≤ 𝑊 )

Metamath Proof Explorer

Theorem cdlemg31d

Proof