This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑘 ) ( 𝑥 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) } )