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

Metamath Proof Explorer

Theorem grpoinvf

Description: Mapping of the inverse function of a group. (Contributed by NM, 29-Mar-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpasscan1.1 ⊢ 𝑋 = ran 𝐺
grpasscan1.2 ⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion grpoinvf ( 𝐺 ∈ GrpOp → 𝑁 : 𝑋 –1-1-onto→ 𝑋 )

Proof

Step Hyp Ref Expression
1 grpasscan1.1 ⊢ 𝑋 = ran 𝐺
2 grpasscan1.2 ⊢ 𝑁 = ( inv ‘ 𝐺 )
3 riotaex ⊢ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) ∈ V
4 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) )
5 3 4 fnmpti ⊢ ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) ) Fn 𝑋
6 eqid ⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
7 1 6 2 grpoinvfval ⊢ ( 𝐺 ∈ GrpOp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) ) )
8 7 fneq1d ⊢ ( 𝐺 ∈ GrpOp → ( 𝑁 Fn 𝑋 ↔ ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) ) Fn 𝑋 ) )
9 5 8 mpbiri ⊢ ( 𝐺 ∈ GrpOp → 𝑁 Fn 𝑋 )
10 fnrnfv ⊢ ( 𝑁 Fn 𝑋 → ran 𝑁 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) } )
11 9 10 syl ⊢ ( 𝐺 ∈ GrpOp → ran 𝑁 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) } )
12 1 2 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑦 ) ∈ 𝑋 )
13 1 2 grpo2inv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) = 𝑦 )
14 13 eqcomd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) → 𝑦 = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) )
15 fveq2 ⊢ ( 𝑥 = ( 𝑁 ‘ 𝑦 ) → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) )
16 15 rspceeqv ⊢ ( ( ( 𝑁 ‘ 𝑦 ) ∈ 𝑋 ∧ 𝑦 = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) )
17 12 14 16 syl2anc ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) )
18 17 ex ⊢ ( 𝐺 ∈ GrpOp → ( 𝑦 ∈ 𝑋 → ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) ) )
19 simpr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 = ( 𝑁 ‘ 𝑥 ) ) → 𝑦 = ( 𝑁 ‘ 𝑥 ) )
20 1 2 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑥 ) ∈ 𝑋 )
21 20 adantr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 = ( 𝑁 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝑥 ) ∈ 𝑋 )
22 19 21 eqeltrd ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 = ( 𝑁 ‘ 𝑥 ) ) → 𝑦 ∈ 𝑋 )
23 22 rexlimdva2 ⊢ ( 𝐺 ∈ GrpOp → ( ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) → 𝑦 ∈ 𝑋 ) )
24 18 23 impbid ⊢ ( 𝐺 ∈ GrpOp → ( 𝑦 ∈ 𝑋 ↔ ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) ) )
25 24 eqabdv ⊢ ( 𝐺 ∈ GrpOp → 𝑋 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) } )
26 11 25 eqtr4d ⊢ ( 𝐺 ∈ GrpOp → ran 𝑁 = 𝑋 )
27 fveq2 ⊢ ( ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑦 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) )
28 1 2 grpo2inv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑥 ) ) = 𝑥 )
29 28 13 eqeqan12d ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) ↔ 𝑥 = 𝑦 ) )
30 29 anandis ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) ↔ 𝑥 = 𝑦 ) )
31 27 30 imbitrid ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
32 31 ralrimivva ⊢ ( 𝐺 ∈ GrpOp → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
33 dff1o6 ⊢ ( 𝑁 : 𝑋 –1-1-onto→ 𝑋 ↔ ( 𝑁 Fn 𝑋 ∧ ran 𝑁 = 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
34 9 26 32 33 syl3anbrc ⊢ ( 𝐺 ∈ GrpOp → 𝑁 : 𝑋 –1-1-onto→ 𝑋 )