psgnghm - Metamath Proof Explorer

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

Theorem psgnghm 19745

Description: The sign is a homomorphism from the finitary permutation group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015.)

**Hypotheses**
Ref	Expression
psgnghm.s	⊢ 𝑆 = (SymGrp‘𝐷)
psgnghm.n	⊢ 𝑁 = (pmSgn‘𝐷)
psgnghm.f	⊢ 𝐹 = (𝑆 ↾_s dom 𝑁)
psgnghm.u	⊢ 𝑈 = ((mulGrp‘ℂ_fld) ↾_s {1, -1})

**Assertion**
Ref	Expression
psgnghm	⊢ (𝐷 ∈ 𝑉 → 𝑁 ∈ (𝐹 GrpHom 𝑈))

Proof of Theorem psgnghm Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		psgnghm.s	. . . . . 6 ⊢ 𝑆 = (SymGrp‘𝐷)
2		eqid 2610	. . . . . 6 ⊢ (Base‘𝑆) = (Base‘𝑆)
3		eqid 2610	. . . . . 6 ⊢ {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} = {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin}
4		psgnghm.n	. . . . . 6 ⊢ 𝑁 = (pmSgn‘𝐷)
5	1, 2, 3, 4	psgnfn 17744	. . . . 5 ⊢ 𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin}
6		fndm 5904	. . . . 5 ⊢ (𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} → dom 𝑁 = {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin})
7	5, 6	ax-mp 5	. . . 4 ⊢ dom 𝑁 = {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin}
8		ssrab2 3650	. . . 4 ⊢ {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} ⊆ (Base‘𝑆)
9	7, 8	eqsstri 3598	. . 3 ⊢ dom 𝑁 ⊆ (Base‘𝑆)
10		psgnghm.f	. . . 4 ⊢ 𝐹 = (𝑆 ↾_s dom 𝑁)
11	10, 2	ressbas2 15758	. . 3 ⊢ (dom 𝑁 ⊆ (Base‘𝑆) → dom 𝑁 = (Base‘𝐹))
12	9, 11	ax-mp 5	. 2 ⊢ dom 𝑁 = (Base‘𝐹)
13		psgnghm.u	. . 3 ⊢ 𝑈 = ((mulGrp‘ℂ_fld) ↾_s {1, -1})
14	13	cnmsgnbas 19743	. 2 ⊢ {1, -1} = (Base‘𝑈)
15		fvex 6113	. . . 4 ⊢ (Base‘𝐹) ∈ V
16	12, 15	eqeltri 2684	. . 3 ⊢ dom 𝑁 ∈ V
17		eqid 2610	. . . 4 ⊢ (+_g‘𝑆) = (+_g‘𝑆)
18	10, 17	ressplusg 15818	. . 3 ⊢ (dom 𝑁 ∈ V → (+_g‘𝑆) = (+_g‘𝐹))
19	16, 18	ax-mp 5	. 2 ⊢ (+_g‘𝑆) = (+_g‘𝐹)
20		prex 4836	. . 3 ⊢ {1, -1} ∈ V
21		eqid 2610	. . . . 5 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
22		cnfldmul 19573	. . . . 5 ⊢ · = (._r‘ℂ_fld)
23	21, 22	mgpplusg 18316	. . . 4 ⊢ · = (+_g‘(mulGrp‘ℂ_fld))
24	13, 23	ressplusg 15818	. . 3 ⊢ ({1, -1} ∈ V → · = (+_g‘𝑈))
25	20, 24	ax-mp 5	. 2 ⊢ · = (+_g‘𝑈)
26	1, 4	psgndmsubg 17745	. . 3 ⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝑆))
27	10	subggrp 17420	. . 3 ⊢ (dom 𝑁 ∈ (SubGrp‘𝑆) → 𝐹 ∈ Grp)
28	26, 27	syl 17	. 2 ⊢ (𝐷 ∈ 𝑉 → 𝐹 ∈ Grp)
29	13	cnmsgngrp 19744	. . 3 ⊢ 𝑈 ∈ Grp
30	29	a1i 11	. 2 ⊢ (𝐷 ∈ 𝑉 → 𝑈 ∈ Grp)
31		fnfun 5902	. . . . . 6 ⊢ (𝑁 Fn {𝑥 ∈ (Base‘𝑆) ∣ dom (𝑥 ∖ I ) ∈ Fin} → Fun 𝑁)
32	5, 31	ax-mp 5	. . . . 5 ⊢ Fun 𝑁
33		funfn 5833	. . . . 5 ⊢ (Fun 𝑁 ↔ 𝑁 Fn dom 𝑁)
34	32, 33	mpbi 219	. . . 4 ⊢ 𝑁 Fn dom 𝑁
35	34	a1i 11	. . 3 ⊢ (𝐷 ∈ 𝑉 → 𝑁 Fn dom 𝑁)
36		eqid 2610	. . . . . 6 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
37	1, 36, 4	psgnvali 17751	. . . . 5 ⊢ (𝑥 ∈ dom 𝑁 → ∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σ_g 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))))
38		lencl 13179	. . . . . . . . . . 11 ⊢ (𝑧 ∈ Word ran (pmTrsp‘𝐷) → (#‘𝑧) ∈ ℕ₀)
39	38	nn0zd 11356	. . . . . . . . . 10 ⊢ (𝑧 ∈ Word ran (pmTrsp‘𝐷) → (#‘𝑧) ∈ ℤ)
40		m1expcl2 12744	. . . . . . . . . . 11 ⊢ ((#‘𝑧) ∈ ℤ → (-1↑(#‘𝑧)) ∈ {-1, 1})
41		prcom 4211	. . . . . . . . . . 11 ⊢ {-1, 1} = {1, -1}
42	40, 41	syl6eleq 2698	. . . . . . . . . 10 ⊢ ((#‘𝑧) ∈ ℤ → (-1↑(#‘𝑧)) ∈ {1, -1})
43	39, 42	syl 17	. . . . . . . . 9 ⊢ (𝑧 ∈ Word ran (pmTrsp‘𝐷) → (-1↑(#‘𝑧)) ∈ {1, -1})
44	43	adantl 481	. . . . . . . 8 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran (pmTrsp‘𝐷)) → (-1↑(#‘𝑧)) ∈ {1, -1})
45		eleq1a 2683	. . . . . . . 8 ⊢ ((-1↑(#‘𝑧)) ∈ {1, -1} → ((𝑁‘𝑥) = (-1↑(#‘𝑧)) → (𝑁‘𝑥) ∈ {1, -1}))
46	44, 45	syl 17	. . . . . . 7 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran (pmTrsp‘𝐷)) → ((𝑁‘𝑥) = (-1↑(#‘𝑧)) → (𝑁‘𝑥) ∈ {1, -1}))
47	46	adantld 482	. . . . . 6 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran (pmTrsp‘𝐷)) → ((𝑥 = (𝑆 Σ_g 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) → (𝑁‘𝑥) ∈ {1, -1}))
48	47	rexlimdva 3013	. . . . 5 ⊢ (𝐷 ∈ 𝑉 → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σ_g 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) → (𝑁‘𝑥) ∈ {1, -1}))
49	37, 48	syl5 33	. . . 4 ⊢ (𝐷 ∈ 𝑉 → (𝑥 ∈ dom 𝑁 → (𝑁‘𝑥) ∈ {1, -1}))
50	49	ralrimiv 2948	. . 3 ⊢ (𝐷 ∈ 𝑉 → ∀𝑥 ∈ dom 𝑁(𝑁‘𝑥) ∈ {1, -1})
51		ffnfv 6295	. . 3 ⊢ (𝑁:dom 𝑁⟶{1, -1} ↔ (𝑁 Fn dom 𝑁 ∧ ∀𝑥 ∈ dom 𝑁(𝑁‘𝑥) ∈ {1, -1}))
52	35, 50, 51	sylanbrc 695	. 2 ⊢ (𝐷 ∈ 𝑉 → 𝑁:dom 𝑁⟶{1, -1})
53	1, 36, 4	psgnvali 17751	. . . . . 6 ⊢ (𝑦 ∈ dom 𝑁 → ∃𝑤 ∈ Word ran (pmTrsp‘𝐷)(𝑦 = (𝑆 Σ_g 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤))))
54	37, 53	anim12i 588	. . . . 5 ⊢ ((𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁) → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σ_g 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ ∃𝑤 ∈ Word ran (pmTrsp‘𝐷)(𝑦 = (𝑆 Σ_g 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))))
55		reeanv 3086	. . . . 5 ⊢ (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σ_g 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ (𝑦 = (𝑆 Σ_g 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) ↔ (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)(𝑥 = (𝑆 Σ_g 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ ∃𝑤 ∈ Word ran (pmTrsp‘𝐷)(𝑦 = (𝑆 Σ_g 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))))
56	54, 55	sylibr 223	. . . 4 ⊢ ((𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁) → ∃𝑧 ∈ Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σ_g 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ (𝑦 = (𝑆 Σ_g 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))))
57		ccatcl 13212	. . . . . . . 8 ⊢ ((𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷)) → (𝑧 ++ 𝑤) ∈ Word ran (pmTrsp‘𝐷))
58	1, 36, 4	psgnvalii 17752	. . . . . . . 8 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ++ 𝑤) ∈ Word ran (pmTrsp‘𝐷)) → (𝑁‘(𝑆 Σ_g (𝑧 ++ 𝑤))) = (-1↑(#‘(𝑧 ++ 𝑤))))
59	57, 58	sylan2 490	. . . . . . 7 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘(𝑆 Σ_g (𝑧 ++ 𝑤))) = (-1↑(#‘(𝑧 ++ 𝑤))))
60	1	symggrp 17643	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Grp)
61		grpmnd 17252	. . . . . . . . . . 11 ⊢ (𝑆 ∈ Grp → 𝑆 ∈ Mnd)
62	60, 61	syl 17	. . . . . . . . . 10 ⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Mnd)
63	36, 1, 2	symgtrf 17712	. . . . . . . . . . . 12 ⊢ ran (pmTrsp‘𝐷) ⊆ (Base‘𝑆)
64		sswrd 13168	. . . . . . . . . . . 12 ⊢ (ran (pmTrsp‘𝐷) ⊆ (Base‘𝑆) → Word ran (pmTrsp‘𝐷) ⊆ Word (Base‘𝑆))
65	63, 64	ax-mp 5	. . . . . . . . . . 11 ⊢ Word ran (pmTrsp‘𝐷) ⊆ Word (Base‘𝑆)
66	65	sseli 3564	. . . . . . . . . 10 ⊢ (𝑧 ∈ Word ran (pmTrsp‘𝐷) → 𝑧 ∈ Word (Base‘𝑆))
67	65	sseli 3564	. . . . . . . . . 10 ⊢ (𝑤 ∈ Word ran (pmTrsp‘𝐷) → 𝑤 ∈ Word (Base‘𝑆))
68	2, 17	gsumccat 17201	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Mnd ∧ 𝑧 ∈ Word (Base‘𝑆) ∧ 𝑤 ∈ Word (Base‘𝑆)) → (𝑆 Σ_g (𝑧 ++ 𝑤)) = ((𝑆 Σ_g 𝑧)(+_g‘𝑆)(𝑆 Σ_g 𝑤)))
69	62, 66, 67, 68	syl3an 1360	. . . . . . . . 9 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷)) → (𝑆 Σ_g (𝑧 ++ 𝑤)) = ((𝑆 Σ_g 𝑧)(+_g‘𝑆)(𝑆 Σ_g 𝑤)))
70	69	3expb 1258	. . . . . . . 8 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑆 Σ_g (𝑧 ++ 𝑤)) = ((𝑆 Σ_g 𝑧)(+_g‘𝑆)(𝑆 Σ_g 𝑤)))
71	70	fveq2d 6107	. . . . . . 7 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘(𝑆 Σ_g (𝑧 ++ 𝑤))) = (𝑁‘((𝑆 Σ_g 𝑧)(+_g‘𝑆)(𝑆 Σ_g 𝑤))))
72		ccatlen 13213	. . . . . . . . . 10 ⊢ ((𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷)) → (#‘(𝑧 ++ 𝑤)) = ((#‘𝑧) + (#‘𝑤)))
73	72	adantl 481	. . . . . . . . 9 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (#‘(𝑧 ++ 𝑤)) = ((#‘𝑧) + (#‘𝑤)))
74	73	oveq2d 6565	. . . . . . . 8 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (-1↑(#‘(𝑧 ++ 𝑤))) = (-1↑((#‘𝑧) + (#‘𝑤))))
75		neg1cn 11001	. . . . . . . . . 10 ⊢ -1 ∈ ℂ
76	75	a1i 11	. . . . . . . . 9 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → -1 ∈ ℂ)
77		lencl 13179	. . . . . . . . . 10 ⊢ (𝑤 ∈ Word ran (pmTrsp‘𝐷) → (#‘𝑤) ∈ ℕ₀)
78	77	ad2antll 761	. . . . . . . . 9 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (#‘𝑤) ∈ ℕ₀)
79	38	ad2antrl 760	. . . . . . . . 9 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (#‘𝑧) ∈ ℕ₀)
80	76, 78, 79	expaddd 12872	. . . . . . . 8 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (-1↑((#‘𝑧) + (#‘𝑤))) = ((-1↑(#‘𝑧)) · (-1↑(#‘𝑤))))
81	74, 80	eqtrd 2644	. . . . . . 7 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (-1↑(#‘(𝑧 ++ 𝑤))) = ((-1↑(#‘𝑧)) · (-1↑(#‘𝑤))))
82	59, 71, 81	3eqtr3d 2652	. . . . . 6 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (𝑁‘((𝑆 Σ_g 𝑧)(+_g‘𝑆)(𝑆 Σ_g 𝑤))) = ((-1↑(#‘𝑧)) · (-1↑(#‘𝑤))))
83		oveq12 6558	. . . . . . . . 9 ⊢ ((𝑥 = (𝑆 Σ_g 𝑧) ∧ 𝑦 = (𝑆 Σ_g 𝑤)) → (𝑥(+_g‘𝑆)𝑦) = ((𝑆 Σ_g 𝑧)(+_g‘𝑆)(𝑆 Σ_g 𝑤)))
84	83	fveq2d 6107	. . . . . . . 8 ⊢ ((𝑥 = (𝑆 Σ_g 𝑧) ∧ 𝑦 = (𝑆 Σ_g 𝑤)) → (𝑁‘(𝑥(+_g‘𝑆)𝑦)) = (𝑁‘((𝑆 Σ_g 𝑧)(+_g‘𝑆)(𝑆 Σ_g 𝑤))))
85		oveq12 6558	. . . . . . . 8 ⊢ (((𝑁‘𝑥) = (-1↑(#‘𝑧)) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤))) → ((𝑁‘𝑥) · (𝑁‘𝑦)) = ((-1↑(#‘𝑧)) · (-1↑(#‘𝑤))))
86	84, 85	eqeqan12d 2626	. . . . . . 7 ⊢ (((𝑥 = (𝑆 Σ_g 𝑧) ∧ 𝑦 = (𝑆 Σ_g 𝑤)) ∧ ((𝑁‘𝑥) = (-1↑(#‘𝑧)) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) → ((𝑁‘(𝑥(+_g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)) ↔ (𝑁‘((𝑆 Σ_g 𝑧)(+_g‘𝑆)(𝑆 Σ_g 𝑤))) = ((-1↑(#‘𝑧)) · (-1↑(#‘𝑤)))))
87	86	an4s 865	. . . . . 6 ⊢ (((𝑥 = (𝑆 Σ_g 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ (𝑦 = (𝑆 Σ_g 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) → ((𝑁‘(𝑥(+_g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)) ↔ (𝑁‘((𝑆 Σ_g 𝑧)(+_g‘𝑆)(𝑆 Σ_g 𝑤))) = ((-1↑(#‘𝑧)) · (-1↑(#‘𝑤)))))
88	82, 87	syl5ibrcom 236	. . . . 5 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑧 ∈ Word ran (pmTrsp‘𝐷) ∧ 𝑤 ∈ Word ran (pmTrsp‘𝐷))) → (((𝑥 = (𝑆 Σ_g 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ (𝑦 = (𝑆 Σ_g 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) → (𝑁‘(𝑥(+_g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦))))
89	88	rexlimdvva 3020	. . . 4 ⊢ (𝐷 ∈ 𝑉 → (∃𝑧 ∈ Word ran (pmTrsp‘𝐷)∃𝑤 ∈ Word ran (pmTrsp‘𝐷)((𝑥 = (𝑆 Σ_g 𝑧) ∧ (𝑁‘𝑥) = (-1↑(#‘𝑧))) ∧ (𝑦 = (𝑆 Σ_g 𝑤) ∧ (𝑁‘𝑦) = (-1↑(#‘𝑤)))) → (𝑁‘(𝑥(+_g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦))))
90	56, 89	syl5 33	. . 3 ⊢ (𝐷 ∈ 𝑉 → ((𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁) → (𝑁‘(𝑥(+_g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦))))
91	90	imp 444	. 2 ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑥 ∈ dom 𝑁 ∧ 𝑦 ∈ dom 𝑁)) → (𝑁‘(𝑥(+_g‘𝑆)𝑦)) = ((𝑁‘𝑥) · (𝑁‘𝑦)))
92	12, 14, 19, 25, 28, 30, 52, 91	isghmd 17492	1 ⊢ (𝐷 ∈ 𝑉 → 𝑁 ∈ (𝐹 GrpHom 𝑈))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 {crab 2900 Vcvv 3173 ∖ cdif 3537 ⊆ wss 3540 {cpr 4127 I cid 4948 dom cdm 5038 ran crn 5039 Fun wfun 5798 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 Fincfn 7841 ℂcc 9813 1c1 9816 + caddc 9818 · cmul 9820 -cneg 10146 ℕ₀cn0 11169 ℤcz 11254 ↑cexp 12722 #chash 12979 Word cword 13146 ++ cconcat 13148 Basecbs 15695 ↾_s cress 15696 +_gcplusg 15768 Σ_g cgsu 15924 Mndcmnd 17117 Grpcgrp 17245 SubGrpcsubg 17411 GrpHom cghm 17480 SymGrpcsymg 17620 pmTrspcpmtr 17684 pmSgncpsgn 17732 mulGrpcmgp 18312 ℂ_fldccnfld 19567

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-addf 9894 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-xor 1457 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-ot 4134 df-uni 4373 df-int 4411 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-tpos 7239 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-xnn0 11241 df-z 11255 df-dec 11370 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-seq 12664 df-exp 12723 df-hash 12980 df-word 13154 df-lsw 13155 df-concat 13156 df-s1 13157 df-substr 13158 df-splice 13159 df-reverse 13160 df-s2 13444 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-starv 15783 df-tset 15787 df-ple 15788 df-ds 15791 df-unif 15792 df-0g 15925 df-gsum 15926 df-mre 16069 df-mrc 16070 df-acs 16072 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-mhm 17158 df-submnd 17159 df-grp 17248 df-minusg 17249 df-subg 17414 df-ghm 17481 df-gim 17524 df-oppg 17599 df-symg 17621 df-pmtr 17685 df-psgn 17734 df-cmn 18018 df-abl 18019 df-mgp 18313 df-ur 18325 df-ring 18372 df-cring 18373 df-oppr 18446 df-dvdsr 18464 df-unit 18465 df-invr 18495 df-dvr 18506 df-drng 18572 df-cnfld 19568

This theorem is referenced by: psgnghm2 19746 evpmss 19751

W3C validator