Theorem trnsetN

Description: The set of translations for a fiducial atom D . (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	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\}$$

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	trnfsetN	$$⊢K\in B\to T=\left(d\in A⟼\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)$$
10	9	fveq1d	$$⊢K\in B\to T\left(D\right)=\left(d\in A⟼\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)\left(D\right)$$
11		fveq2	$$⊢d=D\to L\left(d\right)=L\left(D\right)$$
12		fveq2	$$⊢d=D\to W\left(d\right)=W\left(D\right)$$
13		sneq	$$⊢d=D\to \left\{d\right\}=\left\{D\right\}$$
14	13	fveq2d	$$⊢d=D\to \underset{\dot{}}{\perp }\left(\left\{d\right\}\right)=\underset{\dot{}}{\perp }\left(\left\{D\right\}\right)$$
15	14	ineq2d	$$⊢d=D\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)$$
16	14	ineq2d	$$⊢d=D\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	15 16	eqeq12d	$$⊢d=D\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	12 17	raleqbidv	$$⊢d=D\to \left(\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 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	12 18	raleqbidv	$$⊢d=D\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)$$
20	11 19	rabeqbidv	$$⊢d=D\to \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\}=\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\}$$
21		eqid	$$⊢\left(d\in A⟼\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)=\left(d\in A⟼\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)$$
22		fvex	$$⊢L\left(D\right)\in \mathrm{V}$$
23	22	rabex	$$⊢\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\}\in \mathrm{V}$$
24	20 21 23	fvmpt	$$⊢D\in A\to \left(d\in A⟼\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)\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\}$$
25	10 24	sylan9eq	$$⊢\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\}$$