imasgrp2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > imasgrp2		Structured version Visualization version GIF version

Theorem imasgrp2 18938

Description: The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.)

**Hypotheses**
Ref	Expression
imasgrp.u	⊢ (𝜑 → 𝑈 = (𝐹 “_s 𝑅))
imasgrp.v	⊢ (𝜑 → 𝑉 = (Base‘𝑅))
imasgrp.p	⊢ (𝜑 → + = (+_g‘𝑅))
imasgrp.f	⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
imasgrp.e	⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))
imasgrp2.r	⊢ (𝜑 → 𝑅 ∈ 𝑊)
imasgrp2.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)
imasgrp2.2	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧))))
imasgrp2.3	⊢ (𝜑 → 0 ∈ 𝑉)
imasgrp2.4	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥))
imasgrp2.5	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)
imasgrp2.6	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘ 0 ))

**Assertion**
Ref	Expression
imasgrp2	⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0_g‘𝑈)))

Distinct variable groups: 𝑞,𝑝,𝑥,𝐵 𝑁,𝑝 𝑎,𝑏,𝑝,𝑞,𝑥,𝑦,𝑧,𝜑 𝑅,𝑝,𝑞 𝐹,𝑎,𝑏,𝑝,𝑞,𝑥,𝑦,𝑧 + ,𝑝,𝑞,𝑥,𝑦 𝑈,𝑎,𝑏,𝑝,𝑞,𝑥,𝑦,𝑧 𝑉,𝑎,𝑏,𝑝,𝑞,𝑥,𝑦,𝑧 0 ,𝑝,𝑞,𝑥 Allowed substitution hints: 𝐵(𝑦,𝑧,𝑎,𝑏) + (𝑧,𝑎,𝑏) 𝑅(𝑥,𝑦,𝑧,𝑎,𝑏) 𝑁(𝑥,𝑦,𝑧,𝑞,𝑎,𝑏) 𝑊(𝑥,𝑦,𝑧,𝑞,𝑝,𝑎,𝑏) 0 (𝑦,𝑧,𝑎,𝑏)

