dchrptlem2 - Metamath Proof Explorer

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

Theorem dchrptlem2 27216

Description: Lemma for dchrpt 27218. (Contributed by Mario Carneiro, 28-Apr-2016.)

**Hypotheses**
Ref	Expression
dchrpt.g	⊢ 𝐺 = (DChr‘𝑁)
dchrpt.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
dchrpt.d	⊢ 𝐷 = (Base‘𝐺)
dchrpt.b	⊢ 𝐵 = (Base‘𝑍)
dchrpt.1	⊢ 1 = (1_r‘𝑍)
dchrpt.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
dchrpt.n1	⊢ (𝜑 → 𝐴 ≠ 1 )
dchrpt.u	⊢ 𝑈 = (Unit‘𝑍)
dchrpt.h	⊢ 𝐻 = ((mulGrp‘𝑍) ↾_s 𝑈)
dchrpt.m	⊢ · = (._g‘𝐻)
dchrpt.s	⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))
dchrpt.au	⊢ (𝜑 → 𝐴 ∈ 𝑈)
dchrpt.w	⊢ (𝜑 → 𝑊 ∈ Word 𝑈)
dchrpt.2	⊢ (𝜑 → 𝐻dom DProd 𝑆)
dchrpt.3	⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)
dchrpt.p	⊢ 𝑃 = (𝐻dProj𝑆)
dchrpt.o	⊢ 𝑂 = (od‘𝐻)
dchrpt.t	⊢ 𝑇 = (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))
dchrpt.i	⊢ (𝜑 → 𝐼 ∈ dom 𝑊)
dchrpt.4	⊢ (𝜑 → ((𝑃‘𝐼)‘𝐴) ≠ 1 )
dchrpt.5	⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))

**Assertion**
Ref	Expression
dchrptlem2	⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)

Distinct variable groups: ℎ,𝑘,𝑚,𝑛,𝑥, 1 𝑢,ℎ,𝐴,𝑘,𝑚,𝑛,𝑥 ℎ,𝐼,𝑘,𝑚,𝑢 𝑥,𝐵 𝑥,𝐺 ℎ,𝐻,𝑘,𝑚,𝑛,𝑢,𝑥 𝑥,𝑁 ℎ,𝑊,𝑘,𝑚,𝑛,𝑢,𝑥 · ,ℎ,𝑘,𝑚,𝑛,𝑢,𝑥 𝑥,𝑋 𝑃,ℎ,𝑚,𝑢 𝑆,ℎ,𝑘,𝑚,𝑛,𝑢,𝑥 ℎ,𝑍,𝑘,𝑚,𝑛,𝑢,𝑥 𝑥,𝐷 𝜑,ℎ,𝑘,𝑚,𝑛,𝑥 𝑇,ℎ,𝑚,𝑢 𝑈,ℎ,𝑚,𝑢,𝑥 Allowed substitution hints: 𝜑(𝑢) 𝐵(𝑢,ℎ,𝑘,𝑚,𝑛) 𝐷(𝑢,ℎ,𝑘,𝑚,𝑛) 𝑃(𝑥,𝑘,𝑛) 𝑇(𝑥,𝑘,𝑛) 𝑈(𝑘,𝑛) 1 (𝑢) 𝐺(𝑢,ℎ,𝑘,𝑚,𝑛) 𝐼(𝑥,𝑛) 𝑁(𝑢,ℎ,𝑘,𝑚,𝑛) 𝑂(𝑥,𝑢,ℎ,𝑘,𝑚,𝑛) 𝑋(𝑢,ℎ,𝑘,𝑚,𝑛)

