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 19025

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 17470	. . 3 ⊢ (𝜑 → 𝐵 = (Base‘𝑈))
6		eqidd 2738	. . 3 ⊢ (𝜑 → (+_g‘𝑈) = (+_g‘𝑈))
7		imasgrp.e	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))
8		imasgrp.p	. . . . . . . . . 10 ⊢ (𝜑 → + = (+_g‘𝑅))
9	8	oveqd 7378	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 + 𝑏) = (𝑎(+_g‘𝑅)𝑏))
10	9	fveq2d 6839	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑎(+_g‘𝑅)𝑏)))
11	8	oveqd 7378	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 + 𝑞) = (𝑝(+_g‘𝑅)𝑞))
12	11	fveq2d 6839	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑝 + 𝑞)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞)))
13	10, 12	eqeq12d 2753	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
14	13	3ad2ant1 1134	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
15	7, 14	sylibd 239	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
16		eqid 2737	. . . . 5 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
17		eqid 2737	. . . . 5 ⊢ (+_g‘𝑈) = (+_g‘𝑈)
18	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) = (𝑝(+_g‘𝑅)𝑞))
19		imasgrp2.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)
20	19	3expb 1121	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
21	20	caovclg 7553	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) ∈ 𝑉)
22	18, 21	eqeltrrd 2838	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝(+_g‘𝑅)𝑞) ∈ 𝑉)
23	3, 15, 1, 2, 4, 16, 17, 22	imasaddf 17491	. . . 4 ⊢ (𝜑 → (+_g‘𝑈):(𝐵 × 𝐵)⟶𝐵)
24		fovcdm 7531	. . . 4 ⊢ (((+_g‘𝑈):(𝐵 × 𝐵)⟶𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+_g‘𝑈)𝑣) ∈ 𝐵)
25	23, 24	syl3an1 1164	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+_g‘𝑈)𝑣) ∈ 𝐵)
26		forn 6750	. . . . . . . . . 10 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
27	3, 26	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 = 𝐵)
28	27	eleq2d 2823	. . . . . . . 8 ⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ 𝑢 ∈ 𝐵))
29	27	eleq2d 2823	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ ran 𝐹 ↔ 𝑣 ∈ 𝐵))
30	27	eleq2d 2823	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ ran 𝐹 ↔ 𝑤 ∈ 𝐵))
31	28, 29, 30	3anbi123d 1439	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))
32		fofn 6749	. . . . . . . . 9 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉)
33	3, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝑉)
34		fvelrnb 6895	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
35		fvelrnb 6895	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣))
36		fvelrnb 6895	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))
37	34, 35, 36	3anbi123d 1439	. . . . . . . 8 ⊢ (𝐹 Fn 𝑉 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
38	33, 37	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
39	31, 38	bitr3d 281	. . . . . 6 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
40		3reeanv 3211	. . . . . 6 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))
41	39, 40	bitr4di 289	. . . . 5 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤)))
42		imasgrp2.2	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧))))
43	8	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → + = (+_g‘𝑅))
44	43	oveqd 7378	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) = ((𝑥 + 𝑦)(+_g‘𝑅)𝑧))
45	44	fveq2d 6839	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
46	43	oveqd 7378	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + (𝑦 + 𝑧)) = (𝑥(+_g‘𝑅)(𝑦 + 𝑧)))
47	46	fveq2d 6839	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + (𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
48	42, 45, 47	3eqtr3d 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
49		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝜑)
50	19	3adant3r3 1186	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
51		simpr3 1198	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ 𝑉)
52	3, 15, 1, 2, 4, 16, 17	imasaddval 17490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 + 𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
53	49, 50, 51, 52	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
54		simpr1 1196	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑥 ∈ 𝑉)
55	21	caovclg 7553	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉)
56	55	3adantr1 1171	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉)
57	3, 15, 1, 2, 4, 16, 17	imasaddval 17490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝑦 + 𝑧) ∈ 𝑉) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
58	49, 54, 56, 57	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
59	48, 53, 58	3eqtr4d 2782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))))
60	3, 15, 1, 2, 4, 16, 17	imasaddval 17490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
61	60	3adant3r3 1186	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
62	43	oveqd 7378	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) = (𝑥(+_g‘𝑅)𝑦))
63	62	fveq2d 6839	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
64	61, 63	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥 + 𝑦)))
65	64	oveq1d 7376	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)))
66	3, 15, 1, 2, 4, 16, 17	imasaddval 17490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
67	66	3adant3r1 1184	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
68	43	oveqd 7378	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) = (𝑦(+_g‘𝑅)𝑧))
69	68	fveq2d 6839	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑦 + 𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
70	67, 69	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦 + 𝑧)))
71	70	oveq2d 7377	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) = ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))))
72	59, 65, 71	3eqtr4d 2782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))))
73		simp1 1137	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑥) = 𝑢)
74		simp2 1138	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑦) = 𝑣)
75	73, 74	oveq12d 7379	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝑢(+_g‘𝑈)𝑣))
76		simp3 1139	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑧) = 𝑤)
77	75, 76	oveq12d 7379	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤))
78	74, 76	oveq12d 7379	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝑣(+_g‘𝑈)𝑤))
79	73, 78	oveq12d 7379	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))
80	77, 79	eqeq12d 2753	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) ↔ ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
81	72, 80	syl5ibcom 245	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
82	81	3exp2 1356	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝑉 → (𝑦 ∈ 𝑉 → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))))))
83	82	imp32 418	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))))
84	83	rexlimdv 3137	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
85	84	rexlimdvva 3195	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
86	41, 85	sylbid 240	. . . 4 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
87	86	imp 406	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))
88		fof 6747	. . . . 5 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
89	3, 88	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
90		imasgrp2.3	. . . 4 ⊢ (𝜑 → 0 ∈ 𝑉)
91	89, 90	ffvelcdmd 7032	. . 3 ⊢ (𝜑 → (𝐹‘ 0 ) ∈ 𝐵)
92	33, 34	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
93	28, 92	bitr3d 281	. . . . 5 ⊢ (𝜑 → (𝑢 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
94		simpl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝜑)
95	90	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ∈ 𝑉)
96		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
97	3, 15, 1, 2, 4, 16, 17	imasaddval 17490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
98	94, 95, 96, 97	syl3anc 1374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
99	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → + = (+_g‘𝑅))
100	99	oveqd 7378	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) = ( 0 (+_g‘𝑅)𝑥))
101	100	fveq2d 6839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
102		imasgrp2.4	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥))
103	98, 101, 102	3eqtr2d 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥))
104		oveq2 7369	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘ 0 )(+_g‘𝑈)𝑢))
105		id 22	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → (𝐹‘𝑥) = 𝑢)
106	104, 105	eqeq12d 2753	. . . . . . 7 ⊢ ((𝐹‘𝑥) = 𝑢 → (((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥) ↔ ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
107	103, 106	syl5ibcom 245	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
108	107	rexlimdva 3139	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
109	93, 108	sylbid 240	. . . 4 ⊢ (𝜑 → (𝑢 ∈ 𝐵 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
110	109	imp 406	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢)
111	89	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝐹:𝑉⟶𝐵)
112		imasgrp2.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)
113	111, 112	ffvelcdmd 7032	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘𝑁) ∈ 𝐵)
114	3, 15, 1, 2, 4, 16, 17	imasaddval 17490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
115	94, 112, 96, 114	syl3anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
116	99	oveqd 7378	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) = (𝑁(+_g‘𝑅)𝑥))
117	116	fveq2d 6839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
118		imasgrp2.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘ 0 ))
119	115, 117, 118	3eqtr2d 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
120		oveq1 7368	. . . . . . . . . 10 ⊢ (𝑣 = (𝐹‘𝑁) → (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)))
121	120	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑣 = (𝐹‘𝑁) → ((𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )))
122	121	rspcev 3565	. . . . . . . 8 ⊢ (((𝐹‘𝑁) ∈ 𝐵 ∧ ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
123	113, 119, 122	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
124		oveq2 7369	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) = 𝑢 → (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝑣(+_g‘𝑈)𝑢))
125	124	eqeq1d 2739	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → ((𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
126	125	rexbidv 3162	. . . . . . 7 ⊢ ((𝐹‘𝑥) = 𝑢 → (∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
127	123, 126	syl5ibcom 245	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
128	127	rexlimdva 3139	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
129	93, 128	sylbid 240	. . . 4 ⊢ (𝜑 → (𝑢 ∈ 𝐵 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
130	129	imp 406	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 ))
131	5, 6, 25, 87, 91, 110, 130	isgrpde 18927	. 2 ⊢ (𝜑 → 𝑈 ∈ Grp)
132	5, 6, 91, 110, 131	grpidd2 18947	. 2 ⊢ (𝜑 → (𝐹‘ 0 ) = (0_g‘𝑈))
133	131, 132	jca 511	1 ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0_g‘𝑈)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∃wrex 3062 × cxp 5623 ran crn 5626 Fn wfn 6488 ⟶wf 6489 –onto→wfo 6491 ‘cfv 6493 (class class class)co 7361 Basecbs 17173 +_gcplusg 17214 0_gc0g 17396 “_s cimas 17462 Grpcgrp 18903

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7812 df-1st 7936 df-2nd 7937 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-sup 9349 df-inf 9350 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-7 12243 df-8 12244 df-9 12245 df-n0 12432 df-z 12519 df-dec 12639 df-uz 12783 df-fz 13456 df-struct 17111 df-slot 17146 df-ndx 17158 df-base 17174 df-plusg 17227 df-mulr 17228 df-sca 17230 df-vsca 17231 df-ip 17232 df-tset 17233 df-ple 17234 df-ds 17236 df-0g 17398 df-imas 17466 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-grp 18906

This theorem is referenced by: imasgrp 19026 qusgrp2 19028

W3C validator