Theorem istrnN

Description: The predicate "is a translation". (Contributed by NM, 4-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	trnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	trnset.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
	trnset.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
	trnset.o	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
	trnset.w	$$⊢W=\mathrm{WAtoms}\left(K\right)$$
	trnset.m	$$⊢M=\mathrm{PAut}\left(K\right)$$
	trnset.l	$$⊢L=\mathrm{Dil}\left(K\right)$$
	trnset.t	$$⊢T=\mathrm{Trn}\left(K\right)$$
Assertion	istrnN	$$⊢\left(K\in B\wedge D\in A\right)\to \left(F\in T\left(D\right)\leftrightarrow \left(F\in L\left(D\right)\wedge \forall q\in W\left(D\right)\forall r\in W\left(D\right)\left(q\underset{\dot{}}{+}F\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}F\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		trnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		trnset.s	$$⊢S=\mathrm{PSubSp}\left(K\right)$$
3		trnset.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
4		trnset.o	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
5		trnset.w	$$⊢W=\mathrm{WAtoms}\left(K\right)$$
6		trnset.m	$$⊢M=\mathrm{PAut}\left(K\right)$$
7		trnset.l	$$⊢L=\mathrm{Dil}\left(K\right)$$
8		trnset.t	$$⊢T=\mathrm{Trn}\left(K\right)$$
9	1 2 3 4 5 6 7 8	trnsetN	$$⊢\left(K\in B\wedge D\in A\right)\to T\left(D\right)=\left\{f\in L\left(D\right)|\forall q\in W\left(D\right)\forall r\in W\left(D\right)\left(q\underset{\dot{}}{+}f\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}f\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)\right\}$$
10	9	eleq2d	$$⊢\left(K\in B\wedge D\in A\right)\to \left(F\in T\left(D\right)\leftrightarrow F\in \left\{f\in L\left(D\right)|\forall q\in W\left(D\right)\forall r\in W\left(D\right)\left(q\underset{\dot{}}{+}f\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}f\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)\right\}\right)$$
11		fveq1	$$⊢f=F\to f\left(q\right)=F\left(q\right)$$
12	11	oveq2d	$$⊢f=F\to q\underset{\dot{}}{+}f\left(q\right)=q\underset{\dot{}}{+}F\left(q\right)$$
13	12	ineq1d	$$⊢f=F\to \left(q\underset{\dot{}}{+}f\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(q\underset{\dot{}}{+}F\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)$$
14		fveq1	$$⊢f=F\to f\left(r\right)=F\left(r\right)$$
15	14	oveq2d	$$⊢f=F\to r\underset{\dot{}}{+}f\left(r\right)=r\underset{\dot{}}{+}F\left(r\right)$$
16	15	ineq1d	$$⊢f=F\to \left(r\underset{\dot{}}{+}f\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}F\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)$$
17	13 16	eqeq12d	$$⊢f=F\to \left(\left(q\underset{\dot{}}{+}f\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}f\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)\leftrightarrow \left(q\underset{\dot{}}{+}F\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}F\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)\right)$$
18	17	2ralbidv	$$⊢f=F\to \left(\forall q\in W\left(D\right)\forall r\in W\left(D\right)\left(q\underset{\dot{}}{+}f\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}f\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)\leftrightarrow \forall q\in W\left(D\right)\forall r\in W\left(D\right)\left(q\underset{\dot{}}{+}F\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}F\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)\right)$$
19	18	elrab	$$⊢F\in \left\{f\in L\left(D\right)|\forall q\in W\left(D\right)\forall r\in W\left(D\right)\left(q\underset{\dot{}}{+}f\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}f\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)\right\}\leftrightarrow \left(F\in L\left(D\right)\wedge \forall q\in W\left(D\right)\forall r\in W\left(D\right)\left(q\underset{\dot{}}{+}F\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}F\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)\right)$$
20	10 19	syl6bb	$$⊢\left(K\in B\wedge D\in A\right)\to \left(F\in T\left(D\right)\leftrightarrow \left(F\in L\left(D\right)\wedge \forall q\in W\left(D\right)\forall r\in W\left(D\right)\left(q\underset{\dot{}}{+}F\left(q\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)=\left(r\underset{\dot{}}{+}F\left(r\right)\right)\cap \underset{\dot{}}{\perp }\left(\left\{D\right\}\right)\right)\right)$$