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 19277

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 17696	. . 3 ⊢ (𝜑 → 𝐵 = (Base‘𝑈))
6		eqidd 2764	. . 3 ⊢ (𝜑 → (+_g‘𝑈) = (+_g‘𝑈))
7		imasgrp.e	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))
8		imasgrp.p	. . . . . . . . . 10 ⊢ (𝜑 → + = (+_g‘𝑅))
9	8	oveqd 7444	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 + 𝑏) = (𝑎(+_g‘𝑅)𝑏))
10	9	fveq2d 6897	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑎(+_g‘𝑅)𝑏)))
11	8	oveqd 7444	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 + 𝑞) = (𝑝(+_g‘𝑅)𝑞))
12	11	fveq2d 6897	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑝 + 𝑞)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞)))
13	10, 12	eqeq12d 2779	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
14	13	3ad2ant1 1151	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
15	7, 14	sylibd 242	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
16		eqid 2763	. . . . 5 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
17		eqid 2763	. . . . 5 ⊢ (+_g‘𝑈) = (+_g‘𝑈)
18	11	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) = (𝑝(+_g‘𝑅)𝑞))
19		imasgrp2.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)
20	19	3expb 1138	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
21	20	caovclg 7620	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) ∈ 𝑉)
22	18, 21	eqeltrrd 2864	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝(+_g‘𝑅)𝑞) ∈ 𝑉)
23	3, 15, 1, 2, 4, 16, 17, 22	imasaddf 17717	. . . 4 ⊢ (𝜑 → (+_g‘𝑈):(𝐵 × 𝐵)⟶𝐵)
24		fovcdm 7598	. . . 4 ⊢ (((+_g‘𝑈):(𝐵 × 𝐵)⟶𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+_g‘𝑈)𝑣) ∈ 𝐵)
25	23, 24	syl3an1 1181	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+_g‘𝑈)𝑣) ∈ 𝐵)
26		forn 6807	. . . . . . . . . 10 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
27	3, 26	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 = 𝐵)
28	27	eleq2d 2849	. . . . . . . 8 ⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ 𝑢 ∈ 𝐵))
29	27	eleq2d 2849	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ ran 𝐹 ↔ 𝑣 ∈ 𝐵))
30	27	eleq2d 2849	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ ran 𝐹 ↔ 𝑤 ∈ 𝐵))
31	28, 29, 30	3anbi123d 1464	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))
32		fofn 6806	. . . . . . . . 9 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉)
33	3, 32	syl 18	. . . . . . . 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 1464	. . . . . . . 8 ⊢ (𝐹 Fn 𝑉 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
38	33, 37	syl 18	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
39	31, 38	bitr3d 284	. . . . . 6 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
40		3reeanv 3238	. . . . . 6 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))
41	39, 40	bitr4di 292	. . . . 5 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤)))
42		imasgrp2.2	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧))))
43	8	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → + = (+_g‘𝑅))
44	43	oveqd 7444	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) = ((𝑥 + 𝑦)(+_g‘𝑅)𝑧))
45	44	fveq2d 6897	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
46	43	oveqd 7444	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + (𝑦 + 𝑧)) = (𝑥(+_g‘𝑅)(𝑦 + 𝑧)))
47	46	fveq2d 6897	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + (𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
48	42, 45, 47	3eqtr3d 2806	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
49		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝜑)
50	19	3adant3r3 1203	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
51		simpr3 1215	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ 𝑉)
52	3, 15, 1, 2, 4, 16, 17	imasaddval 17716	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 + 𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
53	49, 50, 51, 52	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
54		simpr1 1213	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑥 ∈ 𝑉)
55	21	caovclg 7620	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉)
56	55	3adantr1 1188	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉)
57	3, 15, 1, 2, 4, 16, 17	imasaddval 17716	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝑦 + 𝑧) ∈ 𝑉) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
58	49, 54, 56, 57	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
59	48, 53, 58	3eqtr4d 2808	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))))
60	3, 15, 1, 2, 4, 16, 17	imasaddval 17716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
61	60	3adant3r3 1203	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
62	43	oveqd 7444	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) = (𝑥(+_g‘𝑅)𝑦))
63	62	fveq2d 6897	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
64	61, 63	eqtr4d 2801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥 + 𝑦)))
65	64	oveq1d 7442	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)))
66	3, 15, 1, 2, 4, 16, 17	imasaddval 17716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
67	66	3adant3r1 1201	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
68	43	oveqd 7444	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) = (𝑦(+_g‘𝑅)𝑧))
69	68	fveq2d 6897	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑦 + 𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
70	67, 69	eqtr4d 2801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦 + 𝑧)))
71	70	oveq2d 7443	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) = ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))))
72	59, 65, 71	3eqtr4d 2808	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))))
73		simp1 1154	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑥) = 𝑢)
74		simp2 1155	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑦) = 𝑣)
75	73, 74	oveq12d 7445	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝑢(+_g‘𝑈)𝑣))
76		simp3 1156	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑧) = 𝑤)
77	75, 76	oveq12d 7445	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤))
78	74, 76	oveq12d 7445	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝑣(+_g‘𝑈)𝑤))
79	73, 78	oveq12d 7445	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))
80	77, 79	eqeq12d 2779	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) ↔ ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
81	72, 80	syl5ibcom 248	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
82	81	3exp2 1373	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝑉 → (𝑦 ∈ 𝑉 → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))))))
83	82	imp32 424	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))))
84	83	rexlimdv 3164	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
85	84	rexlimdvva 3222	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
86	41, 85	sylbid 243	. . . 4 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
87	86	imp 412	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))
88		fof 6804	. . . . 5 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
89	3, 88	syl 18	. . . 4 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
90		imasgrp2.3	. . . 4 ⊢ (𝜑 → 0 ∈ 𝑉)
91	89, 90	ffvelcdmd 7093	. . 3 ⊢ (𝜑 → (𝐹‘ 0 ) ∈ 𝐵)
92	33, 34	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
93	28, 92	bitr3d 284	. . . . 5 ⊢ (𝜑 → (𝑢 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
94		simpl 488	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝜑)
95	90	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ∈ 𝑉)
96		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
97	3, 15, 1, 2, 4, 16, 17	imasaddval 17716	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
98	94, 95, 96, 97	syl3anc 1398	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
99	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → + = (+_g‘𝑅))
100	99	oveqd 7444	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) = ( 0 (+_g‘𝑅)𝑥))
101	100	fveq2d 6897	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
102		imasgrp2.4	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥))
103	98, 101, 102	3eqtr2d 2804	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥))
104		oveq2 7435	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘ 0 )(+_g‘𝑈)𝑢))
105		id 23	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → (𝐹‘𝑥) = 𝑢)
106	104, 105	eqeq12d 2779	. . . . . . 7 ⊢ ((𝐹‘𝑥) = 𝑢 → (((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥) ↔ ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
107	103, 106	syl5ibcom 248	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
108	107	rexlimdva 3166	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
109	93, 108	sylbid 243	. . . 4 ⊢ (𝜑 → (𝑢 ∈ 𝐵 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
110	109	imp 412	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢)
111	89	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝐹:𝑉⟶𝐵)
112		imasgrp2.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)
113	111, 112	ffvelcdmd 7093	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘𝑁) ∈ 𝐵)
114	3, 15, 1, 2, 4, 16, 17	imasaddval 17716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
115	94, 112, 96, 114	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
116	99	oveqd 7444	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) = (𝑁(+_g‘𝑅)𝑥))
117	116	fveq2d 6897	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
118		imasgrp2.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘ 0 ))
119	115, 117, 118	3eqtr2d 2804	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
120		oveq1 7434	. . . . . . . . . 10 ⊢ (𝑣 = (𝐹‘𝑁) → (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)))
121	120	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑣 = (𝐹‘𝑁) → ((𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )))
122	121	rspcev 3579	. . . . . . . 8 ⊢ (((𝐹‘𝑁) ∈ 𝐵 ∧ ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
123	113, 119, 122	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
124		oveq2 7435	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) = 𝑢 → (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝑣(+_g‘𝑈)𝑢))
125	124	eqeq1d 2765	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → ((𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
126	125	rexbidv 3189	. . . . . . 7 ⊢ ((𝐹‘𝑥) = 𝑢 → (∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
127	123, 126	syl5ibcom 248	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
128	127	rexlimdva 3166	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
129	93, 128	sylbid 243	. . . 4 ⊢ (𝜑 → (𝑢 ∈ 𝐵 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
130	129	imp 412	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 ))
131	5, 6, 25, 87, 91, 110, 130	isgrpde 19180	. 2 ⊢ (𝜑 → 𝑈 ∈ Grp)
132	5, 6, 91, 110, 131	grpidd2 19200	. 2 ⊢ (𝜑 → (𝐹‘ 0 ) = (0_g‘𝑈))
133	131, 132	jca 521	1 ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0_g‘𝑈)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2146 ∃wrex 3089 × cxp 5652 ran crn 5655 Fn wfn 6541 ⟶wf 6542 –onto→wfo 6544 ‘cfv 6546 (class class class)co 7427 Basecbs 17399 +_gcplusg 17440 0_gc0g 17622 “_s cimas 17688 Grpcgrp 19156

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5234 ax-sep 5251 ax-nul 5262 ax-pow 5330 ax-pr 5394 ax-un 7758 ax-cnex 11266 ax-resscn 11267 ax-1cn 11268 ax-icn 11269 ax-addcl 11270 ax-addrcl 11271 ax-mulcl 11272 ax-mulrcl 11273 ax-mulcom 11274 ax-addass 11275 ax-mulass 11276 ax-distr 11277 ax-i2m1 11278 ax-1ne0 11279 ax-1rid 11280 ax-rnegex 11281 ax-rrecex 11282 ax-cnre 11283 ax-pre-lttri 11284 ax-pre-lttrn 11285 ax-pre-ltadd 11286 ax-pre-mulgt0 11287

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-pss 4016 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-pw 4561 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4838 df-uni 4870 df-iun 4955 df-br 5106 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5549 df-eprel 5554 df-po 5562 df-so 5563 df-fr 5607 df-we 5609 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6310 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-riota 7384 df-ov 7430 df-oprab 7431 df-mpo 7432 df-om 7885 df-1st 8008 df-2nd 8009 df-frecs 8310 df-wrecs 8341 df-recs 8390 df-rdg 8429 df-1o 8487 df-er 8728 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-sup 9444 df-inf 9445 df-pnf 11355 df-mnf 11356 df-xr 11357 df-ltxr 11358 df-le 11359 df-sub 11553 df-neg 11554 df-nn 12346 df-2 12415 df-3 12416 df-4 12417 df-5 12418 df-6 12419 df-7 12420 df-8 12421 df-9 12422 df-n0 12617 df-z 12704 df-dec 12825 df-uz 12976 df-fz 13650 df-struct 17337 df-slot 17372 df-ndx 17384 df-base 17400 df-plusg 17453 df-mulr 17454 df-sca 17456 df-vsca 17457 df-ip 17458 df-tset 17459 df-ple 17460 df-ds 17462 df-0g 17624 df-imas 17692 df-mgm 18828 df-sgrp 18920 df-mnd 18936 df-grp 19159

This theorem is used by: imasgrp 19278 qusgrp2 19280

W3C validator