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 41381

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 1152	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp2r 1217	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
3		simp2l 1216	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
4		trlcoabs.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
5		trlcoabs.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
6	4, 5	ltrncnv 40805	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
7	1, 3, 6	syl2anc 595	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ^◡𝐹 ∈ 𝑇)
8	4, 5	ltrnco 41378	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
9	1, 2, 7, 8	syl3anc 1396	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
10		trlcoabs.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
11		trlcoabs.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
12	10, 11, 4, 5	ltrnel 40798	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
13	12	3adant2r 1196	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
14		trlcoabs.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
15		eqid 2769	. . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾)
16		trlcoabs.r	. . . . 5 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
17	10, 14, 15, 11, 4, 5, 16	trlval2 40822	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇 ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) = (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)𝑊))
18	1, 9, 13, 17	syl3anc 1396	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) = (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)𝑊))
19	18	oveq2d 7424	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ((𝐹‘𝑃) ∨ (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)𝑊)))
20		simp1l 1214	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL)
21		simp3l 1218	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
22	10, 11, 4, 5	ltrnat 40799	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴)
23	1, 3, 21, 22	syl3anc 1396	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ 𝐴)
24	10, 11, 4, 5	ltrnat 40799	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇 ∧ (𝐹‘𝑃) ∈ 𝐴) → ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)) ∈ 𝐴)
25	1, 9, 23, 24	syl3anc 1396	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)) ∈ 𝐴)
26		eqid 2769	. . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾)
27	26, 14, 11	hlatjcl 40026	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)) ∈ 𝐴) → ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∈ (Base‘𝐾))
28	20, 23, 25, 27	syl3anc 1396	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∈ (Base‘𝐾))
29		simp1r 1215	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
30	26, 4	lhpbase 40657	. . . 4 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
31	29, 30	syl 18	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾))
32	10, 14, 11	hlatlej1 40034	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)) ∈ 𝐴) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))))
33	20, 23, 25, 32	syl3anc 1396	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))))
34	26, 10, 14, 15, 11	atmod3i1 40523	. . 3 ⊢ ((𝐾 ∈ HL ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))) → ((𝐹‘𝑃) ∨ (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)𝑊)) = (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)((𝐹‘𝑃) ∨ 𝑊)))
35	20, 23, 28, 31, 33, 34	syl131anc 1408	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)𝑊)) = (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)((𝐹‘𝑃) ∨ 𝑊)))
36	10, 11, 4, 5	ltrncoval 40804	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐺 ∘ ^◡𝐹) ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (((𝐺 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃) = ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))
37	1, 9, 3, 21, 36	syl121anc 1400	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃) = ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))
38		coass 6264	. . . . . . . 8 ⊢ ((𝐺 ∘ ^◡𝐹) ∘ 𝐹) = (𝐺 ∘ (^◡𝐹 ∘ 𝐹))
39	26, 4, 5	ltrn1o 40783	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
40	1, 3, 39	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
41		f1ococnv1 6848	. . . . . . . . . . 11 ⊢ (𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) → (^◡𝐹 ∘ 𝐹) = ( I ↾ (Base‘𝐾)))
42	40, 41	syl 18	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (^◡𝐹 ∘ 𝐹) = ( I ↾ (Base‘𝐾)))
43	42	coeq2d 5846	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ (^◡𝐹 ∘ 𝐹)) = (𝐺 ∘ ( I ↾ (Base‘𝐾))))
44	26, 4, 5	ltrn1o 40783	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
45	1, 2, 44	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
46		f1of 6818	. . . . . . . . . 10 ⊢ (𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾) → 𝐺:(Base‘𝐾)⟶(Base‘𝐾))
47		fcoi1 6750	. . . . . . . . . 10 ⊢ (𝐺:(Base‘𝐾)⟶(Base‘𝐾) → (𝐺 ∘ ( I ↾ (Base‘𝐾))) = 𝐺)
48	45, 46, 47	3syl 19	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ ( I ↾ (Base‘𝐾))) = 𝐺)
49	43, 48	eqtrd 2804	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ (^◡𝐹 ∘ 𝐹)) = 𝐺)
50	38, 49	eqtrid 2816	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺 ∘ ^◡𝐹) ∘ 𝐹) = 𝐺)
51	50	fveq1d 6881	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃) = (𝐺‘𝑃))
52	37, 51	eqtr3d 2806	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)) = (𝐺‘𝑃))
53	52	oveq2d 7424	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃))) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))
54		eqid 2769	. . . . . 6 ⊢ (1.‘𝐾) = (1.‘𝐾)
55	10, 14, 54, 11, 4	lhpjat2 40680	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → ((𝐹‘𝑃) ∨ 𝑊) = (1.‘𝐾))
56	1, 13, 55	syl2anc 595	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ 𝑊) = (1.‘𝐾))
57	53, 56	oveq12d 7426	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)((𝐹‘𝑃) ∨ 𝑊)) = (((𝐹‘𝑃) ∨ (𝐺‘𝑃))(meet‘𝐾)(1.‘𝐾)))
58		hlol 40020	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
59	20, 58	syl 18	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ OL)
60	10, 11, 4, 5	ltrnat 40799	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐴)
61	1, 2, 21, 60	syl3anc 1396	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺‘𝑃) ∈ 𝐴)
62	26, 14, 11	hlatjcl 40026	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ (𝐺‘𝑃) ∈ 𝐴) → ((𝐹‘𝑃) ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾))
63	20, 23, 61, 62	syl3anc 1396	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾))
64	26, 15, 54	olm11 39886	. . . 4 ⊢ ((𝐾 ∈ OL ∧ ((𝐹‘𝑃) ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾)) → (((𝐹‘𝑃) ∨ (𝐺‘𝑃))(meet‘𝐾)(1.‘𝐾)) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))
65	59, 63, 64	syl2anc 595	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ (𝐺‘𝑃))(meet‘𝐾)(1.‘𝐾)) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))
66	57, 65	eqtrd 2804	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ ((𝐺 ∘ ^◡𝐹)‘(𝐹‘𝑃)))(meet‘𝐾)((𝐹‘𝑃) ∨ 𝑊)) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))
67	19, 35, 66	3eqtrd 2808	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 class class class wbr 5110 I cid 5553 ^◡ccnv 5658 ↾ cres 5661 ∘ ccom 5663 ⟶wf 6529 –1-1-onto→wf1o 6532 ‘cfv 6533 (class class class)co 7408 Basecbs 17265 lecple 17313 joincjn 18363 meetcmee 18364 1.cp1 18474 OLcol 39833 Atomscatm 39922 HLchlt 40009 LHypclh 40643 LTrncltrn 40760 trLctrl 40817

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-riotaBAD 39612

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-iun 4959 df-iin 4960 df-br 5111 df-opab 5175 df-mpt 5194 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-1st 7982 df-2nd 7983 df-undef 8265 df-map 8822 df-proset 18346 df-poset 18365 df-plt 18380 df-lub 18396 df-glb 18397 df-join 18398 df-meet 18399 df-p0 18475 df-p1 18476 df-lat 18484 df-clat 18551 df-oposet 39835 df-ol 39837 df-oml 39838 df-covers 39925 df-ats 39926 df-atl 39957 df-cvlat 39981 df-hlat 40010 df-llines 40157 df-lplanes 40158 df-lvols 40159 df-lines 40160 df-psubsp 40162 df-pmap 40163 df-padd 40455 df-lhyp 40647 df-laut 40648 df-ldil 40763 df-ltrn 40764 df-trl 40818

This theorem is referenced by: cdlemkfid1N 41580

W3C validator