dihmeetlem1N

Description: Isomorphism H of a conjunction. (Contributed by NM, 21-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihglblem5a.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dihglblem5a.m	⊢ ∧ = ( meet ‘ 𝐾 )
	dihglblem5a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihglblem5a.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dihglblem5a.l	⊢ ≤ = ( le ‘ 𝐾 )
	dihglblem5a.j	⊢ ∨ = ( join ‘ 𝐾 )
	dihglblem5a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dihglblem5a.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
	dihglblem5a.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dihglblem5a.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	dihglblem5a.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dihglblem5a.g	⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑞 )
	dihglblem5a.o	⊢ 0 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion	dihmeetlem1N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihglblem5a.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dihglblem5a.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		dihglblem5a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dihglblem5a.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5		dihglblem5a.l	⊢ ≤ = ( le ‘ 𝐾 )
6		dihglblem5a.j	⊢ ∨ = ( join ‘ 𝐾 )
7		dihglblem5a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
8		dihglblem5a.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
9		dihglblem5a.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
10		dihglblem5a.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
11		dihglblem5a.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
12		dihglblem5a.g	⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑞 )
13		dihglblem5a.o	⊢ 0 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
14		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
15	14	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
16		simp2l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐵 )
17		simp3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → 𝑌 ∈ 𝐵 )
18	1 5 2	latmle1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
19	15 16 17 18	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
20		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21	1 2	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
22	15 16 17 21	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
23	1 5 3 4	dihord	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊆ ( 𝐼 ‘ 𝑋 ) ↔ ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ) )
24	20 22 16 23	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊆ ( 𝐼 ‘ 𝑋 ) ↔ ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ) )
25	19 24	mpbird	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊆ ( 𝐼 ‘ 𝑋 ) )
26	1 5 2	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
27	15 16 17 26	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
28	1 5 3 4	dihord	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ) )
29	20 22 17 28	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ) )
30	27 29	mpbird	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊆ ( 𝐼 ‘ 𝑌 ) )
31	25 30	ssind	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ⊆ ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
32	3 4	dihvalrel	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) )
33		relin1	⊢ ( Rel ( 𝐼 ‘ 𝑋 ) → Rel ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
34	32 33	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → Rel ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
35	34	3ad2ant1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → Rel ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )
36		elin	⊢ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) ↔ ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) )
37	1 5 6 2 7 3	lhpmcvr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
38	37	3adant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
39		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
40		simpl2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) )
41		simprl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → 𝑞 ∈ 𝐴 )
42		simprrl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ¬ 𝑞 ≤ 𝑊 )
43	41 42	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) )
44		simprrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 )
45		vex	⊢ 𝑓 ∈ V
46		vex	⊢ 𝑠 ∈ V
47	1 5 6 2 7 3 8 9 10 11 4 12 45 46	dihopelvalc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ) ) )
48	39 40 43 44 47	syl112anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ) ) )
49		simpr	⊢ ( ( ( 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ) → ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 )
50	48 49	biimtrdi	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) → ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ) )
51		simpl3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) )
52	1 5 3 9 10 13 4	dihopelvalbN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) )
53	39 51 52	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) )
54	53	biimpd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) → ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) )
55		simprll	⊢ ( ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) → 𝑓 ∈ 𝑇 )
56	55	3ad2ant3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝑓 ∈ 𝑇 )
57		simp3rr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝑠 = 0 )
58	57	fveq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑠 ‘ 𝐺 ) = ( 0 ‘ 𝐺 ) )
59		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
60	5 7 3 8	lhpocnel2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
61	59 60	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
62		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝑞 ∈ 𝐴 )
63		simp2rl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ¬ 𝑞 ≤ 𝑊 )
64	5 7 3 9 12	ltrniotacl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
65	59 61 62 63 64	syl112anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝐺 ∈ 𝑇 )
66	13 1	tendo02	⊢ ( 𝐺 ∈ 𝑇 → ( 0 ‘ 𝐺 ) = ( I ↾ 𝐵 ) )
67	65 66	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 0 ‘ 𝐺 ) = ( I ↾ 𝐵 ) )
68	58 67	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑠 ‘ 𝐺 ) = ( I ↾ 𝐵 ) )
69	68	cnveqd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ^◡ ( 𝑠 ‘ 𝐺 ) = ^◡ ( I ↾ 𝐵 ) )
70		cnvresid	⊢ ^◡ ( I ↾ 𝐵 ) = ( I ↾ 𝐵 )
71	69 70	eqtrdi	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ^◡ ( 𝑠 ‘ 𝐺 ) = ( I ↾ 𝐵 ) )
72	71	coeq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) = ( 𝑓 ∘ ( I ↾ 𝐵 ) ) )
73	1 3 9	ltrn1o	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → 𝑓 : 𝐵 –1-1-onto→ 𝐵 )
74	59 56 73	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝑓 : 𝐵 –1-1-onto→ 𝐵 )
75		f1of	⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 → 𝑓 : 𝐵 ⟶ 𝐵 )
76		fcoi1	⊢ ( 𝑓 : 𝐵 ⟶ 𝐵 → ( 𝑓 ∘ ( I ↾ 𝐵 ) ) = 𝑓 )
77	74 75 76	3syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑓 ∘ ( I ↾ 𝐵 ) ) = 𝑓 )
78	72 77	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) = 𝑓 )
79	78	fveq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) = ( 𝑅 ‘ 𝑓 ) )
80		simp3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 )
81	79 80	eqbrtrrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 )
82		simprlr	⊢ ( ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 )
83	82	3ad2ant3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 )
84		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝐾 ∈ HL )
85	84	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝐾 ∈ Lat )
86	1 3 9 10	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑅 ‘ 𝑓 ) ∈ 𝐵 )
87	59 56 86	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑅 ‘ 𝑓 ) ∈ 𝐵 )
88		simp12l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝑋 ∈ 𝐵 )
89		simp13l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝑌 ∈ 𝐵 )
90	1 5 2	latlem12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ‘ 𝑓 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ↔ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑌 ) ) )
91	85 87 88 89 90	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( ( ( 𝑅 ‘ 𝑓 ) ≤ 𝑋 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ↔ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑌 ) ) )
92	81 83 91	mpbi2and	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑌 ) )
93	56 92	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑌 ) ) )
94	85 88 89 21	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
95		simp11r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝑊 ∈ 𝐻 )
96	1 3	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
97	95 96	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝑊 ∈ 𝐵 )
98	85 88 89 26	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
99		simp13r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → 𝑌 ≤ 𝑊 )
100	1 5 85 94 89 97 98 99	lattrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 )
101	1 5 3 9 10 13 4	dihopelvalbN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑌 ) ) ∧ 𝑠 = 0 ) ) )
102	59 94 100 101	syl12anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ↔ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ ( 𝑋 ∧ 𝑌 ) ) ∧ 𝑠 = 0 ) ) )
103	93 57 102	mpbir2and	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) )
104	103	3expia	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( ( ( 𝑅 ‘ ( 𝑓 ∘ ^◡ ( 𝑠 ‘ 𝐺 ) ) ) ≤ 𝑋 ∧ ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) ≤ 𝑌 ) ∧ 𝑠 = 0 ) ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ) )
105	50 54 104	syl2and	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ) → ( ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ) )
106	38 105	rexlimddv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ∧ ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑌 ) ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ) )
107	36 106	biimtrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ⟨ 𝑓 , 𝑠 ⟩ ∈ ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) → ⟨ 𝑓 , 𝑠 ⟩ ∈ ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) ) )
108	35 107	relssdv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) ⊆ ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) )
109	31 108	eqssd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑋 ∧ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) ∩ ( 𝐼 ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem dihmeetlem1N

Proof