pautsetN

Description: The set of projective automorphisms. (Contributed by NM, 26-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pautset.s	$⊢ S = PSubSp (K)$
	pautset.m	$⊢ M = PAut (K)$
Assertion	pautsetN	$⊢ K \in B \to M = \{f \| (f : S \underset{1-1 onto}{⟶} S \land \forall x \in S \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))\}$

Proof

Step	Hyp	Ref	Expression
1		pautset.s	$⊢ S = PSubSp (K)$
2		pautset.m	$⊢ M = PAut (K)$
3		elex	$⊢ K \in B \to K \in V$
4		fveq2	$⊢ k = K \to PSubSp (k) = PSubSp (K)$
5	4 1	eqtr4di	$⊢ k = K \to PSubSp (k) = S$
6	5	f1oeq2d	$⊢ k = K \to (f : PSubSp (k) \underset{1-1 onto}{⟶} PSubSp (k) \leftrightarrow f : S \underset{1-1 onto}{⟶} PSubSp (k))$
7		f1oeq3	$⊢ PSubSp (k) = S \to (f : S \underset{1-1 onto}{⟶} PSubSp (k) \leftrightarrow f : S \underset{1-1 onto}{⟶} S)$
8	5 7	syl	$⊢ k = K \to (f : S \underset{1-1 onto}{⟶} PSubSp (k) \leftrightarrow f : S \underset{1-1 onto}{⟶} S)$
9	6 8	bitrd	$⊢ k = K \to (f : PSubSp (k) \underset{1-1 onto}{⟶} PSubSp (k) \leftrightarrow f : S \underset{1-1 onto}{⟶} S)$
10	5	raleqdv	$⊢ k = K \to (\forall y \in PSubSp (k) (x \subseteq y \leftrightarrow f (x) \subseteq f (y)) \leftrightarrow \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))$
11	5 10	raleqbidv	$⊢ k = K \to (\forall x \in PSubSp (k) \forall y \in PSubSp (k) (x \subseteq y \leftrightarrow f (x) \subseteq f (y)) \leftrightarrow \forall x \in S \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))$
12	9 11	anbi12d	$⊢ k = K \to ((f : PSubSp (k) \underset{1-1 onto}{⟶} PSubSp (k) \land \forall x \in PSubSp (k) \forall y \in PSubSp (k) (x \subseteq y \leftrightarrow f (x) \subseteq f (y))) \leftrightarrow (f : S \underset{1-1 onto}{⟶} S \land \forall x \in S \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y))))$
13	12	abbidv	$⊢ k = K \to \{f \| (f : PSubSp (k) \underset{1-1 onto}{⟶} PSubSp (k) \land \forall x \in PSubSp (k) \forall y \in PSubSp (k) (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))\} = \{f \| (f : S \underset{1-1 onto}{⟶} S \land \forall x \in S \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))\}$
14		df-pautN	$⊢ PAut = (k \in V ⟼ \{f \| (f : PSubSp (k) \underset{1-1 onto}{⟶} PSubSp (k) \land \forall x \in PSubSp (k) \forall y \in PSubSp (k) (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))\})$
15	1	fvexi	$⊢ S \in V$
16	15 15	mapval	$⊢ S^{S} = \{f \| f : S ⟶ S\}$
17		ovex	$⊢ S^{S} \in V$
18	16 17	eqeltrri	$⊢ \{f \| f : S ⟶ S\} \in V$
19		f1of	$⊢ f : S \underset{1-1 onto}{⟶} S \to f : S ⟶ S$
20	19	ss2abi	$⊢ \{f \| f : S \underset{1-1 onto}{⟶} S\} \subseteq \{f \| f : S ⟶ S\}$
21	18 20	ssexi	$⊢ \{f \| f : S \underset{1-1 onto}{⟶} S\} \in V$
22		simpl	$⊢ (f : S \underset{1-1 onto}{⟶} S \land \forall x \in S \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y))) \to f : S \underset{1-1 onto}{⟶} S$
23	22	ss2abi	$⊢ \{f \| (f : S \underset{1-1 onto}{⟶} S \land \forall x \in S \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))\} \subseteq \{f \| f : S \underset{1-1 onto}{⟶} S\}$
24	21 23	ssexi	$⊢ \{f \| (f : S \underset{1-1 onto}{⟶} S \land \forall x \in S \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))\} \in V$
25	13 14 24	fvmpt	$⊢ K \in V \to PAut (K) = \{f \| (f : S \underset{1-1 onto}{⟶} S \land \forall x \in S \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))\}$
26	2 25	eqtrid	$⊢ K \in V \to M = \{f \| (f : S \underset{1-1 onto}{⟶} S \land \forall x \in S \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))\}$
27	3 26	syl	$⊢ K \in B \to M = \{f \| (f : S \underset{1-1 onto}{⟶} S \land \forall x \in S \forall y \in S (x \subseteq y \leftrightarrow f (x) \subseteq f (y)))\}$

Metamath Proof Explorer

Theorem pautsetN

Proof