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 40984

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 1229	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝐹) ≠ (𝑅‘𝐺))
2		simp11 1204	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3		simp12l 1287	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐹 ∈ 𝑇)
4		trlcone.h	. . . . . . . . . . 11 ⊢ 𝐻 = (LHyp‘𝐾)
5		trlcone.t	. . . . . . . . . . 11 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
6	4, 5	ltrncnv 40402	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
7	2, 3, 6	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ^◡𝐹 ∈ 𝑇)
8		simp12r 1288	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺 ∈ 𝑇)
9	4, 5	ltrnco 40975	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ 𝐺) ∈ 𝑇)
10	2, 3, 8, 9	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝐹 ∘ 𝐺) ∈ 𝑇)
11		eqid 2736	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
12		eqid 2736	. . . . . . . . . 10 ⊢ (join‘𝐾) = (join‘𝐾)
13		trlcone.r	. . . . . . . . . 10 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
14	11, 12, 4, 5, 13	trlco 40983	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ^◡𝐹 ∈ 𝑇 ∧ (𝐹 ∘ 𝐺) ∈ 𝑇) → (𝑅‘(^◡𝐹 ∘ (𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
15	2, 7, 10, 14	syl3anc 1373	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘(^◡𝐹 ∘ (𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
16		trlcone.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝐾)
17	16, 4, 5	ltrn1o 40380	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
18	2, 3, 17	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐹:𝐵–1-1-onto→𝐵)
19		f1ococnv1 6803	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐵–1-1-onto→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵))
20	18, 19	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵))
21	20	coeq1d 5810	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((^◡𝐹 ∘ 𝐹) ∘ 𝐺) = (( I ↾ 𝐵) ∘ 𝐺))
22	16, 4, 5	ltrn1o 40380	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → 𝐺:𝐵–1-1-onto→𝐵)
23	2, 8, 22	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺:𝐵–1-1-onto→𝐵)
24		f1of 6774	. . . . . . . . . . . 12 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵⟶𝐵)
25		fcoi2 6709	. . . . . . . . . . . 12 ⊢ (𝐺:𝐵⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐺) = 𝐺)
26	23, 24, 25	3syl 18	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (( I ↾ 𝐵) ∘ 𝐺) = 𝐺)
27	21, 26	eqtrd 2771	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((^◡𝐹 ∘ 𝐹) ∘ 𝐺) = 𝐺)
28		coass 6224	. . . . . . . . . 10 ⊢ ((^◡𝐹 ∘ 𝐹) ∘ 𝐺) = (^◡𝐹 ∘ (𝐹 ∘ 𝐺))
29	27, 28	eqtr3di 2786	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺 = (^◡𝐹 ∘ (𝐹 ∘ 𝐺)))
30	29	fveq2d 6838	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺) = (𝑅‘(^◡𝐹 ∘ (𝐹 ∘ 𝐺))))
31		simp11l 1285	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐾 ∈ HL)
32		simp2 1137	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) ∈ (Atoms‘𝐾))
33		eqid 2736	. . . . . . . . . . 11 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
34	12, 33	hlatjidm 39625	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐹)(join‘𝐾)(𝑅‘𝐹)) = (𝑅‘𝐹))
35	31, 32, 34	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((𝑅‘𝐹)(join‘𝐾)(𝑅‘𝐹)) = (𝑅‘𝐹))
36	4, 5, 13	trlcnv 40421	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
37	2, 3, 36	syl2anc 584	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
38	37	eqcomd 2742	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = (𝑅‘^◡𝐹))
39		simp3 1138	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺)))
40	38, 39	oveq12d 7376	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((𝑅‘𝐹)(join‘𝐾)(𝑅‘𝐹)) = ((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
41	35, 40	eqtr3d 2773	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = ((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
42	15, 30, 41	3brtr4d 5130	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺)(le‘𝐾)(𝑅‘𝐹))
43		hlatl 39616	. . . . . . . . 9 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
44	31, 43	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐾 ∈ AtLat)
45		simp13r 1290	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺 ≠ ( I ↾ 𝐵))
46	16, 33, 4, 5, 13	trlnidat 40429	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐺) ∈ (Atoms‘𝐾))
47	2, 8, 45, 46	syl3anc 1373	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺) ∈ (Atoms‘𝐾))
48	11, 33	atcmp 39567	. . . . . . . 8 ⊢ ((𝐾 ∈ AtLat ∧ (𝑅‘𝐺) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐺)(le‘𝐾)(𝑅‘𝐹) ↔ (𝑅‘𝐺) = (𝑅‘𝐹)))
49	44, 47, 32, 48	syl3anc 1373	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((𝑅‘𝐺)(le‘𝐾)(𝑅‘𝐹) ↔ (𝑅‘𝐺) = (𝑅‘𝐹)))
50	42, 49	mpbid 232	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺) = (𝑅‘𝐹))
51	50	eqcomd 2742	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = (𝑅‘𝐺))
52	51	3expia 1121	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺)) → (𝑅‘𝐹) = (𝑅‘𝐺)))
53	52	necon3d 2953	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐹) ≠ (𝑅‘𝐺) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺))))
54	1, 53	mpd 15	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))
55		simpl3r 1230	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐺 ≠ ( I ↾ 𝐵))
56		simpl1 1192	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
57		simpl2r 1228	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐺 ∈ 𝑇)
58		eqid 2736	. . . . . . . 8 ⊢ (0.‘𝐾) = (0.‘𝐾)
59	16, 58, 4, 5, 13	trlid0b 40434	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝐺 = ( I ↾ 𝐵) ↔ (𝑅‘𝐺) = (0.‘𝐾)))
60	56, 57, 59	syl2anc 584	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐺 = ( I ↾ 𝐵) ↔ (𝑅‘𝐺) = (0.‘𝐾)))
61	60	necon3bid 2976	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐺 ≠ ( I ↾ 𝐵) ↔ (𝑅‘𝐺) ≠ (0.‘𝐾)))
62	55, 61	mpbid 232	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝐺) ≠ (0.‘𝐾))
63	62	necomd 2987	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (0.‘𝐾) ≠ (𝑅‘𝐺))
64		simpr 484	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝐹) = (0.‘𝐾))
65		simpl2l 1227	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐹 ∈ 𝑇)
66	16, 58, 4, 5, 13	trlid0b 40434	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐹 = ( I ↾ 𝐵) ↔ (𝑅‘𝐹) = (0.‘𝐾)))
67	56, 65, 66	syl2anc 584	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐹 = ( I ↾ 𝐵) ↔ (𝑅‘𝐹) = (0.‘𝐾)))
68	64, 67	mpbird 257	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐹 = ( I ↾ 𝐵))
69	68	coeq1d 5810	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐹 ∘ 𝐺) = (( I ↾ 𝐵) ∘ 𝐺))
70	56, 57, 22	syl2anc 584	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐺:𝐵–1-1-onto→𝐵)
71	70, 24, 25	3syl 18	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (( I ↾ 𝐵) ∘ 𝐺) = 𝐺)
72	69, 71	eqtrd 2771	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐹 ∘ 𝐺) = 𝐺)
73	72	fveq2d 6838	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘(𝐹 ∘ 𝐺)) = (𝑅‘𝐺))
74	63, 64, 73	3netr4d 3009	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))
75		simp1 1136	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
76		simp2l 1200	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → 𝐹 ∈ 𝑇)
77	58, 33, 4, 5, 13	trlator0 40427	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅‘𝐹) = (0.‘𝐾)))
78	75, 76, 77	syl2anc 584	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅‘𝐹) = (0.‘𝐾)))
79	54, 74, 78	mpjaodan 960	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 class class class wbr 5098 I cid 5518 ^◡ccnv 5623 ↾ cres 5626 ∘ ccom 5628 ⟶wf 6488 –1-1-onto→wf1o 6491 ‘cfv 6492 (class class class)co 7358 Basecbs 17136 lecple 17184 joincjn 18234 0.cp0 18344 Atomscatm 39519 AtLatcal 39520 HLchlt 39606 LHypclh 40240 LTrncltrn 40357 trLctrl 40414

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-riotaBAD 39209

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-1st 7933 df-2nd 7934 df-undef 8215 df-map 8765 df-proset 18217 df-poset 18236 df-plt 18251 df-lub 18267 df-glb 18268 df-join 18269 df-meet 18270 df-p0 18346 df-p1 18347 df-lat 18355 df-clat 18422 df-oposet 39432 df-ol 39434 df-oml 39435 df-covers 39522 df-ats 39523 df-atl 39554 df-cvlat 39578 df-hlat 39607 df-llines 39754 df-lplanes 39755 df-lvols 39756 df-lines 39757 df-psubsp 39759 df-pmap 39760 df-padd 40052 df-lhyp 40244 df-laut 40245 df-ldil 40360 df-ltrn 40361 df-trl 40415

This theorem is referenced by: trljco 40996 cdlemh2 41072 cdlemh 41073 cdlemk3 41089 cdlemk12 41106 cdlemk12u 41128 cdlemkfid1N 41177 cdlemk54 41214

W3C validator