trl0

Description: If an atom not under the fiducial co-atom W equals its lattice translation, the trace of the translation is zero. (Contributed by NM, 24-May-2012)

	Ref	Expression
Hypotheses	trl0.l	⊢ ≤ = ( le ‘ 𝐾 )
	trl0.z	⊢ 0 = ( 0. ‘ 𝐾 )
	trl0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	trl0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	trl0.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	trl0.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	trl0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		trl0.l	⊢ ≤ = ( le ‘ 𝐾 )
2		trl0.z	⊢ 0 = ( 0. ‘ 𝐾 )
3		trl0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		trl0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		trl0.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		trl0.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
7		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		simp3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → 𝐹 ∈ 𝑇 )
9		simp2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
10		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
11		eqid	⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
12	1 10 11 3 4 5 6	trlval2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ( join ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
13	7 8 9 12	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ( join ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
14		simp3r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝐹 ‘ 𝑃 ) = 𝑃 )
15	14	oveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝑃 ( join ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) = ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) )
16		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → 𝐾 ∈ HL )
17		simp2l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → 𝑃 ∈ 𝐴 )
18	10 3	hlatjidm	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) = 𝑃 )
19	16 17 18	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝑃 ( join ‘ 𝐾 ) 𝑃 ) = 𝑃 )
20	15 19	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝑃 ( join ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) = 𝑃 )
21	20	oveq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( ( 𝑃 ( join ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ( meet ‘ 𝐾 ) 𝑊 ) = ( 𝑃 ( meet ‘ 𝐾 ) 𝑊 ) )
22	1 11 2 3 4	lhpmat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ( meet ‘ 𝐾 ) 𝑊 ) = 0 )
23	7 9 22	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝑃 ( meet ‘ 𝐾 ) 𝑊 ) = 0 )
24	13 21 23	3eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) = 0 )

Metamath Proof Explorer

Theorem trl0

Proof