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

Metamath Proof Explorer

Theorem qusgrp2

Description: Prove that a quotient structure is a group. (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypotheses qusgrp2.u ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
qusgrp2.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
qusgrp2.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
qusgrp2.r ⊢ ( 𝜑 → ∼ Er 𝑉 )
qusgrp2.x ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
qusgrp2.e ⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 + 𝑏 ) ∼ ( 𝑝 + 𝑞 ) ) )
qusgrp2.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
qusgrp2.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) ∼ ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
qusgrp2.3 ⊢ ( 𝜑 → 0 ∈ 𝑉 )
qusgrp2.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 0 + 𝑥 ) ∼ 𝑥 )
qusgrp2.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑁 ∈ 𝑉 )
qusgrp2.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑁 + 𝑥 ) ∼ 0 )
Assertion qusgrp2 ( 𝜑 → ( 𝑈 ∈ Grp ∧ [ 0 ] ∼ = ( 0g ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 qusgrp2.u ⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) )
2 qusgrp2.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 qusgrp2.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
4 qusgrp2.r ⊢ ( 𝜑 → ∼ Er 𝑉 )
5 qusgrp2.x ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
6 qusgrp2.e ⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 + 𝑏 ) ∼ ( 𝑝 + 𝑞 ) ) )
7 qusgrp2.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
8 qusgrp2.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) ∼ ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
9 qusgrp2.3 ⊢ ( 𝜑 → 0 ∈ 𝑉 )
10 qusgrp2.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 0 + 𝑥 ) ∼ 𝑥 )
11 qusgrp2.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑁 ∈ 𝑉 )
12 qusgrp2.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑁 + 𝑥 ) ∼ 0 )
13 eqid ⊢ ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) = ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ )
14 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
15 2 14 eqeltrdi ⊢ ( 𝜑 → 𝑉 ∈ V )
16 erex ⊢ ( ∼ Er 𝑉 → ( 𝑉 ∈ V → ∼ ∈ V ) )
17 4 15 16 sylc ⊢ ( 𝜑 → ∼ ∈ V )
18 1 2 13 17 5 qusval ⊢ ( 𝜑 → 𝑈 = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) “s 𝑅 ) )
19 1 2 13 17 5 quslem ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) : 𝑉 –onto→ ( 𝑉 / ∼ ) )
20 7 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
21 4 15 13 20 6 ercpbl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑎 ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑝 ) ∧ ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑏 ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑞 ) ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑝 + 𝑞 ) ) ) )
22 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ∼ Er 𝑉 )
23 22 8 erthi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → [ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ] ∼ = [ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ] ∼ )
24 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑉 ∈ V )
25 22 24 13 divsfval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = [ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ] ∼ )
26 22 24 13 divsfval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) = [ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ] ∼ )
27 23 25 26 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
28 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ∼ Er 𝑉 )
29 28 10 erthi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → [ ( 0 + 𝑥 ) ] ∼ = [ 𝑥 ] ∼ )
30 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑉 ∈ V )
31 28 30 13 divsfval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 0 + 𝑥 ) ) = [ ( 0 + 𝑥 ) ] ∼ )
32 28 30 13 divsfval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑥 ) = [ 𝑥 ] ∼ )
33 29 31 32 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 0 + 𝑥 ) ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 𝑥 ) )
34 28 12 ersym ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 0 ∼ ( 𝑁 + 𝑥 ) )
35 28 34 erthi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → [ 0 ] ∼ = [ ( 𝑁 + 𝑥 ) ] ∼ )
36 28 30 13 divsfval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) = [ 0 ] ∼ )
37 28 30 13 divsfval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑁 + 𝑥 ) ) = [ ( 𝑁 + 𝑥 ) ] ∼ )
38 35 36 37 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ ( 𝑁 + 𝑥 ) ) = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) )
39 18 2 3 19 21 5 7 27 9 33 11 38 imasgrp2 ⊢ ( 𝜑 → ( 𝑈 ∈ Grp ∧ ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )
40 4 15 13 divsfval ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) = [ 0 ] ∼ )
41 40 eqcomd ⊢ ( 𝜑 → [ 0 ] ∼ = ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) )
42 41 eqeq1d ⊢ ( 𝜑 → ( [ 0 ] ∼ = ( 0g ‘ 𝑈 ) ↔ ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )
43 42 anbi2d ⊢ ( 𝜑 → ( ( 𝑈 ∈ Grp ∧ [ 0 ] ∼ = ( 0g ‘ 𝑈 ) ) ↔ ( 𝑈 ∈ Grp ∧ ( ( 𝑢 ∈ 𝑉 ↦ [ 𝑢 ] ∼ ) ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) )
44 39 43 mpbird ⊢ ( 𝜑 → ( 𝑈 ∈ Grp ∧ [ 0 ] ∼ = ( 0g ‘ 𝑈 ) ) )