Proof of Theorem imasgrp2 Dummy variables 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		imasgrp.u	. . . 4 ⊢ (𝜑 → 𝑈 = (𝐹 “_s 𝑅))
2		imasgrp.v	. . . 4 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
3		imasgrp.f	. . . 4 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
4		imasgrp2.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑊)
5	1, 2, 3, 4	imasbas 17458	. . 3 ⊢ (𝜑 → 𝐵 = (Base‘𝑈))
6		eqidd 2734	. . 3 ⊢ (𝜑 → (+_g‘𝑈) = (+_g‘𝑈))
7		imasgrp.e	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))
8		imasgrp.p	. . . . . . . . . 10 ⊢ (𝜑 → + = (+_g‘𝑅))
9	8	oveqd 7426	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 + 𝑏) = (𝑎(+_g‘𝑅)𝑏))
10	9	fveq2d 6896	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑎(+_g‘𝑅)𝑏)))
11	8	oveqd 7426	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 + 𝑞) = (𝑝(+_g‘𝑅)𝑞))
12	11	fveq2d 6896	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑝 + 𝑞)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞)))
13	10, 12	eqeq12d 2749	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
14	13	3ad2ant1 1134	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
15	7, 14	sylibd 238	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
16		eqid 2733	. . . . 5 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
17		eqid 2733	. . . . 5 ⊢ (+_g‘𝑈) = (+_g‘𝑈)
18	11	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) = (𝑝(+_g‘𝑅)𝑞))
19		imasgrp2.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)
20	19	3expb 1121	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
21	20	caovclg 7599	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) ∈ 𝑉)
22	18, 21	eqeltrrd 2835	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝(+_g‘𝑅)𝑞) ∈ 𝑉)
23	3, 15, 1, 2, 4, 16, 17, 22	imasaddf 17479	. . . 4 ⊢ (𝜑 → (+_g‘𝑈):(𝐵 × 𝐵)⟶𝐵)
24		fovcdm 7577	. . . 4 ⊢ (((+_g‘𝑈):(𝐵 × 𝐵)⟶𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+_g‘𝑈)𝑣) ∈ 𝐵)
25	23, 24	syl3an1 1164	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+_g‘𝑈)𝑣) ∈ 𝐵)
26		forn 6809	. . . . . . . . . 10 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
27	3, 26	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 = 𝐵)
28	27	eleq2d 2820	. . . . . . . 8 ⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ 𝑢 ∈ 𝐵))
29	27	eleq2d 2820	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ ran 𝐹 ↔ 𝑣 ∈ 𝐵))
30	27	eleq2d 2820	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ ran 𝐹 ↔ 𝑤 ∈ 𝐵))
31	28, 29, 30	3anbi123d 1437	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))
32		fofn 6808	. . . . . . . . 9 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉)
33	3, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝑉)
34		fvelrnb 6953	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
35		fvelrnb 6953	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣))
36		fvelrnb 6953	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))
37	34, 35, 36	3anbi123d 1437	. . . . . . . 8 ⊢ (𝐹 Fn 𝑉 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
38	33, 37	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
39	31, 38	bitr3d 281	. . . . . 6 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
40		3reeanv 3228	. . . . . 6 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))
41	39, 40	bitr4di 289	. . . . 5 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤)))
42		imasgrp2.2	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧))))
43	8	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → + = (+_g‘𝑅))
44	43	oveqd 7426	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) = ((𝑥 + 𝑦)(+_g‘𝑅)𝑧))
45	44	fveq2d 6896	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
46	43	oveqd 7426	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + (𝑦 + 𝑧)) = (𝑥(+_g‘𝑅)(𝑦 + 𝑧)))
47	46	fveq2d 6896	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + (𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
48	42, 45, 47	3eqtr3d 2781	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
49		simpl 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝜑)
50	19	3adant3r3 1185	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
51		simpr3 1197	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ 𝑉)
52	3, 15, 1, 2, 4, 16, 17	imasaddval 17478	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 + 𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
53	49, 50, 51, 52	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
54		simpr1 1195	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑥 ∈ 𝑉)
55	21	caovclg 7599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉)
56	55	3adantr1 1170	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉)
57	3, 15, 1, 2, 4, 16, 17	imasaddval 17478	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝑦 + 𝑧) ∈ 𝑉) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
58	49, 54, 56, 57	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
59	48, 53, 58	3eqtr4d 2783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))))
60	3, 15, 1, 2, 4, 16, 17	imasaddval 17478	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
61	60	3adant3r3 1185	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
62	43	oveqd 7426	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) = (𝑥(+_g‘𝑅)𝑦))
63	62	fveq2d 6896	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
64	61, 63	eqtr4d 2776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥 + 𝑦)))
65	64	oveq1d 7424	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)))
66	3, 15, 1, 2, 4, 16, 17	imasaddval 17478	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
67	66	3adant3r1 1183	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
68	43	oveqd 7426	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) = (𝑦(+_g‘𝑅)𝑧))
69	68	fveq2d 6896	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑦 + 𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
70	67, 69	eqtr4d 2776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦 + 𝑧)))
71	70	oveq2d 7425	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) = ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))))
72	59, 65, 71	3eqtr4d 2783	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))))
73		simp1 1137	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑥) = 𝑢)
74		simp2 1138	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑦) = 𝑣)
75	73, 74	oveq12d 7427	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝑢(+_g‘𝑈)𝑣))
76		simp3 1139	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑧) = 𝑤)
77	75, 76	oveq12d 7427	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤))
78	74, 76	oveq12d 7427	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝑣(+_g‘𝑈)𝑤))
79	73, 78	oveq12d 7427	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))
80	77, 79	eqeq12d 2749	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) ↔ ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
81	72, 80	syl5ibcom 244	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
82	81	3exp2 1355	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝑉 → (𝑦 ∈ 𝑉 → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))))))
83	82	imp32 420	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))))
84	83	rexlimdv 3154	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
85	84	rexlimdvva 3212	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
86	41, 85	sylbid 239	. . . 4 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
87	86	imp 408	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))
88		fof 6806	. . . . 5 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
89	3, 88	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
90		imasgrp2.3	. . . 4 ⊢ (𝜑 → 0 ∈ 𝑉)
91	89, 90	ffvelcdmd 7088	. . 3 ⊢ (𝜑 → (𝐹‘ 0 ) ∈ 𝐵)
92	33, 34	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
93	28, 92	bitr3d 281	. . . . 5 ⊢ (𝜑 → (𝑢 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
94		simpl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝜑)
95	90	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ∈ 𝑉)
96		simpr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
97	3, 15, 1, 2, 4, 16, 17	imasaddval 17478	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
98	94, 95, 96, 97	syl3anc 1372	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
99	8	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → + = (+_g‘𝑅))
100	99	oveqd 7426	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) = ( 0 (+_g‘𝑅)𝑥))
101	100	fveq2d 6896	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
102		imasgrp2.4	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥))
103	98, 101, 102	3eqtr2d 2779	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥))
104		oveq2 7417	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘ 0 )(+_g‘𝑈)𝑢))
105		id 22	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → (𝐹‘𝑥) = 𝑢)
106	104, 105	eqeq12d 2749	. . . . . . 7 ⊢ ((𝐹‘𝑥) = 𝑢 → (((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥) ↔ ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
107	103, 106	syl5ibcom 244	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
108	107	rexlimdva 3156	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
109	93, 108	sylbid 239	. . . 4 ⊢ (𝜑 → (𝑢 ∈ 𝐵 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
110	109	imp 408	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢)
111	89	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝐹:𝑉⟶𝐵)
112		imasgrp2.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)
113	111, 112	ffvelcdmd 7088	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘𝑁) ∈ 𝐵)
114	3, 15, 1, 2, 4, 16, 17	imasaddval 17478	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
115	94, 112, 96, 114	syl3anc 1372	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
116	99	oveqd 7426	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) = (𝑁(+_g‘𝑅)𝑥))
117	116	fveq2d 6896	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
118		imasgrp2.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘ 0 ))
119	115, 117, 118	3eqtr2d 2779	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
120		oveq1 7416	. . . . . . . . . 10 ⊢ (𝑣 = (𝐹‘𝑁) → (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)))
121	120	eqeq1d 2735	. . . . . . . . 9 ⊢ (𝑣 = (𝐹‘𝑁) → ((𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )))
122	121	rspcev 3613	. . . . . . . 8 ⊢ (((𝐹‘𝑁) ∈ 𝐵 ∧ ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
123	113, 119, 122	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
124		oveq2 7417	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) = 𝑢 → (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝑣(+_g‘𝑈)𝑢))
125	124	eqeq1d 2735	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → ((𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
126	125	rexbidv 3179	. . . . . . 7 ⊢ ((𝐹‘𝑥) = 𝑢 → (∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
127	123, 126	syl5ibcom 244	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
128	127	rexlimdva 3156	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
129	93, 128	sylbid 239	. . . 4 ⊢ (𝜑 → (𝑢 ∈ 𝐵 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
130	129	imp 408	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 ))
131	5, 6, 25, 87, 91, 110, 130	isgrpde 18843	. 2 ⊢ (𝜑 → 𝑈 ∈ Grp)
132	5, 6, 91, 110, 131	grpidd2 18862	. 2 ⊢ (𝜑 → (𝐹‘ 0 ) = (0_g‘𝑈))
133	131, 132	jca 513	1 ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0_g‘𝑈)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∃wrex 3071 × cxp 5675 ran crn 5678 Fn wfn 6539 ⟶wf 6540 –onto→wfo 6542 ‘cfv 6544 (class class class)co 7409 Basecbs 17144 +_gcplusg 17197 0_gc0g 17385 “_s cimas 17450 Grpcgrp 18819

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9437 df-inf 9438 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-nn 12213 df-2 12275 df-3 12276 df-4 12277 df-5 12278 df-6 12279 df-7 12280 df-8 12281 df-9 12282 df-n0 12473 df-z 12559 df-dec 12678 df-uz 12823 df-fz 13485 df-struct 17080 df-slot 17115 df-ndx 17127 df-base 17145 df-plusg 17210 df-mulr 17211 df-sca 17213 df-vsca 17214 df-ip 17215 df-tset 17216 df-ple 17217 df-ds 17219 df-0g 17387 df-imas 17454 df-mgm 18561 df-sgrp 18610 df-mnd 18626 df-grp 18822

This theorem is referenced by: imasgrp 18939 qusgrp2 18941

W3C validator