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 18690

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 17223	. . 3 ⊢ (𝜑 → 𝐵 = (Base‘𝑈))
6		eqidd 2739	. . 3 ⊢ (𝜑 → (+_g‘𝑈) = (+_g‘𝑈))
7		imasgrp.e	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))
8		imasgrp.p	. . . . . . . . . 10 ⊢ (𝜑 → + = (+_g‘𝑅))
9	8	oveqd 7292	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 + 𝑏) = (𝑎(+_g‘𝑅)𝑏))
10	9	fveq2d 6778	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑎(+_g‘𝑅)𝑏)))
11	8	oveqd 7292	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 + 𝑞) = (𝑝(+_g‘𝑅)𝑞))
12	11	fveq2d 6778	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑝 + 𝑞)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞)))
13	10, 12	eqeq12d 2754	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
14	13	3ad2ant1 1132	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
15	7, 14	sylibd 238	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
16		eqid 2738	. . . . 5 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
17		eqid 2738	. . . . 5 ⊢ (+_g‘𝑈) = (+_g‘𝑈)
18	11	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) = (𝑝(+_g‘𝑅)𝑞))
19		imasgrp2.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)
20	19	3expb 1119	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
21	20	caovclg 7464	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) ∈ 𝑉)
22	18, 21	eqeltrrd 2840	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝(+_g‘𝑅)𝑞) ∈ 𝑉)
23	3, 15, 1, 2, 4, 16, 17, 22	imasaddf 17244	. . . 4 ⊢ (𝜑 → (+_g‘𝑈):(𝐵 × 𝐵)⟶𝐵)
24		fovrn 7442	. . . 4 ⊢ (((+_g‘𝑈):(𝐵 × 𝐵)⟶𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+_g‘𝑈)𝑣) ∈ 𝐵)
25	23, 24	syl3an1 1162	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+_g‘𝑈)𝑣) ∈ 𝐵)
26		forn 6691	. . . . . . . . . 10 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
27	3, 26	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 = 𝐵)
28	27	eleq2d 2824	. . . . . . . 8 ⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ 𝑢 ∈ 𝐵))
29	27	eleq2d 2824	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ ran 𝐹 ↔ 𝑣 ∈ 𝐵))
30	27	eleq2d 2824	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ ran 𝐹 ↔ 𝑤 ∈ 𝐵))
31	28, 29, 30	3anbi123d 1435	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))
32		fofn 6690	. . . . . . . . 9 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉)
33	3, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝑉)
34		fvelrnb 6830	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
35		fvelrnb 6830	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣))
36		fvelrnb 6830	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))
37	34, 35, 36	3anbi123d 1435	. . . . . . . 8 ⊢ (𝐹 Fn 𝑉 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
38	33, 37	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
39	31, 38	bitr3d 280	. . . . . 6 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
40		3reeanv 3295	. . . . . 6 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))
41	39, 40	bitr4di 289	. . . . 5 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤)))
42		imasgrp2.2	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧))))
43	8	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → + = (+_g‘𝑅))
44	43	oveqd 7292	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) = ((𝑥 + 𝑦)(+_g‘𝑅)𝑧))
45	44	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
46	43	oveqd 7292	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + (𝑦 + 𝑧)) = (𝑥(+_g‘𝑅)(𝑦 + 𝑧)))
47	46	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + (𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
48	42, 45, 47	3eqtr3d 2786	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
49		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝜑)
50	19	3adant3r3 1183	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
51		simpr3 1195	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ 𝑉)
52	3, 15, 1, 2, 4, 16, 17	imasaddval 17243	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 + 𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
53	49, 50, 51, 52	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
54		simpr1 1193	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑥 ∈ 𝑉)
55	21	caovclg 7464	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉)
56	55	3adantr1 1168	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉)
57	3, 15, 1, 2, 4, 16, 17	imasaddval 17243	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝑦 + 𝑧) ∈ 𝑉) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
58	49, 54, 56, 57	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
59	48, 53, 58	3eqtr4d 2788	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))))
60	3, 15, 1, 2, 4, 16, 17	imasaddval 17243	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
61	60	3adant3r3 1183	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
62	43	oveqd 7292	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) = (𝑥(+_g‘𝑅)𝑦))
63	62	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
64	61, 63	eqtr4d 2781	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥 + 𝑦)))
65	64	oveq1d 7290	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)))
66	3, 15, 1, 2, 4, 16, 17	imasaddval 17243	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
67	66	3adant3r1 1181	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
68	43	oveqd 7292	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) = (𝑦(+_g‘𝑅)𝑧))
69	68	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑦 + 𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
70	67, 69	eqtr4d 2781	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦 + 𝑧)))
71	70	oveq2d 7291	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) = ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))))
72	59, 65, 71	3eqtr4d 2788	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))))
73		simp1 1135	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑥) = 𝑢)
74		simp2 1136	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑦) = 𝑣)
75	73, 74	oveq12d 7293	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝑢(+_g‘𝑈)𝑣))
76		simp3 1137	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑧) = 𝑤)
77	75, 76	oveq12d 7293	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤))
78	74, 76	oveq12d 7293	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝑣(+_g‘𝑈)𝑤))
79	73, 78	oveq12d 7293	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))
80	77, 79	eqeq12d 2754	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) ↔ ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
81	72, 80	syl5ibcom 244	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
82	81	3exp2 1353	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝑉 → (𝑦 ∈ 𝑉 → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))))))
83	82	imp32 419	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))))
84	83	rexlimdv 3212	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
85	84	rexlimdvva 3223	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
86	41, 85	sylbid 239	. . . 4 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
87	86	imp 407	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))
88		fof 6688	. . . . 5 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
89	3, 88	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
90		imasgrp2.3	. . . 4 ⊢ (𝜑 → 0 ∈ 𝑉)
91	89, 90	ffvelrnd 6962	. . 3 ⊢ (𝜑 → (𝐹‘ 0 ) ∈ 𝐵)
92	33, 34	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
93	28, 92	bitr3d 280	. . . . 5 ⊢ (𝜑 → (𝑢 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
94		simpl 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝜑)
95	90	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ∈ 𝑉)
96		simpr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
97	3, 15, 1, 2, 4, 16, 17	imasaddval 17243	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
98	94, 95, 96, 97	syl3anc 1370	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
99	8	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → + = (+_g‘𝑅))
100	99	oveqd 7292	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) = ( 0 (+_g‘𝑅)𝑥))
101	100	fveq2d 6778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
102		imasgrp2.4	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥))
103	98, 101, 102	3eqtr2d 2784	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥))
104		oveq2 7283	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘ 0 )(+_g‘𝑈)𝑢))
105		id 22	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → (𝐹‘𝑥) = 𝑢)
106	104, 105	eqeq12d 2754	. . . . . . 7 ⊢ ((𝐹‘𝑥) = 𝑢 → (((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥) ↔ ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
107	103, 106	syl5ibcom 244	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
108	107	rexlimdva 3213	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
109	93, 108	sylbid 239	. . . 4 ⊢ (𝜑 → (𝑢 ∈ 𝐵 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
110	109	imp 407	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢)
111	89	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝐹:𝑉⟶𝐵)
112		imasgrp2.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)
113	111, 112	ffvelrnd 6962	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘𝑁) ∈ 𝐵)
114	3, 15, 1, 2, 4, 16, 17	imasaddval 17243	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
115	94, 112, 96, 114	syl3anc 1370	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
116	99	oveqd 7292	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) = (𝑁(+_g‘𝑅)𝑥))
117	116	fveq2d 6778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
118		imasgrp2.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘ 0 ))
119	115, 117, 118	3eqtr2d 2784	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
120		oveq1 7282	. . . . . . . . . 10 ⊢ (𝑣 = (𝐹‘𝑁) → (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)))
121	120	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑣 = (𝐹‘𝑁) → ((𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )))
122	121	rspcev 3561	. . . . . . . 8 ⊢ (((𝐹‘𝑁) ∈ 𝐵 ∧ ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
123	113, 119, 122	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
124		oveq2 7283	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) = 𝑢 → (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝑣(+_g‘𝑈)𝑢))
125	124	eqeq1d 2740	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → ((𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
126	125	rexbidv 3226	. . . . . . 7 ⊢ ((𝐹‘𝑥) = 𝑢 → (∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
127	123, 126	syl5ibcom 244	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
128	127	rexlimdva 3213	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
129	93, 128	sylbid 239	. . . 4 ⊢ (𝜑 → (𝑢 ∈ 𝐵 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
130	129	imp 407	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 ))
131	5, 6, 25, 87, 91, 110, 130	isgrpde 18600	. 2 ⊢ (𝜑 → 𝑈 ∈ Grp)
132	5, 6, 91, 110, 131	grpidd2 18617	. 2 ⊢ (𝜑 → (𝐹‘ 0 ) = (0_g‘𝑈))
133	131, 132	jca 512	1 ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0_g‘𝑈)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∃wrex 3065 × cxp 5587 ran crn 5590 Fn wfn 6428 ⟶wf 6429 –onto→wfo 6431 ‘cfv 6433 (class class class)co 7275 Basecbs 16912 +_gcplusg 16962 0_gc0g 17150 “_s cimas 17215 Grpcgrp 18577

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-sup 9201 df-inf 9202 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-fz 13240 df-struct 16848 df-slot 16883 df-ndx 16895 df-base 16913 df-plusg 16975 df-mulr 16976 df-sca 16978 df-vsca 16979 df-ip 16980 df-tset 16981 df-ple 16982 df-ds 16984 df-0g 17152 df-imas 17219 df-mgm 18326 df-sgrp 18375 df-mnd 18386 df-grp 18580

This theorem is referenced by: imasgrp 18691 qusgrp2 18693

W3C validator