Theorem qusgrp2 13420

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

Hypotheses

Ref	Expression
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

Ref	Expression
qusgrp2	⊢ (𝜑 → (𝑈 ∈ Grp ∧ [ 0 ] ∼ = (0g‘𝑈)))

Distinct variable groups:   𝑎,𝑏,𝑝,𝑞,𝑥,𝑦,𝑧, ∼   0 ,𝑎,𝑏,𝑝,𝑞,𝑥   𝑁,𝑝   𝑅,𝑝,𝑞   + ,𝑎,𝑏,𝑝,𝑞,𝑥,𝑦   𝜑,𝑎,𝑏,𝑝,𝑞,𝑥,𝑦,𝑧   𝑉,𝑎,𝑏,𝑝,𝑞,𝑥,𝑦,𝑧   𝑈,𝑎,𝑏,𝑝,𝑞,𝑥,𝑦,𝑧

Allowed substitution hints:   + (𝑧)   𝑅(𝑥,𝑦,𝑧,𝑎,𝑏)   𝑁(𝑥,𝑦,𝑧,𝑞,𝑎,𝑏)   𝑋(𝑥,𝑦,𝑧,𝑞,𝑝,𝑎,𝑏)   0 (𝑦,𝑧)

Proof of Theorem qusgrp2

Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		qusgrp2.u	. . . 4 ⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))
2		qusgrp2.v	. . . 4 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
3		eqid 2204	. . . 4 ⊢ (𝑢 ∈ 𝑉 ↦ [𝑢] ∼ ) = (𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )
4		qusgrp2.r	. . . . 5 ⊢ (𝜑 → ∼ Er 𝑉)
5		basfn 12861	. . . . . . 7 ⊢ Base Fn V
6		qusgrp2.x	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ 𝑋)
7	6	elexd 2784	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ V)
8		funfvex 5592	. . . . . . . 8 ⊢ ((Fun Base ∧ 𝑅 ∈ dom Base) → (Base‘𝑅) ∈ V)
9	8	funfni 5375	. . . . . . 7 ⊢ ((Base Fn V ∧ 𝑅 ∈ V) → (Base‘𝑅) ∈ V)
10	5, 7, 9	sylancr 414	. . . . . 6 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
11	2, 10	eqeltrd 2281	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ V)
12		erex 6643	. . . . 5 ⊢ ( ∼ Er 𝑉 → (𝑉 ∈ V → ∼ ∈ V))
13	4, 11, 12	sylc 62	. . . 4 ⊢ (𝜑 → ∼ ∈ V)
14	1, 2, 3, 13, 6	qusval 13126	. . 3 ⊢ (𝜑 → 𝑈 = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ ) “s 𝑅))
15		qusgrp2.p	. . 3 ⊢ (𝜑 → + = (+g‘𝑅))
16	1, 2, 3, 13, 6	quslem 13127	. . 3 ⊢ (𝜑 → (𝑢 ∈ 𝑉 ↦ [𝑢] ∼ ):𝑉–onto→(𝑉 / ∼ ))
17		qusgrp2.1	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)
18	17	3expb 1206	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
19		qusgrp2.e	. . . 4 ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞)))
20	4, 11, 3, 18, 19	ercpbl 13134	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑎) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑝) ∧ ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑏) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑞)) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘(𝑎 + 𝑏)) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘(𝑝 + 𝑞))))
21	4	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ∼ Er 𝑉)
22		qusgrp2.2	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) ∼ (𝑥 + (𝑦 + 𝑧)))
23	21, 22	erthi 6667	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → [((𝑥 + 𝑦) + 𝑧)] ∼ = [(𝑥 + (𝑦 + 𝑧))] ∼ )
24	11	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑉 ∈ V)
25	21, 22	ercl 6630	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) ∈ 𝑉)
26	21, 24, 3, 25	divsfvalg 13132	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘((𝑥 + 𝑦) + 𝑧)) = [((𝑥 + 𝑦) + 𝑧)] ∼ )
27	21, 22	ercl2 6632	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + (𝑦 + 𝑧)) ∈ 𝑉)
28	21, 24, 3, 27	divsfvalg 13132	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘(𝑥 + (𝑦 + 𝑧))) = [(𝑥 + (𝑦 + 𝑧))] ∼ )
29	23, 26, 28	3eqtr4d 2247	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘((𝑥 + 𝑦) + 𝑧)) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘(𝑥 + (𝑦 + 𝑧))))
30		qusgrp2.3	. . 3 ⊢ (𝜑 → 0 ∈ 𝑉)
31	4	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ∼ Er 𝑉)
32		qusgrp2.4	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) ∼ 𝑥)
33	31, 32	erthi 6667	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → [( 0 + 𝑥)] ∼ = [𝑥] ∼ )
34	11	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑉 ∈ V)
35	31, 32	ercl 6630	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) ∈ 𝑉)
36	31, 34, 3, 35	divsfvalg 13132	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘( 0 + 𝑥)) = [( 0 + 𝑥)] ∼ )
37		simpr 110	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
38	31, 34, 3, 37	divsfvalg 13132	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑥) = [𝑥] ∼ )
39	33, 36, 38	3eqtr4d 2247	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘( 0 + 𝑥)) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘𝑥))
40		qusgrp2.5	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)
41		qusgrp2.6	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) ∼ 0 )
42	31, 41	ersym 6631	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ∼ (𝑁 + 𝑥))
43	31, 42	erthi 6667	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → [ 0 ] ∼ = [(𝑁 + 𝑥)] ∼ )
44	30	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ∈ 𝑉)
45	31, 34, 3, 44	divsfvalg 13132	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘ 0 ) = [ 0 ] ∼ )
46	31, 41	ercl 6630	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) ∈ 𝑉)
47	31, 34, 3, 46	divsfvalg 13132	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘(𝑁 + 𝑥)) = [(𝑁 + 𝑥)] ∼ )
48	43, 45, 47	3eqtr4rd 2248	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘(𝑁 + 𝑥)) = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘ 0 ))
49	14, 2, 15, 16, 20, 6, 17, 29, 30, 39, 40, 48	imasgrp2 13417	. 2 ⊢ (𝜑 → (𝑈 ∈ Grp ∧ ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘ 0 ) = (0g‘𝑈)))
50	4, 11, 3, 30	divsfvalg 13132	. . . . 5 ⊢ (𝜑 → ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘ 0 ) = [ 0 ] ∼ )
51	50	eqcomd 2210	. . . 4 ⊢ (𝜑 → [ 0 ] ∼ = ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘ 0 ))
52	51	eqeq1d 2213	. . 3 ⊢ (𝜑 → ([ 0 ] ∼ = (0g‘𝑈) ↔ ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘ 0 ) = (0g‘𝑈)))
53	52	anbi2d 464	. 2 ⊢ (𝜑 → ((𝑈 ∈ Grp ∧ [ 0 ] ∼ = (0g‘𝑈)) ↔ (𝑈 ∈ Grp ∧ ((𝑢 ∈ 𝑉 ↦ [𝑢] ∼ )‘ 0 ) = (0g‘𝑈))))
54	49, 53	mpbird 167	1 ⊢ (𝜑 → (𝑈 ∈ Grp ∧ [ 0 ] ∼ = (0g‘𝑈)))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980   = wceq 1372   ∈ wcel 2175  Vcvv 2771   class class class wbr 4043   ↦ cmpt 4104   Fn wfn 5265  ‘cfv 5270  (class class class)co 5943   Er wer 6616  [cec 6617   / cqs 6618  Basecbs 12803  +_gcplusg 12880  0_gc0g 13059   /_s cqus 13103  Grpcgrp 13303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-coll 4158  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4479  ax-setind 4584  ax-cnex 8015  ax-resscn 8016  ax-1cn 8017  ax-1re 8018  ax-icn 8019  ax-addcl 8020  ax-addrcl 8021  ax-mulcl 8022  ax-addcom 8024  ax-addass 8026  ax-i2m1 8029  ax-0lt1 8030  ax-0id 8032  ax-rnegex 8033  ax-pre-ltirr 8036  ax-pre-lttrn 8038  ax-pre-ltadd 8040

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-reu 2490  df-rmo 2491  df-rab 2492  df-v 2773  df-sbc 2998  df-csb 3093  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-nul 3460  df-pw 3617  df-sn 3638  df-pr 3639  df-tp 3640  df-op 3641  df-uni 3850  df-int 3885  df-iun 3928  df-br 4044  df-opab 4105  df-mpt 4106  df-id 4339  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-rn 4685  df-res 4686  df-ima 4687  df-iota 5231  df-fun 5272  df-fn 5273  df-f 5274  df-f1 5275  df-fo 5276  df-f1o 5277  df-fv 5278  df-riota 5898  df-ov 5946  df-oprab 5947  df-mpo 5948  df-er 6619  df-ec 6621  df-qs 6625  df-pnf 8108  df-mnf 8109  df-ltxr 8111  df-inn 9036  df-2 9094  df-3 9095  df-ndx 12806  df-slot 12807  df-base 12809  df-plusg 12893  df-mulr 12894  df-0g 13061  df-iimas 13105  df-qus 13106  df-mgm 13159  df-sgrp 13205  df-mnd 13220  df-grp 13306

This theorem is referenced by:  qusgrp  13539