Metamath Proof Explorer


Theorem 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 B M = f | f : S 1-1 onto S x S y S x y f x f y

Proof

Step Hyp Ref Expression
1 pautset.s S = PSubSp K
2 pautset.m M = PAut K
3 elex K B K V
4 fveq2 k = K PSubSp k = PSubSp K
5 4 1 eqtr4di k = K PSubSp k = S
6 5 f1oeq2d k = K f : PSubSp k 1-1 onto PSubSp k f : S 1-1 onto PSubSp k
7 f1oeq3 PSubSp k = S f : S 1-1 onto PSubSp k f : S 1-1 onto S
8 5 7 syl k = K f : S 1-1 onto PSubSp k f : S 1-1 onto S
9 6 8 bitrd k = K f : PSubSp k 1-1 onto PSubSp k f : S 1-1 onto S
10 5 raleqdv k = K y PSubSp k x y f x f y y S x y f x f y
11 5 10 raleqbidv k = K x PSubSp k y PSubSp k x y f x f y x S y S x y f x f y
12 9 11 anbi12d k = K f : PSubSp k 1-1 onto PSubSp k x PSubSp k y PSubSp k x y f x f y f : S 1-1 onto S x S y S x y f x f y
13 12 abbidv k = K f | f : PSubSp k 1-1 onto PSubSp k x PSubSp k y PSubSp k x y f x f y = f | f : S 1-1 onto S x S y S x y f x f y
14 df-pautN PAut = k V f | f : PSubSp k 1-1 onto PSubSp k x PSubSp k y PSubSp k x y f x f y
15 1 fvexi S V
16 15 15 mapval S S = f | f : S S
17 ovex S S V
18 16 17 eqeltrri f | f : S S V
19 f1of f : S 1-1 onto S f : S S
20 19 ss2abi f | f : S 1-1 onto S f | f : S S
21 18 20 ssexi f | f : S 1-1 onto S V
22 simpl f : S 1-1 onto S x S y S x y f x f y f : S 1-1 onto S
23 22 ss2abi f | f : S 1-1 onto S x S y S x y f x f y f | f : S 1-1 onto S
24 21 23 ssexi f | f : S 1-1 onto S x S y S x y f x f y V
25 13 14 24 fvmpt K V PAut K = f | f : S 1-1 onto S x S y S x y f x f y
26 2 25 syl5eq K V M = f | f : S 1-1 onto S x S y S x y f x f y
27 3 26 syl K B M = f | f : S 1-1 onto S x S y S x y f x f y