trljco - Mathbox for Norm Megill

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

Theorem trljco 38352

Description: Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013.)

**Hypotheses**
Ref	Expression
trljco.j	⊢ ∨ = (join‘𝐾)
trljco.h	⊢ 𝐻 = (LHyp‘𝐾)
trljco.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
trljco.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
trljco	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))

**Proof of Theorem trljco**
Step	Hyp	Ref	Expression
1		coeq1 5704	. . . . 5 ⊢ (𝐹 = ( I ↾ (Base‘𝐾)) → (𝐹 ∘ 𝐺) = (( I ↾ (Base‘𝐾)) ∘ 𝐺))
2		eqid 2759	. . . . . . . 8 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		trljco.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
4		trljco.t	. . . . . . . 8 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
5	2, 3, 4	ltrn1o 37736	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
6	5	3adant2 1129	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
7		f1of 6608	. . . . . 6 ⊢ (𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾) → 𝐺:(Base‘𝐾)⟶(Base‘𝐾))
8		fcoi2 6544	. . . . . 6 ⊢ (𝐺:(Base‘𝐾)⟶(Base‘𝐾) → (( I ↾ (Base‘𝐾)) ∘ 𝐺) = 𝐺)
9	6, 7, 8	3syl 18	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (( I ↾ (Base‘𝐾)) ∘ 𝐺) = 𝐺)
10	1, 9	sylan9eqr 2816	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐹 = ( I ↾ (Base‘𝐾))) → (𝐹 ∘ 𝐺) = 𝐺)
11	10	fveq2d 6668	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐹 = ( I ↾ (Base‘𝐾))) → (𝑅‘(𝐹 ∘ 𝐺)) = (𝑅‘𝐺))
12	11	oveq2d 7173	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐹 = ( I ↾ (Base‘𝐾))) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
13		simp1l 1195	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐾 ∈ HL)
14	13	hllatd 36976	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐾 ∈ Lat)
15		trljco.r	. . . . . . . 8 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
16	2, 3, 4, 15	trlcl 37776	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ∈ (Base‘𝐾))
17	16	3adant3 1130	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐹) ∈ (Base‘𝐾))
18		trljco.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
19	2, 18	latjidm 17765	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝐹) ∈ (Base‘𝐾)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹)) = (𝑅‘𝐹))
20	14, 17, 19	syl2anc 587	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹)) = (𝑅‘𝐹))
21		hlol 36973	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
22	13, 21	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐾 ∈ OL)
23		eqid 2759	. . . . . . 7 ⊢ (0.‘𝐾) = (0.‘𝐾)
24	2, 18, 23	olj01 36837	. . . . . 6 ⊢ ((𝐾 ∈ OL ∧ (𝑅‘𝐹) ∈ (Base‘𝐾)) → ((𝑅‘𝐹) ∨ (0.‘𝐾)) = (𝑅‘𝐹))
25	22, 17, 24	syl2anc 587	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (0.‘𝐾)) = (𝑅‘𝐹))
26	20, 25	eqtr4d 2797	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹)) = ((𝑅‘𝐹) ∨ (0.‘𝐾)))
27	26	adantr 484	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹)) = ((𝑅‘𝐹) ∨ (0.‘𝐾)))
28		coeq2 5705	. . . . . 6 ⊢ (𝐺 = ( I ↾ (Base‘𝐾)) → (𝐹 ∘ 𝐺) = (𝐹 ∘ ( I ↾ (Base‘𝐾))))
29	2, 3, 4	ltrn1o 37736	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
30	29	3adant3 1130	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
31		f1of 6608	. . . . . . 7 ⊢ (𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) → 𝐹:(Base‘𝐾)⟶(Base‘𝐾))
32		fcoi1 6543	. . . . . . 7 ⊢ (𝐹:(Base‘𝐾)⟶(Base‘𝐾) → (𝐹 ∘ ( I ↾ (Base‘𝐾))) = 𝐹)
33	30, 31, 32	3syl 18	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ ( I ↾ (Base‘𝐾))) = 𝐹)
34	28, 33	sylan9eqr 2816	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → (𝐹 ∘ 𝐺) = 𝐹)
35	34	fveq2d 6668	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → (𝑅‘(𝐹 ∘ 𝐺)) = (𝑅‘𝐹))
36	35	oveq2d 7173	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐹)))
37	2, 23, 3, 4, 15	trlid0b 37790	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝐺 = ( I ↾ (Base‘𝐾)) ↔ (𝑅‘𝐺) = (0.‘𝐾)))
38	37	3adant2 1129	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐺 = ( I ↾ (Base‘𝐾)) ↔ (𝑅‘𝐺) = (0.‘𝐾)))
39	38	biimpa 480	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → (𝑅‘𝐺) = (0.‘𝐾))
40	39	oveq2d 7173	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) = ((𝑅‘𝐹) ∨ (0.‘𝐾)))
41	27, 36, 40	3eqtr4d 2804	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
42		eqid 2759	. . 3 ⊢ (le‘𝐾) = (le‘𝐾)
43	14	adantr 484	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → 𝐾 ∈ Lat)
44		simp1 1134	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
45	3, 4	ltrnco 38331	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ 𝐺) ∈ 𝑇)
46	2, 3, 4, 15	trlcl 37776	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∘ 𝐺) ∈ 𝑇) → (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Base‘𝐾))
47	44, 45, 46	syl2anc 587	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Base‘𝐾))
48	2, 18	latjcl 17742	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Base‘𝐾)) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) ∈ (Base‘𝐾))
49	14, 17, 47, 48	syl3anc 1369	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) ∈ (Base‘𝐾))
50	49	adantr 484	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) ∈ (Base‘𝐾))
51	2, 3, 4, 15	trlcl 37776	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ∈ (Base‘𝐾))
52	51	3adant2 1129	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ∈ (Base‘𝐾))
53	2, 18	latjcl 17742	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑅‘𝐺) ∈ (Base‘𝐾)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∈ (Base‘𝐾))
54	14, 17, 52, 53	syl3anc 1369	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∈ (Base‘𝐾))
55	54	adantr 484	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∈ (Base‘𝐾))
56	2, 42, 18	latlej1 17751	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑅‘𝐺) ∈ (Base‘𝐾)) → (𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
57	14, 17, 52, 56	syl3anc 1369	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
58	42, 18, 3, 4, 15	trlco 38339	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘(𝐹 ∘ 𝐺))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
59	2, 42, 18	latjle12 17753	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Base‘𝐾) ∧ ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∈ (Base‘𝐾))) → (((𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∧ (𝑅‘(𝐹 ∘ 𝐺))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺))) ↔ ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺))))
60	14, 17, 47, 54, 59	syl13anc 1370	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (((𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∧ (𝑅‘(𝐹 ∘ 𝐺))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺))) ↔ ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺))))
61	57, 58, 60	mpbi2and 711	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
62	61	adantr 484	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
63		simpr 488	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → (𝑅‘𝐹) = (𝑅‘𝐺))
64	63	oveq2d 7173	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹)) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
65	2, 42, 18	latlej1 17751	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Base‘𝐾)) → (𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
66	14, 17, 47, 65	syl3anc 1369	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
67	20, 66	eqbrtrd 5059	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
68	67	adantr 484	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
69	64, 68	eqbrtrrd 5061	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
70	2, 42, 43, 50, 55, 62, 69	latasymd 17748	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
71	61	adantr 484	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
72		simpl1l 1222	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ HL)
73		simpl1 1189	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
74		simpl2 1190	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ∈ 𝑇)
75		simpr1 1192	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ≠ ( I ↾ (Base‘𝐾)))
76		eqid 2759	. . . . . 6 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
77	2, 76, 3, 4, 15	trlnidat 37785	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ (Base‘𝐾))) → (𝑅‘𝐹) ∈ (Atoms‘𝐾))
78	73, 74, 75, 77	syl3anc 1369	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐹) ∈ (Atoms‘𝐾))
79		simpl3 1191	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ∈ 𝑇)
80	74, 79	jca 515	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇))
81		simpr3 1194	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐹) ≠ (𝑅‘𝐺))
82	76, 3, 4, 15	trlcoat 38335	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Atoms‘𝐾))
83	73, 80, 81, 82	syl3anc 1369	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Atoms‘𝐾))
84		simpr2 1193	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ≠ ( I ↾ (Base‘𝐾)))
85	2, 3, 4, 15	trlcone 38340	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)))) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))
86	73, 80, 81, 84, 85	syl112anc 1372	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))
87	2, 76, 3, 4, 15	trlnidat 37785	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾))) → (𝑅‘𝐺) ∈ (Atoms‘𝐾))
88	73, 79, 84, 87	syl3anc 1369	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ∈ (Atoms‘𝐾))
89	42, 18, 76	ps-1 37089	. . . 4 ⊢ ((𝐾 ∈ HL ∧ ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺))) ∧ ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐺) ∈ (Atoms‘𝐾))) → (((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ↔ ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺))))
90	72, 78, 83, 86, 78, 88, 89	syl132anc 1386	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ↔ ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺))))
91	71, 90	mpbid 235	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
92	12, 41, 70, 91	pm2.61da3ne 3041	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1085 = wceq 1539 ∈ wcel 2112 ≠ wne 2952 class class class wbr 5037 I cid 5434 ↾ cres 5531 ∘ ccom 5533 ⟶wf 6337 –1-1-onto→wf1o 6340 ‘cfv 6341 (class class class)co 7157 Basecbs 16556 lecple 16645 joincjn 17635 0.cp0 17728 Latclat 17736 OLcol 36786 Atomscatm 36875 HLchlt 36962 LHypclh 37596 LTrncltrn 37713 trLctrl 37770

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5161 ax-sep 5174 ax-nul 5181 ax-pow 5239 ax-pr 5303 ax-un 7466 ax-riotaBAD 36565

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-ral 3076 df-rex 3077 df-reu 3078 df-rmo 3079 df-rab 3080 df-v 3412 df-sbc 3700 df-csb 3809 df-dif 3864 df-un 3866 df-in 3868 df-ss 3878 df-nul 4229 df-if 4425 df-pw 4500 df-sn 4527 df-pr 4529 df-op 4533 df-uni 4803 df-iun 4889 df-iin 4890 df-br 5038 df-opab 5100 df-mpt 5118 df-id 5435 df-xp 5535 df-rel 5536 df-cnv 5537 df-co 5538 df-dm 5539 df-rn 5540 df-res 5541 df-ima 5542 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-riota 7115 df-ov 7160 df-oprab 7161 df-mpo 7162 df-1st 7700 df-2nd 7701 df-undef 7956 df-map 8425 df-proset 17619 df-poset 17637 df-plt 17649 df-lub 17665 df-glb 17666 df-join 17667 df-meet 17668 df-p0 17730 df-p1 17731 df-lat 17737 df-clat 17799 df-oposet 36788 df-ol 36790 df-oml 36791 df-covers 36878 df-ats 36879 df-atl 36910 df-cvlat 36934 df-hlat 36963 df-llines 37110 df-lplanes 37111 df-lvols 37112 df-lines 37113 df-psubsp 37115 df-pmap 37116 df-padd 37408 df-lhyp 37600 df-laut 37601 df-ldil 37716 df-ltrn 37717 df-trl 37771

This theorem is referenced by: trljco2 38353 cdlemkid1 38534

W3C validator