trlcone - Mathbox for Norm Megill

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

Theorem trlcone 41765

Description: If two translations have different traces, the trace of their composition is also different. (Contributed by NM, 14-Jun-2013.)

**Hypotheses**
Ref	Expression
trlcone.b	⊢ 𝐵 = (Base‘𝐾)
trlcone.h	⊢ 𝐻 = (LHyp‘𝐾)
trlcone.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
trlcone.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
trlcone	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))

**Proof of Theorem trlcone**
Step	Hyp	Ref	Expression
1		simpl3l 1247	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝐹) ≠ (𝑅‘𝐺))
2		simp11 1222	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3		simp12l 1305	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐹 ∈ 𝑇)
4		trlcone.h	. . . . . . . . . . 11 ⊢ 𝐻 = (LHyp‘𝐾)
5		trlcone.t	. . . . . . . . . . 11 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
6	4, 5	ltrncnv 41183	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
7	2, 3, 6	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ^◡𝐹 ∈ 𝑇)
8		simp12r 1306	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺 ∈ 𝑇)
9	4, 5	ltrnco 41756	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ 𝐺) ∈ 𝑇)
10	2, 3, 8, 9	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝐹 ∘ 𝐺) ∈ 𝑇)
11		eqid 2761	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
12		eqid 2761	. . . . . . . . . 10 ⊢ (join‘𝐾) = (join‘𝐾)
13		trlcone.r	. . . . . . . . . 10 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
14	11, 12, 4, 5, 13	trlco 41764	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ^◡𝐹 ∈ 𝑇 ∧ (𝐹 ∘ 𝐺) ∈ 𝑇) → (𝑅‘(^◡𝐹 ∘ (𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
15	2, 7, 10, 14	syl3anc 1398	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘(^◡𝐹 ∘ (𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
16		trlcone.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝐾)
17	16, 4, 5	ltrn1o 41161	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
18	2, 3, 17	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐹:𝐵–1-1-onto→𝐵)
19		f1ococnv1 6852	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵–1-1-onto→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵))
20	18, 19	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵))
21	20	coeq1d 5839	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((^◡𝐹 ∘ 𝐹) ∘ 𝐺) = (( I ↾ 𝐵) ∘ 𝐺))
22	16, 4, 5	ltrn1o 41161	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → 𝐺:𝐵–1-1-onto→𝐵)
23	2, 8, 22	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺:𝐵–1-1-onto→𝐵)
24		f1of 6822	. . . . . . . . . . . 12 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵⟶𝐵)
25		fcoi2 6755	. . . . . . . . . . . 12 ⊢ (𝐺:𝐵⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐺) = 𝐺)
26	23, 24, 25	3syl 19	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (( I ↾ 𝐵) ∘ 𝐺) = 𝐺)
27	21, 26	eqtrd 2796	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((^◡𝐹 ∘ 𝐹) ∘ 𝐺) = 𝐺)
28		coass 6266	. . . . . . . . . 10 ⊢ ((^◡𝐹 ∘ 𝐹) ∘ 𝐺) = (^◡𝐹 ∘ (𝐹 ∘ 𝐺))
29	27, 28	eqtr3di 2811	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺 = (^◡𝐹 ∘ (𝐹 ∘ 𝐺)))
30	29	fveq2d 6887	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺) = (𝑅‘(^◡𝐹 ∘ (𝐹 ∘ 𝐺))))
31		simp11l 1303	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐾 ∈ HL)
32		simp2 1155	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) ∈ (Atoms‘𝐾))
33		eqid 2761	. . . . . . . . . . 11 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
34	12, 33	hlatjidm 40406	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐹)(join‘𝐾)(𝑅‘𝐹)) = (𝑅‘𝐹))
35	31, 32, 34	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((𝑅‘𝐹)(join‘𝐾)(𝑅‘𝐹)) = (𝑅‘𝐹))
36	4, 5, 13	trlcnv 41202	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
37	2, 3, 36	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
38	37	eqcomd 2767	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = (𝑅‘^◡𝐹))
39		simp3 1156	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺)))
40	38, 39	oveq12d 7436	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((𝑅‘𝐹)(join‘𝐾)(𝑅‘𝐹)) = ((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
41	35, 40	eqtr3d 2798	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = ((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
42	15, 30, 41	3brtr4d 5137	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺)(le‘𝐾)(𝑅‘𝐹))
43		hlatl 40397	. . . . . . . . 9 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
44	31, 43	syl 18	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐾 ∈ AtLat)
45		simp13r 1308	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺 ≠ ( I ↾ 𝐵))
46	16, 33, 4, 5, 13	trlnidat 41210	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐺) ∈ (Atoms‘𝐾))
47	2, 8, 45, 46	syl3anc 1398	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺) ∈ (Atoms‘𝐾))
48	11, 33	atcmp 40348	. . . . . . . 8 ⊢ ((𝐾 ∈ AtLat ∧ (𝑅‘𝐺) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐺)(le‘𝐾)(𝑅‘𝐹) ↔ (𝑅‘𝐺) = (𝑅‘𝐹)))
49	44, 47, 32, 48	syl3anc 1398	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((𝑅‘𝐺)(le‘𝐾)(𝑅‘𝐹) ↔ (𝑅‘𝐺) = (𝑅‘𝐹)))
50	42, 49	mpbid 235	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺) = (𝑅‘𝐹))
51	50	eqcomd 2767	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = (𝑅‘𝐺))
52	51	3expia 1139	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺)) → (𝑅‘𝐹) = (𝑅‘𝐺)))
53	52	necon3d 2977	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐹) ≠ (𝑅‘𝐺) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺))))
54	1, 53	mpd 16	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))
55		simpl3r 1248	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐺 ≠ ( I ↾ 𝐵))
56		simpl1 1210	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
57		simpl2r 1246	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐺 ∈ 𝑇)
58		eqid 2761	. . . . . . . 8 ⊢ (0.‘𝐾) = (0.‘𝐾)
59	16, 58, 4, 5, 13	trlid0b 41215	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝐺 = ( I ↾ 𝐵) ↔ (𝑅‘𝐺) = (0.‘𝐾)))
60	56, 57, 59	syl2anc 596	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐺 = ( I ↾ 𝐵) ↔ (𝑅‘𝐺) = (0.‘𝐾)))
61	60	necon3bid 3000	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐺 ≠ ( I ↾ 𝐵) ↔ (𝑅‘𝐺) ≠ (0.‘𝐾)))
62	55, 61	mpbid 235	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝐺) ≠ (0.‘𝐾))
63	62	necomd 3011	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (0.‘𝐾) ≠ (𝑅‘𝐺))
64		simpr 490	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝐹) = (0.‘𝐾))
65		simpl2l 1245	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐹 ∈ 𝑇)
66	16, 58, 4, 5, 13	trlid0b 41215	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐹 = ( I ↾ 𝐵) ↔ (𝑅‘𝐹) = (0.‘𝐾)))
67	56, 65, 66	syl2anc 596	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐹 = ( I ↾ 𝐵) ↔ (𝑅‘𝐹) = (0.‘𝐾)))
68	64, 67	mpbird 260	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐹 = ( I ↾ 𝐵))
69	68	coeq1d 5839	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐹 ∘ 𝐺) = (( I ↾ 𝐵) ∘ 𝐺))
70	56, 57, 22	syl2anc 596	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐺:𝐵–1-1-onto→𝐵)
71	70, 24, 25	3syl 19	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (( I ↾ 𝐵) ∘ 𝐺) = 𝐺)
72	69, 71	eqtrd 2796	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐹 ∘ 𝐺) = 𝐺)
73	72	fveq2d 6887	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘(𝐹 ∘ 𝐺)) = (𝑅‘𝐺))
74	63, 64, 73	3netr4d 3033	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))
75		simp1 1154	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
76		simp2l 1218	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → 𝐹 ∈ 𝑇)
77	58, 33, 4, 5, 13	trlator0 41208	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅‘𝐹) = (0.‘𝐾)))
78	75, 76, 77	syl2anc 596	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅‘𝐹) = (0.‘𝐾)))
79	54, 74, 78	mpjaodan 973	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 class class class wbr 5103 I cid 5545 ^◡ccnv 5650 ↾ cres 5653 ∘ ccom 5655 ⟶wf 6533 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7418 Basecbs 17380 lecple 17428 joincjn 18478 0.cp0 18588 Atomscatm 40300 AtLatcal 40301 HLchlt 40387 LHypclh 41021 LTrncltrn 41138 trLctrl 41195

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-riotaBAD 39990

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-1st 7999 df-2nd 8000 df-undef 8283 df-map 8842 df-proset 18461 df-poset 18480 df-plt 18495 df-lub 18511 df-glb 18512 df-join 18513 df-meet 18514 df-p0 18590 df-p1 18591 df-lat 18599 df-clat 18666 df-oposet 40213 df-ol 40215 df-oml 40216 df-covers 40303 df-ats 40304 df-atl 40335 df-cvlat 40359 df-hlat 40388 df-llines 40535 df-lplanes 40536 df-lvols 40537 df-lines 40538 df-psubsp 40540 df-pmap 40541 df-padd 40833 df-lhyp 41025 df-laut 41026 df-ldil 41141 df-ltrn 41142 df-trl 41196

This theorem is used by: trljco 41777 cdlemh2 41853 cdlemh 41854 cdlemk3 41870 cdlemk12 41887 cdlemk12u 41909 cdlemkfid1N 41958 cdlemk54 41995

W3C validator