trnfsetN

Description: The mapping from fiducial atom to set of translations. (Contributed by NM, 4-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	trnset.a	$⊢ A = Atoms (K)$
	trnset.s	$⊢ S = PSubSp (K)$
	trnset.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	trnset.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	trnset.w	$⊢ W = WAtoms (K)$
	trnset.m	$⊢ M = PAut (K)$
	trnset.l	$⊢ L = Dil (K)$
	trnset.t	$⊢ T = Trn (K)$
Assertion	trnfsetN	$⊢ K \in C \to T = (d \in A ⟼ \{f \in L (d) \| \forall q \in W (d) \forall r \in W (d) (q \underset{˙}{+} f (q)) \cap \underset{˙}{⊥} (\{d\}) = (r \underset{˙}{+} f (r)) \cap \underset{˙}{⊥} (\{d\})\})$

Proof

Step	Hyp	Ref	Expression
1		trnset.a	$⊢ A = Atoms (K)$
2		trnset.s	$⊢ S = PSubSp (K)$
3		trnset.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
4		trnset.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
5		trnset.w	$⊢ W = WAtoms (K)$
6		trnset.m	$⊢ M = PAut (K)$
7		trnset.l	$⊢ L = Dil (K)$
8		trnset.t	$⊢ T = Trn (K)$
9		elex	$⊢ K \in C \to K \in V$
10		fveq2	$⊢ k = K \to Atoms (k) = Atoms (K)$
11	10 1	eqtr4di	$⊢ k = K \to Atoms (k) = A$
12		fveq2	$⊢ k = K \to Dil (k) = Dil (K)$
13	12 7	eqtr4di	$⊢ k = K \to Dil (k) = L$
14	13	fveq1d	$⊢ k = K \to Dil (k) (d) = L (d)$
15		fveq2	$⊢ k = K \to WAtoms (k) = WAtoms (K)$
16	15 5	eqtr4di	$⊢ k = K \to WAtoms (k) = W$
17	16	fveq1d	$⊢ k = K \to WAtoms (k) (d) = W (d)$
18		fveq2	$⊢ k = K \to +_{𝑃} (k) = +_{𝑃} (K)$
19	18 3	eqtr4di	$⊢ k = K \to +_{𝑃} (k) = \underset{˙}{+}$
20	19	oveqd	$⊢ k = K \to q +_{𝑃} (k) f (q) = q \underset{˙}{+} f (q)$
21		fveq2	$⊢ k = K \to ⊥_{𝑃} (k) = ⊥_{𝑃} (K)$
22	21 4	eqtr4di	$⊢ k = K \to ⊥_{𝑃} (k) = \underset{˙}{⊥}$
23	22	fveq1d	$⊢ k = K \to ⊥_{𝑃} (k) (\{d\}) = \underset{˙}{⊥} (\{d\})$
24	20 23	ineq12d	$⊢ k = K \to (q +_{𝑃} (k) f (q)) \cap ⊥_{𝑃} (k) (\{d\}) = (q \underset{˙}{+} f (q)) \cap \underset{˙}{⊥} (\{d\})$
25	19	oveqd	$⊢ k = K \to r +_{𝑃} (k) f (r) = r \underset{˙}{+} f (r)$
26	25 23	ineq12d	$⊢ k = K \to (r +_{𝑃} (k) f (r)) \cap ⊥_{𝑃} (k) (\{d\}) = (r \underset{˙}{+} f (r)) \cap \underset{˙}{⊥} (\{d\})$
27	24 26	eqeq12d	$⊢ k = K \to ((q +_{𝑃} (k) f (q)) \cap ⊥_{𝑃} (k) (\{d\}) = (r +_{𝑃} (k) f (r)) \cap ⊥_{𝑃} (k) (\{d\}) \leftrightarrow (q \underset{˙}{+} f (q)) \cap \underset{˙}{⊥} (\{d\}) = (r \underset{˙}{+} f (r)) \cap \underset{˙}{⊥} (\{d\}))$
28	17 27	raleqbidv	$⊢ k = K \to (\forall r \in WAtoms (k) (d) (q +_{𝑃} (k) f (q)) \cap ⊥_{𝑃} (k) (\{d\}) = (r +_{𝑃} (k) f (r)) \cap ⊥_{𝑃} (k) (\{d\}) \leftrightarrow \forall r \in W (d) (q \underset{˙}{+} f (q)) \cap \underset{˙}{⊥} (\{d\}) = (r \underset{˙}{+} f (r)) \cap \underset{˙}{⊥} (\{d\}))$
29	17 28	raleqbidv	$⊢ k = K \to (\forall q \in WAtoms (k) (d) \forall r \in WAtoms (k) (d) (q +_{𝑃} (k) f (q)) \cap ⊥_{𝑃} (k) (\{d\}) = (r +_{𝑃} (k) f (r)) \cap ⊥_{𝑃} (k) (\{d\}) \leftrightarrow \forall q \in W (d) \forall r \in W (d) (q \underset{˙}{+} f (q)) \cap \underset{˙}{⊥} (\{d\}) = (r \underset{˙}{+} f (r)) \cap \underset{˙}{⊥} (\{d\}))$
30	14 29	rabeqbidv	$⊢ k = K \to \{f \in Dil (k) (d) \| \forall q \in WAtoms (k) (d) \forall r \in WAtoms (k) (d) (q +_{𝑃} (k) f (q)) \cap ⊥_{𝑃} (k) (\{d\}) = (r +_{𝑃} (k) f (r)) \cap ⊥_{𝑃} (k) (\{d\})\} = \{f \in L (d) \| \forall q \in W (d) \forall r \in W (d) (q \underset{˙}{+} f (q)) \cap \underset{˙}{⊥} (\{d\}) = (r \underset{˙}{+} f (r)) \cap \underset{˙}{⊥} (\{d\})\}$
31	11 30	mpteq12dv	$⊢ k = K \to (d \in Atoms (k) ⟼ \{f \in Dil (k) (d) \| \forall q \in WAtoms (k) (d) \forall r \in WAtoms (k) (d) (q +_{𝑃} (k) f (q)) \cap ⊥_{𝑃} (k) (\{d\}) = (r +_{𝑃} (k) f (r)) \cap ⊥_{𝑃} (k) (\{d\})\}) = (d \in A ⟼ \{f \in L (d) \| \forall q \in W (d) \forall r \in W (d) (q \underset{˙}{+} f (q)) \cap \underset{˙}{⊥} (\{d\}) = (r \underset{˙}{+} f (r)) \cap \underset{˙}{⊥} (\{d\})\})$
32		df-trnN	$⊢ Trn = (k \in V ⟼ (d \in Atoms (k) ⟼ \{f \in Dil (k) (d) \| \forall q \in WAtoms (k) (d) \forall r \in WAtoms (k) (d) (q +_{𝑃} (k) f (q)) \cap ⊥_{𝑃} (k) (\{d\}) = (r +_{𝑃} (k) f (r)) \cap ⊥_{𝑃} (k) (\{d\})\}))$
33	31 32 1	mptfvmpt	$⊢ K \in V \to Trn (K) = (d \in A ⟼ \{f \in L (d) \| \forall q \in W (d) \forall r \in W (d) (q \underset{˙}{+} f (q)) \cap \underset{˙}{⊥} (\{d\}) = (r \underset{˙}{+} f (r)) \cap \underset{˙}{⊥} (\{d\})\})$
34	8 33	syl5eq	$⊢ K \in V \to T = (d \in A ⟼ \{f \in L (d) \| \forall q \in W (d) \forall r \in W (d) (q \underset{˙}{+} f (q)) \cap \underset{˙}{⊥} (\{d\}) = (r \underset{˙}{+} f (r)) \cap \underset{˙}{⊥} (\{d\})\})$
35	9 34	syl	$⊢ K \in C \to T = (d \in A ⟼ \{f \in L (d) \| \forall q \in W (d) \forall r \in W (d) (q \underset{˙}{+} f (q)) \cap \underset{˙}{⊥} (\{d\}) = (r \underset{˙}{+} f (r)) \cap \underset{˙}{⊥} (\{d\})\})$

Metamath Proof Explorer

Theorem trnfsetN

Proof