Proof of Theorem dchrptlem2 Dummy variables 𝑎 𝑏 𝑣 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dchrpt.g	. . 3 ⊢ 𝐺 = (DChr‘𝑁)
2		dchrpt.z	. . 3 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
3		dchrpt.b	. . 3 ⊢ 𝐵 = (Base‘𝑍)
4		dchrpt.u	. . 3 ⊢ 𝑈 = (Unit‘𝑍)
5		dchrpt.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6		dchrpt.d	. . 3 ⊢ 𝐷 = (Base‘𝐺)
7		fveq2 6829	. . 3 ⊢ (𝑣 = 𝑥 → (𝑋‘𝑣) = (𝑋‘𝑥))
8		fveq2 6829	. . 3 ⊢ (𝑣 = 𝑦 → (𝑋‘𝑣) = (𝑋‘𝑦))
9		fveq2 6829	. . 3 ⊢ (𝑣 = (𝑥(._r‘𝑍)𝑦) → (𝑋‘𝑣) = (𝑋‘(𝑥(._r‘𝑍)𝑦)))
10		fveq2 6829	. . 3 ⊢ (𝑣 = (1_r‘𝑍) → (𝑋‘𝑣) = (𝑋‘(1_r‘𝑍)))
11		dchrpt.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐻dom DProd 𝑆)
12		zex 12522	. . . . . . . . . . . . 13 ⊢ ℤ ∈ V
13	12	mptex 7167	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
14	13	rnex 7850	. . . . . . . . . . 11 ⊢ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
15		dchrpt.s	. . . . . . . . . . 11 ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))
16	14, 15	dmmpti 6631	. . . . . . . . . 10 ⊢ dom 𝑆 = dom 𝑊
17	16	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑆 = dom 𝑊)
18		dchrpt.p	. . . . . . . . 9 ⊢ 𝑃 = (𝐻dProj𝑆)
19		dchrpt.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ dom 𝑊)
20	11, 17, 18, 19	dpjf 20023	. . . . . . . 8 ⊢ (𝜑 → (𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼))
21		dchrpt.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)
22	21	feq2d 6641	. . . . . . . 8 ⊢ (𝜑 → ((𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼) ↔ (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼)))
23	20, 22	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼))
24	23	ffvelcdmda 7025	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ (𝑆‘𝐼))
25	19	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → 𝐼 ∈ dom 𝑊)
26		oveq1 7363	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑎 → (𝑛 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝑘)))
27	26	cbvmptv 5178	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘)))
28		fveq2 6829	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐼 → (𝑊‘𝑘) = (𝑊‘𝐼))
29	28	oveq2d 7372	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐼 → (𝑎 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝐼)))
30	29	mpteq2dv 5168	. . . . . . . . . 10 ⊢ (𝑘 = 𝐼 → (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
31	27, 30	eqtrid 2782	. . . . . . . . 9 ⊢ (𝑘 = 𝐼 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
32	31	rneqd 5882	. . . . . . . 8 ⊢ (𝑘 = 𝐼 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
33	32, 15, 14	fvmpt3i 6942	. . . . . . 7 ⊢ (𝐼 ∈ dom 𝑊 → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
34	25, 33	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
35	24, 34	eleqtrd 2837	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
36		eqid 2735	. . . . . 6 ⊢ (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))
37		ovex 7389	. . . . . 6 ⊢ (𝑎 · (𝑊‘𝐼)) ∈ V
38	36, 37	elrnmpti 5906	. . . . 5 ⊢ (((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
39	35, 38	sylib 218	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
40		dchrpt.1	. . . . . 6 ⊢ 1 = (1_r‘𝑍)
41		dchrpt.n1	. . . . . 6 ⊢ (𝜑 → 𝐴 ≠ 1 )
42		dchrpt.h	. . . . . 6 ⊢ 𝐻 = ((mulGrp‘𝑍) ↾_s 𝑈)
43		dchrpt.m	. . . . . 6 ⊢ · = (._g‘𝐻)
44		dchrpt.au	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
45		dchrpt.w	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ Word 𝑈)
46		dchrpt.o	. . . . . 6 ⊢ 𝑂 = (od‘𝐻)
47		dchrpt.t	. . . . . 6 ⊢ 𝑇 = (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))
48		dchrpt.4	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘𝐴) ≠ 1 )
49		dchrpt.5	. . . . . 6 ⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))
50	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 27215	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) = (𝑇↑𝑎))
51		neg1cn 12133	. . . . . . . . 9 ⊢ -1 ∈ ℂ
52		2re 12244	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
53	5	nnnn0d 12487	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
54	2	zncrng 21513	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing)
55		crngring 20215	. . . . . . . . . . . . . 14 ⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring)
56	53, 54, 55	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ Ring)
57	4, 42	unitgrp 20352	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp)
58	56, 57	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 ∈ Grp)
59	2, 3	znfi 21528	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
60	5, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ Fin)
61	3, 4	unitss 20345	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ 𝐵
62		ssfi 9096	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin)
63	60, 61, 62	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ Fin)
64		wrdf 14469	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ Word 𝑈 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
65	45, 64	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
66	65	fdmd 6667	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
67	19, 66	eleqtrd 2837	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝑊)))
68	65, 67	ffvelcdmd 7026	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑈)
69	4, 42	unitgrpbas 20351	. . . . . . . . . . . . 13 ⊢ 𝑈 = (Base‘𝐻)
70	69, 46	odcl2 19529	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊‘𝐼) ∈ 𝑈) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
71	58, 63, 68, 70	syl3anc 1374	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
72		nndivre 12207	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (𝑂‘(𝑊‘𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
73	52, 71, 72	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
74	73	recnd 11162	. . . . . . . . 9 ⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ)
75		cxpcl 26626	. . . . . . . . 9 ⊢ ((-1 ∈ ℂ ∧ (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
76	51, 74, 75	sylancr 588	. . . . . . . 8 ⊢ (𝜑 → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
77	47, 76	eqeltrid 2839	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℂ)
78	77	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ∈ ℂ)
79	51	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → -1 ∈ ℂ)
80		neg1ne0 12135	. . . . . . . . . 10 ⊢ -1 ≠ 0
81	80	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → -1 ≠ 0)
82	79, 81, 74	cxpne0d 26665	. . . . . . . 8 ⊢ (𝜑 → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
83	47	neeq1i 2994	. . . . . . . 8 ⊢ (𝑇 ≠ 0 ↔ (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
84	82, 83	sylibr 234	. . . . . . 7 ⊢ (𝜑 → 𝑇 ≠ 0)
85	84	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ≠ 0)
86		simprl 771	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ)
87	78, 85, 86	expclzd 14102	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑇↑𝑎) ∈ ℂ)
88	50, 87	eqeltrd 2835	. . . 4 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) ∈ ℂ)
89	39, 88	rexlimddv 3142	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑋‘𝑣) ∈ ℂ)
90		fveqeq2 6838	. . . . . 6 ⊢ (𝑣 = 𝑥 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))))
91	90	rexbidv 3159	. . . . 5 ⊢ (𝑣 = 𝑥 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))))
92	39	ralrimiva 3127	. . . . . 6 ⊢ (𝜑 → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
93	92	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
94		simprl 771	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
95	91, 93, 94	rspcdva 3563	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))
96		fveqeq2 6838	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼))))
97	96	rexbidv 3159	. . . . . 6 ⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼))))
98		oveq1 7363	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝑎 · (𝑊‘𝐼)) = (𝑏 · (𝑊‘𝐼)))
99	98	eqeq2d 2746	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
100	99	cbvrexvw 3214	. . . . . 6 ⊢ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
101	97, 100	bitrdi 287	. . . . 5 ⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
102		simprr 773	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
103	101, 93, 102	rspcdva 3563	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
104		reeanv 3207	. . . . 5 ⊢ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) ↔ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
105	77	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ∈ ℂ)
106	84	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ≠ 0)
107		simprll 779	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑎 ∈ ℤ)
108		simprlr 780	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑏 ∈ ℤ)
109		expaddz 14057	. . . . . . . . 9 ⊢ (((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
110	105, 106, 107, 108, 109	syl22anc 839	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
111		simpll 767	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝜑)
112	56	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑍 ∈ Ring)
113	94	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑥 ∈ 𝑈)
114	102	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑦 ∈ 𝑈)
115		eqid 2735	. . . . . . . . . . 11 ⊢ (._r‘𝑍) = (._r‘𝑍)
116	4, 115	unitmulcl 20349	. . . . . . . . . 10 ⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝑍)𝑦) ∈ 𝑈)
117	112, 113, 114, 116	syl3anc 1374	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑥(._r‘𝑍)𝑦) ∈ 𝑈)
118	107, 108	zaddcld 12626	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑎 + 𝑏) ∈ ℤ)
119		simprrl 781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))
120		simprrr 782	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
121	119, 120	oveq12d 7374	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
122	11, 17, 18, 19	dpjghm 20029	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃‘𝐼) ∈ ((𝐻 ↾_s (𝐻 DProd 𝑆)) GrpHom 𝐻))
123	21	oveq2d 7372	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻 ↾_s (𝐻 DProd 𝑆)) = (𝐻 ↾_s 𝑈))
124	42	ovexi 7390	. . . . . . . . . . . . . . . 16 ⊢ 𝐻 ∈ V
125	69	ressid 17203	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ V → (𝐻 ↾_s 𝑈) = 𝐻)
126	124, 125	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ↾_s 𝑈) = 𝐻
127	123, 126	eqtrdi 2786	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻 ↾_s (𝐻 DProd 𝑆)) = 𝐻)
128	127	oveq1d 7371	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐻 ↾_s (𝐻 DProd 𝑆)) GrpHom 𝐻) = (𝐻 GrpHom 𝐻))
129	122, 128	eleqtrd 2837	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻))
130	129	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻))
131	4	fvexi 6843	. . . . . . . . . . . . 13 ⊢ 𝑈 ∈ V
132		eqid 2735	. . . . . . . . . . . . . . 15 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
133	132, 115	mgpplusg 20114	. . . . . . . . . . . . . 14 ⊢ (._r‘𝑍) = (+_g‘(mulGrp‘𝑍))
134	42, 133	ressplusg 17243	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ V → (._r‘𝑍) = (+_g‘𝐻))
135	131, 134	ax-mp 5	. . . . . . . . . . . 12 ⊢ (._r‘𝑍) = (+_g‘𝐻)
136	69, 135, 135	ghmlin 19185	. . . . . . . . . . 11 ⊢ (((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)))
137	130, 113, 114, 136	syl3anc 1374	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)))
138	58	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝐻 ∈ Grp)
139	68	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑊‘𝐼) ∈ 𝑈)
140	69, 43, 135	mulgdir 19071	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ Grp ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ (𝑊‘𝐼) ∈ 𝑈)) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
141	138, 107, 108, 139, 140	syl13anc 1375	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
142	121, 137, 141	3eqtr4d 2780	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊‘𝐼)))
143	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 27215	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥(._r‘𝑍)𝑦) ∈ 𝑈) ∧ ((𝑎 + 𝑏) ∈ ℤ ∧ ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊‘𝐼)))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏)))
144	111, 117, 118, 142, 143	syl22anc 839	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏)))
145	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 27215	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑥) = (𝑇↑𝑎))
146	111, 113, 107, 119, 145	syl22anc 839	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑥) = (𝑇↑𝑎))
147	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 27215	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑈) ∧ (𝑏 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) → (𝑋‘𝑦) = (𝑇↑𝑏))
148	111, 114, 108, 120, 147	syl22anc 839	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑦) = (𝑇↑𝑏))
149	146, 148	oveq12d 7374	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑋‘𝑥) · (𝑋‘𝑦)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
150	110, 144, 149	3eqtr4d 2780	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
151	150	expr 456	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
152	151	rexlimdvva 3192	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
153	104, 152	biimtrrid 243	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
154	95, 103, 153	mp2and 700	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
155		id 22	. . . . 5 ⊢ (𝜑 → 𝜑)
156		eqid 2735	. . . . . . 7 ⊢ (1_r‘𝑍) = (1_r‘𝑍)
157	4, 156	1unit 20343	. . . . . 6 ⊢ (𝑍 ∈ Ring → (1_r‘𝑍) ∈ 𝑈)
158	56, 157	syl 17	. . . . 5 ⊢ (𝜑 → (1_r‘𝑍) ∈ 𝑈)
159		0zd 12525	. . . . 5 ⊢ (𝜑 → 0 ∈ ℤ)
160		eqid 2735	. . . . . . . 8 ⊢ (0_g‘𝐻) = (0_g‘𝐻)
161	160, 160	ghmid 19186	. . . . . . 7 ⊢ ((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) → ((𝑃‘𝐼)‘(0_g‘𝐻)) = (0_g‘𝐻))
162	129, 161	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘(0_g‘𝐻)) = (0_g‘𝐻))
163	4, 42, 156	unitgrpid 20354	. . . . . . . 8 ⊢ (𝑍 ∈ Ring → (1_r‘𝑍) = (0_g‘𝐻))
164	56, 163	syl 17	. . . . . . 7 ⊢ (𝜑 → (1_r‘𝑍) = (0_g‘𝐻))
165	164	fveq2d 6833	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘(1_r‘𝑍)) = ((𝑃‘𝐼)‘(0_g‘𝐻)))
166	69, 160, 43	mulg0 19039	. . . . . . 7 ⊢ ((𝑊‘𝐼) ∈ 𝑈 → (0 · (𝑊‘𝐼)) = (0_g‘𝐻))
167	68, 166	syl 17	. . . . . 6 ⊢ (𝜑 → (0 · (𝑊‘𝐼)) = (0_g‘𝐻))
168	162, 165, 167	3eqtr4d 2780	. . . . 5 ⊢ (𝜑 → ((𝑃‘𝐼)‘(1_r‘𝑍)) = (0 · (𝑊‘𝐼)))
169	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 27215	. . . . 5 ⊢ (((𝜑 ∧ (1_r‘𝑍) ∈ 𝑈) ∧ (0 ∈ ℤ ∧ ((𝑃‘𝐼)‘(1_r‘𝑍)) = (0 · (𝑊‘𝐼)))) → (𝑋‘(1_r‘𝑍)) = (𝑇↑0))
170	155, 158, 159, 168, 169	syl22anc 839	. . . 4 ⊢ (𝜑 → (𝑋‘(1_r‘𝑍)) = (𝑇↑0))
171	77	exp0d 14091	. . . 4 ⊢ (𝜑 → (𝑇↑0) = 1)
172	170, 171	eqtrd 2770	. . 3 ⊢ (𝜑 → (𝑋‘(1_r‘𝑍)) = 1)
173	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 89, 154, 172	dchrelbasd 27190	. 2 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷)
174	61, 44	sselid 3915	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
175		eleq1 2823	. . . . . . 7 ⊢ (𝑣 = 𝐴 → (𝑣 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈))
176		fveq2 6829	. . . . . . 7 ⊢ (𝑣 = 𝐴 → (𝑋‘𝑣) = (𝑋‘𝐴))
177	175, 176	ifbieq1d 4481	. . . . . 6 ⊢ (𝑣 = 𝐴 → if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
178		eqid 2735	. . . . . 6 ⊢ (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))
179		fvex 6842	. . . . . . 7 ⊢ (𝑋‘𝑣) ∈ V
180		c0ex 11127	. . . . . . 7 ⊢ 0 ∈ V
181	179, 180	ifex 4507	. . . . . 6 ⊢ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) ∈ V
182	177, 178, 181	fvmpt3i 6942	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
183	174, 182	syl 17	. . . 4 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
184	44	iftrued 4464	. . . 4 ⊢ (𝜑 → if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0) = (𝑋‘𝐴))
185	183, 184	eqtrd 2770	. . 3 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = (𝑋‘𝐴))
186		fveqeq2 6838	. . . . . 6 ⊢ (𝑣 = 𝐴 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))))
187	186	rexbidv 3159	. . . . 5 ⊢ (𝑣 = 𝐴 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))))
188	187, 92, 44	rspcdva 3563	. . . 4 ⊢ (𝜑 → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))
189	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 27215	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = (𝑇↑𝑎))
190	47	oveq1i 7366	. . . . . . . 8 ⊢ (𝑇↑𝑎) = ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎)
191	189, 190	eqtrdi 2786	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎))
192	48	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) ≠ 1 )
193	58	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝐻 ∈ Grp)
194	68	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑊‘𝐼) ∈ 𝑈)
195		simprl 771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ)
196	69, 46, 43, 160	oddvds 19511	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ Grp ∧ (𝑊‘𝐼) ∈ 𝑈 ∧ 𝑎 ∈ ℤ) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
197	193, 194, 195, 196	syl3anc 1374	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
198	71	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
199		root1eq1 26707	. . . . . . . . . . 11 ⊢ (((𝑂‘(𝑊‘𝐼)) ∈ ℕ ∧ 𝑎 ∈ ℤ) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎))
200	198, 195, 199	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎))
201		simprr 773	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))
202	40, 164	eqtrid 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 = (0_g‘𝐻))
203	202	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 1 = (0_g‘𝐻))
204	201, 203	eqeq12d 2751	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((𝑃‘𝐼)‘𝐴) = 1 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
205	197, 200, 204	3bitr4d 311	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ ((𝑃‘𝐼)‘𝐴) = 1 ))
206	205	necon3bid 2974	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1 ↔ ((𝑃‘𝐼)‘𝐴) ≠ 1 ))
207	192, 206	mpbird 257	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1)
208	191, 207	eqnetrd 2997	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) ≠ 1)
209	208	rexlimdvaa 3137	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑈) → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1))
210	44, 209	mpdan 688	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1))
211	188, 210	mpd 15	. . 3 ⊢ (𝜑 → (𝑋‘𝐴) ≠ 1)
212	185, 211	eqnetrd 2997	. 2 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1)
213		fveq1 6828	. . . 4 ⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → (𝑥‘𝐴) = ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴))
214	213	neeq1d 2989	. . 3 ⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → ((𝑥‘𝐴) ≠ 1 ↔ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1))
215	214	rspcev 3562	. 2 ⊢ (((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷 ∧ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
216	173, 212, 215	syl2anc 585	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2930 ∀wral 3049 ∃wrex 3059 Vcvv 3427 ⊆ wss 3885 ifcif 4456 class class class wbr 5074 ↦ cmpt 5155 dom cdm 5620 ran crn 5621 ℩cio 6441 ⟶wf 6483 ‘cfv 6487 (class class class)co 7356 Fincfn 8882 ℂcc 11025 ℝcr 11026 0cc0 11027 1c1 11028 + caddc 11030 · cmul 11032 -cneg 11367 / cdiv 11796 ℕcn 12163 2c2 12225 ℕ₀cn0 12426 ℤcz 12513 ..^cfzo 13597 ↑cexp 14012 ♯chash 14281 Word cword 14464 ∥ cdvds 16210 Basecbs 17168 ↾_s cress 17189 +_gcplusg 17209 ._rcmulr 17210 0_gc0g 17391 Grpcgrp 18898 ._gcmg 19032 GrpHom cghm 19176 odcod 19488 DProd cdprd 19959 dProjcdpj 19960 mulGrpcmgp 20110 1_rcur 20151 Ringcrg 20203 CRingccrg 20204 Unitcui 20324 ℤ/nℤczn 21471 ↑_𝑐ccxp 26507 DChrcdchr 27183

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 2184 ax-ext 2707 ax-rep 5201 ax-sep 5220 ax-nul 5230 ax-pow 5296 ax-pr 5364 ax-un 7678 ax-inf2 9551 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104 ax-pre-sup 11105 ax-addf 11106 ax-mulf 11107

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 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3060 df-rmo 3340 df-reu 3341 df-rab 3388 df-v 3429 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4264 df-if 4457 df-pw 4533 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4841 df-int 4880 df-iun 4925 df-iin 4926 df-br 5075 df-opab 5137 df-mpt 5156 df-tr 5182 df-id 5515 df-eprel 5520 df-po 5528 df-so 5529 df-fr 5573 df-se 5574 df-we 5575 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6254 df-ord 6315 df-on 6316 df-lim 6317 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-isom 6496 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8100 df-tpos 8165 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-2o 8395 df-oadd 8398 df-omul 8399 df-er 8632 df-ec 8634 df-qs 8638 df-map 8764 df-pm 8765 df-ixp 8835 df-en 8883 df-dom 8884 df-sdom 8885 df-fin 8886 df-fsupp 9264 df-fi 9313 df-sup 9344 df-inf 9345 df-oi 9414 df-card 9852 df-acn 9855 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12164 df-2 12233 df-3 12234 df-4 12235 df-5 12236 df-6 12237 df-7 12238 df-8 12239 df-9 12240 df-n0 12427 df-z 12514 df-dec 12634 df-uz 12778 df-q 12888 df-rp 12932 df-xneg 13052 df-xadd 13053 df-xmul 13054 df-ioo 13291 df-ioc 13292 df-ico 13293 df-icc 13294 df-fz 13451 df-fzo 13598 df-fl 13740 df-mod 13818 df-seq 13953 df-exp 14013 df-fac 14225 df-bc 14254 df-hash 14282 df-word 14465 df-shft 15018 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-limsup 15422 df-clim 15439 df-rlim 15440 df-sum 15638 df-ef 16021 df-sin 16023 df-cos 16024 df-pi 16026 df-dvds 16211 df-struct 17106 df-sets 17123 df-slot 17141 df-ndx 17153 df-base 17169 df-ress 17190 df-plusg 17222 df-mulr 17223 df-starv 17224 df-sca 17225 df-vsca 17226 df-ip 17227 df-tset 17228 df-ple 17229 df-ds 17231 df-unif 17232 df-hom 17233 df-cco 17234 df-rest 17374 df-topn 17375 df-0g 17393 df-gsum 17394 df-topgen 17395 df-pt 17396 df-prds 17399 df-xrs 17455 df-qtop 17460 df-imas 17461 df-qus 17462 df-xps 17463 df-mre 17537 df-mrc 17538 df-acs 17540 df-mgm 18597 df-sgrp 18676 df-mnd 18692 df-mhm 18740 df-submnd 18741 df-grp 18901 df-minusg 18902 df-sbg 18903 df-mulg 19033 df-subg 19088 df-nsg 19089 df-eqg 19090 df-ghm 19177 df-gim 19223 df-cntz 19281 df-oppg 19310 df-od 19492 df-lsm 19600 df-pj1 19601 df-cmn 19746 df-abl 19747 df-dprd 19961 df-dpj 19962 df-mgp 20111 df-rng 20123 df-ur 20152 df-ring 20205 df-cring 20206 df-oppr 20306 df-dvdsr 20326 df-unit 20327 df-rhm 20441 df-subrng 20512 df-subrg 20536 df-lmod 20846 df-lss 20916 df-lsp 20956 df-sra 21157 df-rgmod 21158 df-lidl 21195 df-rsp 21196 df-2idl 21237 df-psmet 21333 df-xmet 21334 df-met 21335 df-bl 21336 df-mopn 21337 df-fbas 21338 df-fg 21339 df-cnfld 21342 df-zring 21416 df-zrh 21472 df-zn 21475 df-top 22847 df-topon 22864 df-topsp 22886 df-bases 22899 df-cld 22972 df-ntr 22973 df-cls 22974 df-nei 23051 df-lp 23089 df-perf 23090 df-cn 23180 df-cnp 23181 df-haus 23268 df-tx 23515 df-hmeo 23708 df-fil 23799 df-fm 23891 df-flim 23892 df-flf 23893 df-xms 24273 df-ms 24274 df-tms 24275 df-cncf 24833 df-limc 25821 df-dv 25822 df-log 26508 df-cxp 26509 df-dchr 27184

This theorem is referenced by: dchrptlem3 27217

W3C validator