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 41904

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 5835	. . . . 5 ⊢ (𝐹 = ( I ↾ (Base‘𝐾)) → (𝐹 ∘ 𝐺) = (( I ↾ (Base‘𝐾)) ∘ 𝐺))
2		eqid 2760	. . . . . . . 8 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		trljco.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
4		trljco.t	. . . . . . . 8 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
5	2, 3, 4	ltrn1o 41288	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
6	5	3adant2 1149	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
7		f1of 6827	. . . . . 6 ⊢ (𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾) → 𝐺:(Base‘𝐾)⟶(Base‘𝐾))
8		fcoi2 6760	. . . . . 6 ⊢ (𝐺:(Base‘𝐾)⟶(Base‘𝐾) → (( I ↾ (Base‘𝐾)) ∘ 𝐺) = 𝐺)
9	6, 7, 8	3syl 19	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (( I ↾ (Base‘𝐾)) ∘ 𝐺) = 𝐺)
10	1, 9	sylan9eqr 2817	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐹 = ( I ↾ (Base‘𝐾))) → (𝐹 ∘ 𝐺) = 𝐺)
11	10	fveq2d 6892	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐹 = ( I ↾ (Base‘𝐾))) → (𝑅‘(𝐹 ∘ 𝐺)) = (𝑅‘𝐺))
12	11	oveq2d 7438	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐹 = ( I ↾ (Base‘𝐾))) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
13		simp1l 1216	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐾 ∈ HL)
14	13	hllatd 40528	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐾 ∈ Lat)
15		trljco.r	. . . . . . . 8 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
16	2, 3, 4, 15	trlcl 41328	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ∈ (Base‘𝐾))
17	16	3adant3 1150	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐹) ∈ (Base‘𝐾))
18		trljco.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
19	2, 18	latjidm 18643	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝐹) ∈ (Base‘𝐾)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹)) = (𝑅‘𝐹))
20	14, 17, 19	syl2anc 596	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹)) = (𝑅‘𝐹))
21		hlol 40525	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
22	13, 21	syl 18	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐾 ∈ OL)
23		eqid 2760	. . . . . . 7 ⊢ (0.‘𝐾) = (0.‘𝐾)
24	2, 18, 23	olj01 40389	. . . . . 6 ⊢ ((𝐾 ∈ OL ∧ (𝑅‘𝐹) ∈ (Base‘𝐾)) → ((𝑅‘𝐹) ∨ (0.‘𝐾)) = (𝑅‘𝐹))
25	22, 17, 24	syl2anc 596	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (0.‘𝐾)) = (𝑅‘𝐹))
26	20, 25	eqtr4d 2798	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹)) = ((𝑅‘𝐹) ∨ (0.‘𝐾)))
27	26	adantr 486	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹)) = ((𝑅‘𝐹) ∨ (0.‘𝐾)))
28		coeq2 5836	. . . . . 6 ⊢ (𝐺 = ( I ↾ (Base‘𝐾)) → (𝐹 ∘ 𝐺) = (𝐹 ∘ ( I ↾ (Base‘𝐾))))
29	2, 3, 4	ltrn1o 41288	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
30	29	3adant3 1150	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
31		f1of 6827	. . . . . . 7 ⊢ (𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) → 𝐹:(Base‘𝐾)⟶(Base‘𝐾))
32		fcoi1 6759	. . . . . . 7 ⊢ (𝐹:(Base‘𝐾)⟶(Base‘𝐾) → (𝐹 ∘ ( I ↾ (Base‘𝐾))) = 𝐹)
33	30, 31, 32	3syl 19	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ ( I ↾ (Base‘𝐾))) = 𝐹)
34	28, 33	sylan9eqr 2817	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → (𝐹 ∘ 𝐺) = 𝐹)
35	34	fveq2d 6892	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → (𝑅‘(𝐹 ∘ 𝐺)) = (𝑅‘𝐹))
36	35	oveq2d 7438	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐹)))
37	2, 23, 3, 4, 15	trlid0b 41342	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝐺 = ( I ↾ (Base‘𝐾)) ↔ (𝑅‘𝐺) = (0.‘𝐾)))
38	37	3adant2 1149	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐺 = ( I ↾ (Base‘𝐾)) ↔ (𝑅‘𝐺) = (0.‘𝐾)))
39	38	biimpa 482	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → (𝑅‘𝐺) = (0.‘𝐾))
40	39	oveq2d 7438	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) = ((𝑅‘𝐹) ∨ (0.‘𝐾)))
41	27, 36, 40	3eqtr4d 2805	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐺 = ( I ↾ (Base‘𝐾))) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
42		eqid 2760	. . 3 ⊢ (le‘𝐾) = (le‘𝐾)
43	14	adantr 486	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → 𝐾 ∈ Lat)
44		simp1 1154	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
45	3, 4	ltrnco 41883	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ 𝐺) ∈ 𝑇)
46	2, 3, 4, 15	trlcl 41328	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∘ 𝐺) ∈ 𝑇) → (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Base‘𝐾))
47	44, 45, 46	syl2anc 596	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Base‘𝐾))
48	2, 18	latjcl 18620	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Base‘𝐾)) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) ∈ (Base‘𝐾))
49	14, 17, 47, 48	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) ∈ (Base‘𝐾))
50	49	adantr 486	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) ∈ (Base‘𝐾))
51	2, 3, 4, 15	trlcl 41328	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ∈ (Base‘𝐾))
52	51	3adant2 1149	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ∈ (Base‘𝐾))
53	2, 18	latjcl 18620	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑅‘𝐺) ∈ (Base‘𝐾)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∈ (Base‘𝐾))
54	14, 17, 52, 53	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∈ (Base‘𝐾))
55	54	adantr 486	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∈ (Base‘𝐾))
56	2, 42, 18	latlej1 18629	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑅‘𝐺) ∈ (Base‘𝐾)) → (𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
57	14, 17, 52, 56	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
58	42, 18, 3, 4, 15	trlco 41891	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘(𝐹 ∘ 𝐺))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
59	2, 42, 18	latjle12 18631	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Base‘𝐾) ∧ ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∈ (Base‘𝐾))) → (((𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∧ (𝑅‘(𝐹 ∘ 𝐺))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺))) ↔ ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺))))
60	14, 17, 47, 54, 59	syl13anc 1399	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (((𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ∧ (𝑅‘(𝐹 ∘ 𝐺))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺))) ↔ ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺))))
61	57, 58, 60	mpbi2and 725	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
62	61	adantr 486	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
63		simpr 490	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → (𝑅‘𝐹) = (𝑅‘𝐺))
64	63	oveq2d 7438	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹)) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
65	2, 42, 18	latlej1 18629	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝐹) ∈ (Base‘𝐾) ∧ (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Base‘𝐾)) → (𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
66	14, 17, 47, 65	syl3anc 1398	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐹)(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
67	20, 66	eqbrtrd 5126	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
68	67	adantr 486	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐹))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
69	64, 68	eqbrtrrd 5128	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
70	2, 42, 43, 50, 55, 62, 69	latasymd 18626	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
71	61	adantr 486	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
72		simpl1l 1243	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ HL)
73		simpl1 1210	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
74		simpl2 1211	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ∈ 𝑇)
75		simpr1 1213	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ≠ ( I ↾ (Base‘𝐾)))
76		eqid 2760	. . . . . 6 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
77	2, 76, 3, 4, 15	trlnidat 41337	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ (Base‘𝐾))) → (𝑅‘𝐹) ∈ (Atoms‘𝐾))
78	73, 74, 75, 77	syl3anc 1398	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐹) ∈ (Atoms‘𝐾))
79		simpl3 1212	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ∈ 𝑇)
80	74, 79	jca 521	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇))
81		simpr3 1215	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐹) ≠ (𝑅‘𝐺))
82	76, 3, 4, 15	trlcoat 41887	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Atoms‘𝐾))
83	73, 80, 81, 82	syl3anc 1398	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Atoms‘𝐾))
84		simpr2 1214	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ≠ ( I ↾ (Base‘𝐾)))
85	2, 3, 4, 15	trlcone 41892	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)))) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))
86	73, 80, 81, 84, 85	syl112anc 1401	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))
87	2, 76, 3, 4, 15	trlnidat 41337	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾))) → (𝑅‘𝐺) ∈ (Atoms‘𝐾))
88	73, 79, 84, 87	syl3anc 1398	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ (Base‘𝐾)) ∧ 𝐺 ≠ ( I ↾ (Base‘𝐾)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ∈ (Atoms‘𝐾))
89	42, 18, 76	ps-1 40641	. . . 4 ⊢ ((𝐾 ∈ HL ∧ ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺))) ∧ ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐺) ∈ (Atoms‘𝐾))) → (((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘𝐹) ∨ (𝑅‘𝐺)) ↔ ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺))))
90	72, 78, 83, 86, 78, 88, 89	syl132anc 1415	. . 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 3044	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 class class class wbr 5102 I cid 5544 ↾ cres 5652 ∘ ccom 5654 ⟶wf 6537 –1-1-onto→wf1o 6540 ‘cfv 6541 (class class class)co 7422 Basecbs 17394 lecple 17442 joincjn 18492 0.cp0 18602 Latclat 18612 OLcol 40338 Atomscatm 40427 HLchlt 40514 LHypclh 41148 LTrncltrn 41265 trLctrl 41322

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 7753 ax-riotaBAD 40117

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 3848 df-ss 3897 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 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 6496 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7379 df-ov 7425 df-oprab 7426 df-mpo 7427 df-1st 8003 df-2nd 8004 df-undef 8295 df-map 8854 df-proset 18475 df-poset 18494 df-plt 18509 df-lub 18525 df-glb 18526 df-join 18527 df-meet 18528 df-p0 18604 df-p1 18605 df-lat 18613 df-clat 18680 df-oposet 40340 df-ol 40342 df-oml 40343 df-covers 40430 df-ats 40431 df-atl 40462 df-cvlat 40486 df-hlat 40515 df-llines 40662 df-lplanes 40663 df-lvols 40664 df-lines 40665 df-psubsp 40667 df-pmap 40668 df-padd 40960 df-lhyp 41152 df-laut 41153 df-ldil 41268 df-ltrn 41269 df-trl 41323

This theorem is used by: trljco2 41905 cdlemkid1 42086

W3C validator