Theorem trlid0b

Description: A lattice translation is the identity iff its trace is zero. (Contributed by NM, 14-Jun-2013)

	Ref	Expression
Hypotheses	trlid0b.b	$$⊢B={\mathrm{Base}}_K$$
	trlid0b.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	trlid0b.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	trlid0b.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	trlid0b.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
Assertion	trlid0b	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to \left(F={\mathrm{I}\upharpoonright }_B\leftrightarrow R\left(F\right)=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		trlid0b.b	$$⊢B={\mathrm{Base}}_K$$
2		trlid0b.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
3		trlid0b.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		trlid0b.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
5		trlid0b.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
6		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
7	1 6 3 4 5	trlnidatb	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to \left(F\ne {\mathrm{I}\upharpoonright }_B\leftrightarrow R\left(F\right)\in \mathrm{Atoms}\left(K\right)\right)$$
8	2 6 3 4 5	trlatn0	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to \left(R\left(F\right)\in \mathrm{Atoms}\left(K\right)\leftrightarrow R\left(F\right)\ne \underset{\dot{}}{0}\right)$$
9	7 8	bitrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to \left(F\ne {\mathrm{I}\upharpoonright }_B\leftrightarrow R\left(F\right)\ne \underset{\dot{}}{0}\right)$$
10	9	necon4bid	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to \left(F={\mathrm{I}\upharpoonright }_B\leftrightarrow R\left(F\right)=\underset{\dot{}}{0}\right)$$