Metamath Proof Explorer


Definition df-pautN

Description: Define set of all projective automorphisms. This is the intended definition of automorphism in Crawley p. 112. (Contributed by NM, 26-Jan-2012)

Ref Expression
Assertion df-pautN PAut = ( 𝑘 ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥𝑦 ↔ ( 𝑓𝑥 ) ⊆ ( 𝑓𝑦 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpautN PAut
1 vk 𝑘
2 cvv V
3 vf 𝑓
4 3 cv 𝑓
5 cpsubsp PSubSp
6 1 cv 𝑘
7 6 5 cfv ( PSubSp ‘ 𝑘 )
8 7 7 4 wf1o 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 )
9 vx 𝑥
10 vy 𝑦
11 9 cv 𝑥
12 10 cv 𝑦
13 11 12 wss 𝑥𝑦
14 11 4 cfv ( 𝑓𝑥 )
15 12 4 cfv ( 𝑓𝑦 )
16 14 15 wss ( 𝑓𝑥 ) ⊆ ( 𝑓𝑦 )
17 13 16 wb ( 𝑥𝑦 ↔ ( 𝑓𝑥 ) ⊆ ( 𝑓𝑦 ) )
18 17 10 7 wral 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥𝑦 ↔ ( 𝑓𝑥 ) ⊆ ( 𝑓𝑦 ) )
19 18 9 7 wral 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥𝑦 ↔ ( 𝑓𝑥 ) ⊆ ( 𝑓𝑦 ) )
20 8 19 wa ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥𝑦 ↔ ( 𝑓𝑥 ) ⊆ ( 𝑓𝑦 ) ) )
21 20 3 cab { 𝑓 ∣ ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥𝑦 ↔ ( 𝑓𝑥 ) ⊆ ( 𝑓𝑦 ) ) ) }
22 1 2 21 cmpt ( 𝑘 ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥𝑦 ↔ ( 𝑓𝑥 ) ⊆ ( 𝑓𝑦 ) ) ) } )
23 0 22 wceq PAut = ( 𝑘 ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( PSubSp ‘ 𝑘 ) –1-1-onto→ ( PSubSp ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ∀ 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥𝑦 ↔ ( 𝑓𝑥 ) ⊆ ( 𝑓𝑦 ) ) ) } )