trlcoabs2N - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > trlcoabs2N		Structured version Visualization version GIF version

Theorem trlcoabs2N 41873

Description: Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
trlcoabs.l	⊢ ≤ = (le‘𝐾)
trlcoabs.j	⊢ ∨ = (join‘𝐾)
trlcoabs.a	⊢ 𝐴 = (Atoms‘𝐾)
trlcoabs.h	⊢ 𝐻 = (LHyp‘𝐾)
trlcoabs.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
trlcoabs.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
trlcoabs2N	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))

**Proof of Theorem trlcoabs2N**
Step	Hyp	Ref	Expression
1		simp1 1154	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp2r 1219	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
3		simp2l 1218	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
4		trlcoabs.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
5		trlcoabs.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
6	4, 5	ltrncnv 41297	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
7	1, 3, 6	syl2anc 596	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ^◡𝐹 ∈ 𝑇)
8	4, 5	ltrnco 41870	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
9	1, 2, 7, 8	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
10		trlcoabs.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
11		trlcoabs.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
12	10, 11, 4, 5	ltrnel 41290	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
13	12	3adant2r 1198	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
14		trlcoabs.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
15		eqid 2760	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
16		trlcoabs.r	. . . . 5 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
17	10, 14, 15, 11, 4, 5, 16	trlval2 41314	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇 ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) = (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)𝑊))
18	1, 9, 13, 17	syl3anc 1398	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) = (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)𝑊))
19	18	oveq2d 7437	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ((𝐹‘𝑃) ∨ (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)𝑊)))
20		simp1l 1216	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL)
21		simp3l 1220	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
22	10, 11, 4, 5	ltrnat 41291	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴)
23	1, 3, 21, 22	syl3anc 1398	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ 𝐴)
24	10, 11, 4, 5	ltrnat 41291	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇 ∧ (𝐹‘𝑃) ∈ 𝐴) → ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)) ∈ 𝐴)
25	1, 9, 23, 24	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)) ∈ 𝐴)
26		eqid 2760	. . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾)
27	26, 14, 11	hlatjcl 40518	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)) ∈ 𝐴) → ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∈ (Base‘𝐾))
28	20, 23, 25, 27	syl3anc 1398	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∈ (Base‘𝐾))
29		simp1r 1217	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
30	26, 4	lhpbase 41149	. . . 4 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
31	29, 30	syl 18	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾))
32	10, 14, 11	hlatlej1 40526	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)) ∈ 𝐴) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))))
33	20, 23, 25, 32	syl3anc 1398	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))))
34	26, 10, 14, 15, 11	atmod3i1 41015	. . 3 ⊢ ((𝐾 ∈ HL ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))) → ((𝐹‘𝑃) ∨ (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)𝑊)) = (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)((𝐹‘𝑃) ∨ 𝑊)))
35	20, 23, 28, 31, 33, 34	syl131anc 1410	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)𝑊)) = (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)((𝐹‘𝑃) ∨ 𝑊)))
36	10, 11, 4, 5	ltrncoval 41296	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺 ∘ ^◡𝐹) ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (((𝐺 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃) = ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))
37	1, 9, 3, 21, 36	syl121anc 1402	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃) = ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))
38		coass 6267	. . . . . . . 8 ⊢ ((𝐺 ∘ ^◡𝐹) ∘ 𝐹) = (𝐺 ∘ (^◡𝐹 ∘ 𝐹))
39	26, 4, 5	ltrn1o 41275	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
40	1, 3, 39	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
41		f1ococnv1 6855	. . . . . . . . . . 11 ⊢ (𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) → (^◡𝐹 ∘ 𝐹) = ( I ↾ (Base‘𝐾)))
42	40, 41	syl 18	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (^◡𝐹 ∘ 𝐹) = ( I ↾ (Base‘𝐾)))
43	42	coeq2d 5839	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ (^◡𝐹 ∘ 𝐹)) = (𝐺 ∘ ( I ↾ (Base‘𝐾))))
44	26, 4, 5	ltrn1o 41275	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
45	1, 2, 44	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
46		f1of 6825	. . . . . . . . . 10 ⊢ (𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾) → 𝐺:(Base‘𝐾)⟶(Base‘𝐾))
47		fcoi1 6757	. . . . . . . . . 10 ⊢ (𝐺:(Base‘𝐾)⟶(Base‘𝐾) → (𝐺 ∘ ( I ↾ (Base‘𝐾))) = 𝐺)
48	45, 46, 47	3syl 19	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ ( I ↾ (Base‘𝐾))) = 𝐺)
49	43, 48	eqtrd 2795	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ (^◡𝐹 ∘ 𝐹)) = 𝐺)
50	38, 49	eqtrid 2807	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺 ∘ ^◡𝐹) ∘ 𝐹) = 𝐺)
51	50	fveq1d 6888	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃) = (𝐺‘𝑃))
52	37, 51	eqtr3d 2797	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)) = (𝐺‘𝑃))
53	52	oveq2d 7437	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))
54		eqid 2760	. . . . . 6 ⊢ (1.‘𝐾) = (1.‘𝐾)
55	10, 14, 54, 11, 4	lhpjat2 41172	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → ((𝐹‘𝑃) ∨ 𝑊) = (1.‘𝐾))
56	1, 13, 55	syl2anc 596	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ 𝑊) = (1.‘𝐾))
57	53, 56	oveq12d 7439	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)((𝐹‘𝑃) ∨ 𝑊)) = (((𝐹‘𝑃) ∨ (𝐺‘𝑃))(meet‘𝐾)(1.‘𝐾)))
58		hlol 40512	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
59	20, 58	syl 18	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ OL)
60	10, 11, 4, 5	ltrnat 41291	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐴)
61	1, 2, 21, 60	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺‘𝑃) ∈ 𝐴)
62	26, 14, 11	hlatjcl 40518	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ (𝐺‘𝑃) ∈ 𝐴) → ((𝐹‘𝑃) ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾))
63	20, 23, 61, 62	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾))
64	26, 15, 54	olm11 40378	. . . 4 ⊢ ((𝐾 ∈ OL ∧ ((𝐹‘𝑃) ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾)) → (((𝐹‘𝑃) ∨ (𝐺‘𝑃))(meet‘𝐾)(1.‘𝐾)) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))
65	59, 63, 64	syl2anc 596	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ (𝐺‘𝑃))(meet‘𝐾)(1.‘𝐾)) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))
66	57, 65	eqtrd 2795	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)((𝐹‘𝑃) ∨ 𝑊)) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))
67	19, 35, 66	3eqtrd 2799	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 class class class wbr 5102 I cid 5544 ^◡ccnv 5649 ↾ cres 5652 ∘ ccom 5654 ⟶wf 6535 –1-1-onto→wf1o 6538 ‘cfv 6539 (class class class)co 7421 Basecbs 17393 lecple 17441 joincjn 18491 meetcmee 18492 1.cp1 18602 OLcol 40325 Atomscatm 40414 HLchlt 40501 LHypclh 41135 LTrncltrn 41252 trLctrl 41309

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-riotaBAD 40104

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-1st 8002 df-2nd 8003 df-undef 8294 df-map 8853 df-proset 18474 df-poset 18493 df-plt 18508 df-lub 18524 df-glb 18525 df-join 18526 df-meet 18527 df-p0 18603 df-p1 18604 df-lat 18612 df-clat 18679 df-oposet 40327 df-ol 40329 df-oml 40330 df-covers 40417 df-ats 40418 df-atl 40449 df-cvlat 40473 df-hlat 40502 df-llines 40649 df-lplanes 40650 df-lvols 40651 df-lines 40652 df-psubsp 40654 df-pmap 40655 df-padd 40947 df-lhyp 41139 df-laut 41140 df-ldil 41255 df-ltrn 41256 df-trl 41310

This theorem is used by: cdlemkfid1N 42072

W3C validator