imasgrp2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > imasgrp2		GIF version

Theorem imasgrp2 13240

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 12950	. . 3 ⊢ (𝜑 → 𝐵 = (Base‘𝑈))
6		eqidd 2197	. . 3 ⊢ (𝜑 → (+_g‘𝑈) = (+_g‘𝑈))
7		imasgrp.e	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))
8		imasgrp.p	. . . . . . . . . 10 ⊢ (𝜑 → + = (+_g‘𝑅))
9	8	oveqd 5939	. . . . . . . . 9 ⊢ (𝜑 → (𝑎 + 𝑏) = (𝑎(+_g‘𝑅)𝑏))
10	9	fveq2d 5562	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑎(+_g‘𝑅)𝑏)))
11	8	oveqd 5939	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 + 𝑞) = (𝑝(+_g‘𝑅)𝑞))
12	11	fveq2d 5562	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑝 + 𝑞)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞)))
13	10, 12	eqeq12d 2211	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
14	13	3ad2ant1 1020	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
15	7, 14	sylibd 149	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎(+_g‘𝑅)𝑏)) = (𝐹‘(𝑝(+_g‘𝑅)𝑞))))
16		eqid 2196	. . . . 5 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
17		eqid 2196	. . . . 5 ⊢ (+_g‘𝑈) = (+_g‘𝑈)
18	11	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) = (𝑝(+_g‘𝑅)𝑞))
19		imasgrp2.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)
20	19	3expb 1206	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
21	20	caovclg 6076	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) ∈ 𝑉)
22	18, 21	eqeltrrd 2274	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝(+_g‘𝑅)𝑞) ∈ 𝑉)
23	3, 15, 1, 2, 4, 16, 17, 22	imasaddf 12962	. . . 4 ⊢ (𝜑 → (+_g‘𝑈):(𝐵 × 𝐵)⟶𝐵)
24		fovcdm 6066	. . . 4 ⊢ (((+_g‘𝑈):(𝐵 × 𝐵)⟶𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+_g‘𝑈)𝑣) ∈ 𝐵)
25	23, 24	syl3an1 1282	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+_g‘𝑈)𝑣) ∈ 𝐵)
26		forn 5483	. . . . . . . . . 10 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
27	3, 26	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 = 𝐵)
28	27	eleq2d 2266	. . . . . . . 8 ⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ 𝑢 ∈ 𝐵))
29	27	eleq2d 2266	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ ran 𝐹 ↔ 𝑣 ∈ 𝐵))
30	27	eleq2d 2266	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ ran 𝐹 ↔ 𝑤 ∈ 𝐵))
31	28, 29, 30	3anbi123d 1323	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))
32		fofn 5482	. . . . . . . . 9 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉)
33	3, 32	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝑉)
34		fvelrnb 5608	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
35		fvelrnb 5608	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣))
36		fvelrnb 5608	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))
37	34, 35, 36	3anbi123d 1323	. . . . . . . 8 ⊢ (𝐹 Fn 𝑉 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
38	33, 37	syl 14	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
39	31, 38	bitr3d 190	. . . . . 6 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)))
40		3reeanv 2668	. . . . . 6 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))
41	39, 40	bitr4di 198	. . . . 5 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤)))
42		imasgrp2.2	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧))))
43	8	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → + = (+_g‘𝑅))
44	43	oveqd 5939	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) = ((𝑥 + 𝑦)(+_g‘𝑅)𝑧))
45	44	fveq2d 5562	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
46	43	oveqd 5939	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + (𝑦 + 𝑧)) = (𝑥(+_g‘𝑅)(𝑦 + 𝑧)))
47	46	fveq2d 5562	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + (𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
48	42, 45, 47	3eqtr3d 2237	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
49		simpl 109	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝜑)
50	19	3adant3r3 1216	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉)
51		simpr3 1007	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ 𝑉)
52	3, 15, 1, 2, 4, 16, 17	imasaddval 12961	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 + 𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
53	49, 50, 51, 52	syl3anc 1249	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+_g‘𝑅)𝑧)))
54		simpr1 1005	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑥 ∈ 𝑉)
55	21	caovclg 6076	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉)
56	55	3adantr1 1158	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉)
57	3, 15, 1, 2, 4, 16, 17	imasaddval 12961	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝑦 + 𝑧) ∈ 𝑉) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
58	49, 54, 56, 57	syl3anc 1249	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+_g‘𝑅)(𝑦 + 𝑧))))
59	48, 53, 58	3eqtr4d 2239	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))))
60	3, 15, 1, 2, 4, 16, 17	imasaddval 12961	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
61	60	3adant3r3 1216	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
62	43	oveqd 5939	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) = (𝑥(+_g‘𝑅)𝑦))
63	62	fveq2d 5562	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑥(+_g‘𝑅)𝑦)))
64	61, 63	eqtr4d 2232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥 + 𝑦)))
65	64	oveq1d 5937	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘(𝑥 + 𝑦))(+_g‘𝑈)(𝐹‘𝑧)))
66	3, 15, 1, 2, 4, 16, 17	imasaddval 12961	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
67	66	3adant3r1 1214	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
68	43	oveqd 5939	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) = (𝑦(+_g‘𝑅)𝑧))
69	68	fveq2d 5562	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑦 + 𝑧)) = (𝐹‘(𝑦(+_g‘𝑅)𝑧)))
70	67, 69	eqtr4d 2232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦 + 𝑧)))
71	70	oveq2d 5938	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) = ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘(𝑦 + 𝑧))))
72	59, 65, 71	3eqtr4d 2239	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))))
73		simp1 999	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑥) = 𝑢)
74		simp2 1000	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑦) = 𝑣)
75	73, 74	oveq12d 5940	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦)) = (𝑢(+_g‘𝑈)𝑣))
76		simp3 1001	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑧) = 𝑤)
77	75, 76	oveq12d 5940	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤))
78	74, 76	oveq12d 5940	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧)) = (𝑣(+_g‘𝑈)𝑤))
79	73, 78	oveq12d 5940	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))
80	77, 79	eqeq12d 2211	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((((𝐹‘𝑥)(+_g‘𝑈)(𝐹‘𝑦))(+_g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+_g‘𝑈)((𝐹‘𝑦)(+_g‘𝑈)(𝐹‘𝑧))) ↔ ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
81	72, 80	syl5ibcom 155	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
82	81	3exp2 1227	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝑉 → (𝑦 ∈ 𝑉 → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))))))
83	82	imp32 257	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))))
84	83	rexlimdv 2613	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
85	84	rexlimdvva 2622	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
86	41, 85	sylbid 150	. . . 4 ⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤))))
87	86	imp 124	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝑈)𝑣)(+_g‘𝑈)𝑤) = (𝑢(+_g‘𝑈)(𝑣(+_g‘𝑈)𝑤)))
88		fof 5480	. . . . 5 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
89	3, 88	syl 14	. . . 4 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
90		imasgrp2.3	. . . 4 ⊢ (𝜑 → 0 ∈ 𝑉)
91	89, 90	ffvelcdmd 5698	. . 3 ⊢ (𝜑 → (𝐹‘ 0 ) ∈ 𝐵)
92	33, 34	syl 14	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
93	28, 92	bitr3d 190	. . . . 5 ⊢ (𝜑 → (𝑢 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢))
94		simpl 109	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝜑)
95	90	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ∈ 𝑉)
96		simpr 110	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉)
97	3, 15, 1, 2, 4, 16, 17	imasaddval 12961	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
98	94, 95, 96, 97	syl3anc 1249	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
99	8	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → + = (+_g‘𝑅))
100	99	oveqd 5939	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) = ( 0 (+_g‘𝑅)𝑥))
101	100	fveq2d 5562	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘( 0 (+_g‘𝑅)𝑥)))
102		imasgrp2.4	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥))
103	98, 101, 102	3eqtr2d 2235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥))
104		oveq2 5930	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘ 0 )(+_g‘𝑈)𝑢))
105		id 19	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → (𝐹‘𝑥) = 𝑢)
106	104, 105	eqeq12d 2211	. . . . . . 7 ⊢ ((𝐹‘𝑥) = 𝑢 → (((𝐹‘ 0 )(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥) ↔ ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
107	103, 106	syl5ibcom 155	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
108	107	rexlimdva 2614	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
109	93, 108	sylbid 150	. . . 4 ⊢ (𝜑 → (𝑢 ∈ 𝐵 → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢))
110	109	imp 124	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ((𝐹‘ 0 )(+_g‘𝑈)𝑢) = 𝑢)
111	89	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝐹:𝑉⟶𝐵)
112		imasgrp2.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)
113	111, 112	ffvelcdmd 5698	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘𝑁) ∈ 𝐵)
114	3, 15, 1, 2, 4, 16, 17	imasaddval 12961	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
115	94, 112, 96, 114	syl3anc 1249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
116	99	oveqd 5939	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) = (𝑁(+_g‘𝑅)𝑥))
117	116	fveq2d 5562	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘(𝑁(+_g‘𝑅)𝑥)))
118		imasgrp2.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘ 0 ))
119	115, 117, 118	3eqtr2d 2235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
120		oveq1 5929	. . . . . . . . . 10 ⊢ (𝑣 = (𝐹‘𝑁) → (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)))
121	120	eqeq1d 2205	. . . . . . . . 9 ⊢ (𝑣 = (𝐹‘𝑁) → ((𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )))
122	121	rspcev 2868	. . . . . . . 8 ⊢ (((𝐹‘𝑁) ∈ 𝐵 ∧ ((𝐹‘𝑁)(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
123	113, 119, 122	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))
124		oveq2 5930	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) = 𝑢 → (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝑣(+_g‘𝑈)𝑢))
125	124	eqeq1d 2205	. . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑢 → ((𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
126	125	rexbidv 2498	. . . . . . 7 ⊢ ((𝐹‘𝑥) = 𝑢 → (∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
127	123, 126	syl5ibcom 155	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
128	127	rexlimdva 2614	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
129	93, 128	sylbid 150	. . . 4 ⊢ (𝜑 → (𝑢 ∈ 𝐵 → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 )))
130	129	imp 124	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝐵 (𝑣(+_g‘𝑈)𝑢) = (𝐹‘ 0 ))
131	5, 6, 25, 87, 91, 110, 130	isgrpde 13154	. 2 ⊢ (𝜑 → 𝑈 ∈ Grp)
132	5, 6, 91, 110, 131	grpidd2 13173	. 2 ⊢ (𝜑 → (𝐹‘ 0 ) = (0_g‘𝑈))
133	131, 132	jca 306	1 ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0_g‘𝑈)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 980 = wceq 1364 ∈ wcel 2167 ∃wrex 2476 × cxp 4661 ran crn 4664 Fn wfn 5253 ⟶wf 5254 –onto→wfo 5256 ‘cfv 5258 (class class class)co 5922 Basecbs 12678 +_gcplusg 12755 0_gc0g 12927 “_s cimas 12942 Grpcgrp 13132

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-addcom 7979 ax-addass 7981 ax-i2m1 7984 ax-0lt1 7985 ax-0id 7987 ax-rnegex 7988 ax-pre-ltirr 7991 ax-pre-lttrn 7993 ax-pre-ltadd 7995

This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-pw 3607 df-sn 3628 df-pr 3629 df-tp 3630 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-id 4328 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-pnf 8063 df-mnf 8064 df-ltxr 8066 df-inn 8991 df-2 9049 df-3 9050 df-ndx 12681 df-slot 12682 df-base 12684 df-plusg 12768 df-mulr 12769 df-0g 12929 df-iimas 12945 df-mgm 12999 df-sgrp 13045 df-mnd 13058 df-grp 13135

This theorem is referenced by: imasgrp 13241 qusgrp2 13243

W3C validator