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 41227

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 1235	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝐹) ≠ (𝑅‘𝐺))
2		simp11 1210	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3		simp12l 1293	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐹 ∈ 𝑇)
4		trlcone.h	. . . . . . . . . . 11 ⊢ 𝐻 = (LHyp‘𝐾)
5		trlcone.t	. . . . . . . . . . 11 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
6	4, 5	ltrncnv 40645	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
7	2, 3, 6	syl2anc 590	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ^◡𝐹 ∈ 𝑇)
8		simp12r 1294	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺 ∈ 𝑇)
9	4, 5	ltrnco 41218	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ 𝐺) ∈ 𝑇)
10	2, 3, 8, 9	syl3anc 1379	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝐹 ∘ 𝐺) ∈ 𝑇)
11		eqid 2740	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
12		eqid 2740	. . . . . . . . . 10 ⊢ (join‘𝐾) = (join‘𝐾)
13		trlcone.r	. . . . . . . . . 10 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
14	11, 12, 4, 5, 13	trlco 41226	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ^◡𝐹 ∈ 𝑇 ∧ (𝐹 ∘ 𝐺) ∈ 𝑇) → (𝑅‘(^◡𝐹 ∘ (𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
15	2, 7, 10, 14	syl3anc 1379	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘(^◡𝐹 ∘ (𝐹 ∘ 𝐺)))(le‘𝐾)((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
16		trlcone.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝐾)
17	16, 4, 5	ltrn1o 40623	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
18	2, 3, 17	syl2anc 590	. . . . . . . . . . . . 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 40623	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → 𝐺:𝐵–1-1-onto→𝐵)
23	2, 8, 22	syl2anc 590	. . . . . . . . . . . 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 2775	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((^◡𝐹 ∘ 𝐹) ∘ 𝐺) = 𝐺)
28		coass 6224	. . . . . . . . . 10 ⊢ ((^◡𝐹 ∘ 𝐹) ∘ 𝐺) = (^◡𝐹 ∘ (𝐹 ∘ 𝐺))
29	27, 28	eqtr3di 2790	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺 = (^◡𝐹 ∘ (𝐹 ∘ 𝐺)))
30	29	fveq2d 6838	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺) = (𝑅‘(^◡𝐹 ∘ (𝐹 ∘ 𝐺))))
31		simp11l 1291	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐾 ∈ HL)
32		simp2 1143	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) ∈ (Atoms‘𝐾))
33		eqid 2740	. . . . . . . . . . 11 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
34	12, 33	hlatjidm 39868	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐹)(join‘𝐾)(𝑅‘𝐹)) = (𝑅‘𝐹))
35	31, 32, 34	syl2anc 590	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((𝑅‘𝐹)(join‘𝐾)(𝑅‘𝐹)) = (𝑅‘𝐹))
36	4, 5, 13	trlcnv 40664	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
37	2, 3, 36	syl2anc 590	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
38	37	eqcomd 2746	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = (𝑅‘^◡𝐹))
39		simp3 1144	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺)))
40	38, 39	oveq12d 7381	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((𝑅‘𝐹)(join‘𝐾)(𝑅‘𝐹)) = ((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
41	35, 40	eqtr3d 2777	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = ((𝑅‘^◡𝐹)(join‘𝐾)(𝑅‘(𝐹 ∘ 𝐺))))
42	15, 30, 41	3brtr4d 5111	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺)(le‘𝐾)(𝑅‘𝐹))
43		hlatl 39859	. . . . . . . . 9 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
44	31, 43	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐾 ∈ AtLat)
45		simp13r 1296	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → 𝐺 ≠ ( I ↾ 𝐵))
46	16, 33, 4, 5, 13	trlnidat 40672	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐺) ∈ (Atoms‘𝐾))
47	2, 8, 45, 46	syl3anc 1379	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺) ∈ (Atoms‘𝐾))
48	11, 33	atcmp 39810	. . . . . . . 8 ⊢ ((𝐾 ∈ AtLat ∧ (𝑅‘𝐺) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐺)(le‘𝐾)(𝑅‘𝐹) ↔ (𝑅‘𝐺) = (𝑅‘𝐹)))
49	44, 47, 32, 48	syl3anc 1379	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → ((𝑅‘𝐺)(le‘𝐾)(𝑅‘𝐹) ↔ (𝑅‘𝐺) = (𝑅‘𝐹)))
50	42, 49	mpbid 233	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐺) = (𝑅‘𝐹))
51	50	eqcomd 2746	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺))) → (𝑅‘𝐹) = (𝑅‘𝐺))
52	51	3expia 1127	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐹) = (𝑅‘(𝐹 ∘ 𝐺)) → (𝑅‘𝐹) = (𝑅‘𝐺)))
53	52	necon3d 2956	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝐹) ≠ (𝑅‘𝐺) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺))))
54	1, 53	mpd 15	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))
55		simpl3r 1236	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐺 ≠ ( I ↾ 𝐵))
56		simpl1 1198	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
57		simpl2r 1234	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐺 ∈ 𝑇)
58		eqid 2740	. . . . . . . 8 ⊢ (0.‘𝐾) = (0.‘𝐾)
59	16, 58, 4, 5, 13	trlid0b 40677	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝐺 = ( I ↾ 𝐵) ↔ (𝑅‘𝐺) = (0.‘𝐾)))
60	56, 57, 59	syl2anc 590	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐺 = ( I ↾ 𝐵) ↔ (𝑅‘𝐺) = (0.‘𝐾)))
61	60	necon3bid 2979	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐺 ≠ ( I ↾ 𝐵) ↔ (𝑅‘𝐺) ≠ (0.‘𝐾)))
62	55, 61	mpbid 233	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝐺) ≠ (0.‘𝐾))
63	62	necomd 2990	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (0.‘𝐾) ≠ (𝑅‘𝐺))
64		simpr 485	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝐹) = (0.‘𝐾))
65		simpl2l 1233	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐹 ∈ 𝑇)
66	16, 58, 4, 5, 13	trlid0b 40677	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐹 = ( I ↾ 𝐵) ↔ (𝑅‘𝐹) = (0.‘𝐾)))
67	56, 65, 66	syl2anc 590	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐹 = ( I ↾ 𝐵) ↔ (𝑅‘𝐹) = (0.‘𝐾)))
68	64, 67	mpbird 258	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐹 = ( I ↾ 𝐵))
69	68	coeq1d 5810	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐹 ∘ 𝐺) = (( I ↾ 𝐵) ∘ 𝐺))
70	56, 57, 22	syl2anc 590	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐺:𝐵–1-1-onto→𝐵)
71	70, 24, 25	3syl 18	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (( I ↾ 𝐵) ∘ 𝐺) = 𝐺)
72	69, 71	eqtrd 2775	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐹 ∘ 𝐺) = 𝐺)
73	72	fveq2d 6838	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘(𝐹 ∘ 𝐺)) = (𝑅‘𝐺))
74	63, 64, 73	3netr4d 3012	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))
75		simp1 1142	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
76		simp2l 1206	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → 𝐹 ∈ 𝑇)
77	58, 33, 4, 5, 13	trlator0 40670	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅‘𝐹) = (0.‘𝐾)))
78	75, 76, 77	syl2anc 590	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅‘𝐹) = (0.‘𝐾)))
79	54, 74, 78	mpjaodan 966	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2935 class class class wbr 5079 I cid 5519 ^◡ccnv 5624 ↾ cres 5627 ∘ ccom 5629 ⟶wf 6488 –1-1-onto→wf1o 6491 ‘cfv 6492 (class class class)co 7363 Basecbs 17177 lecple 17225 joincjn 18275 0.cp0 18385 Atomscatm 39762 AtLatcal 39763 HLchlt 39849 LHypclh 40483 LTrncltrn 40600 trLctrl 40657

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-riotaBAD 39452

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-iun 4930 df-iin 4931 df-br 5080 df-opab 5142 df-mpt 5161 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 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 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-1st 7938 df-2nd 7939 df-undef 8220 df-map 8772 df-proset 18258 df-poset 18277 df-plt 18292 df-lub 18308 df-glb 18309 df-join 18310 df-meet 18311 df-p0 18387 df-p1 18388 df-lat 18396 df-clat 18463 df-oposet 39675 df-ol 39677 df-oml 39678 df-covers 39765 df-ats 39766 df-atl 39797 df-cvlat 39821 df-hlat 39850 df-llines 39997 df-lplanes 39998 df-lvols 39999 df-lines 40000 df-psubsp 40002 df-pmap 40003 df-padd 40295 df-lhyp 40487 df-laut 40488 df-ldil 40603 df-ltrn 40604 df-trl 40658

This theorem is referenced by: trljco 41239 cdlemh2 41315 cdlemh 41316 cdlemk3 41332 cdlemk12 41349 cdlemk12u 41371 cdlemkfid1N 41420 cdlemk54 41457

W3C validator