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 27236

Description: Lemma for dchrpt 27238. (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 6835	. . 3 ⊢ (𝑣 = 𝑥 → (𝑋‘𝑣) = (𝑋‘𝑥))
8		fveq2 6835	. . 3 ⊢ (𝑣 = 𝑦 → (𝑋‘𝑣) = (𝑋‘𝑦))
9		fveq2 6835	. . 3 ⊢ (𝑣 = (𝑥(._r‘𝑍)𝑦) → (𝑋‘𝑣) = (𝑋‘(𝑥(._r‘𝑍)𝑦)))
10		fveq2 6835	. . 3 ⊢ (𝑣 = (1_r‘𝑍) → (𝑋‘𝑣) = (𝑋‘(1_r‘𝑍)))
11		dchrpt.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐻dom DProd 𝑆)
12		zex 12501	. . . . . . . . . . . . 13 ⊢ ℤ ∈ V
13	12	mptex 7171	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
14	13	rnex 7854	. . . . . . . . . . 11 ⊢ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
15		dchrpt.s	. . . . . . . . . . 11 ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))
16	14, 15	dmmpti 6637	. . . . . . . . . 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 19992	. . . . . . . 8 ⊢ (𝜑 → (𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼))
21		dchrpt.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)
22	21	feq2d 6647	. . . . . . . 8 ⊢ (𝜑 → ((𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼) ↔ (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼)))
23	20, 22	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼))
24	23	ffvelcdmda 7031	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ (𝑆‘𝐼))
25	19	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → 𝐼 ∈ dom 𝑊)
26		oveq1 7367	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑎 → (𝑛 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝑘)))
27	26	cbvmptv 5203	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘)))
28		fveq2 6835	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐼 → (𝑊‘𝑘) = (𝑊‘𝐼))
29	28	oveq2d 7376	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐼 → (𝑎 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝐼)))
30	29	mpteq2dv 5193	. . . . . . . . . 10 ⊢ (𝑘 = 𝐼 → (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
31	27, 30	eqtrid 2784	. . . . . . . . 9 ⊢ (𝑘 = 𝐼 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
32	31	rneqd 5888	. . . . . . . 8 ⊢ (𝑘 = 𝐼 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
33	32, 15, 14	fvmpt3i 6948	. . . . . . 7 ⊢ (𝐼 ∈ dom 𝑊 → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
34	25, 33	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
35	24, 34	eleqtrd 2839	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
36		eqid 2737	. . . . . 6 ⊢ (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))
37		ovex 7393	. . . . . 6 ⊢ (𝑎 · (𝑊‘𝐼)) ∈ V
38	36, 37	elrnmpti 5912	. . . . 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 27235	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) = (𝑇↑𝑎))
51		neg1cn 12134	. . . . . . . . 9 ⊢ -1 ∈ ℂ
52		2re 12223	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
53	5	nnnn0d 12466	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
54	2	zncrng 21503	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing)
55		crngring 20184	. . . . . . . . . . . . . 14 ⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring)
56	53, 54, 55	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ Ring)
57	4, 42	unitgrp 20323	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp)
58	56, 57	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 ∈ Grp)
59	2, 3	znfi 21518	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
60	5, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ Fin)
61	3, 4	unitss 20316	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ 𝐵
62		ssfi 9101	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin)
63	60, 61, 62	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ Fin)
64		wrdf 14445	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ Word 𝑈 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
65	45, 64	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
66	65	fdmd 6673	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
67	19, 66	eleqtrd 2839	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝑊)))
68	65, 67	ffvelcdmd 7032	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑈)
69	4, 42	unitgrpbas 20322	. . . . . . . . . . . . 13 ⊢ 𝑈 = (Base‘𝐻)
70	69, 46	odcl2 19498	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊‘𝐼) ∈ 𝑈) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
71	58, 63, 68, 70	syl3anc 1374	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
72		nndivre 12190	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (𝑂‘(𝑊‘𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
73	52, 71, 72	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
74	73	recnd 11164	. . . . . . . . 9 ⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ)
75		cxpcl 26643	. . . . . . . . 9 ⊢ ((-1 ∈ ℂ ∧ (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
76	51, 74, 75	sylancr 588	. . . . . . . 8 ⊢ (𝜑 → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
77	47, 76	eqeltrid 2841	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℂ)
78	77	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ∈ ℂ)
79	51	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → -1 ∈ ℂ)
80		neg1ne0 12136	. . . . . . . . . 10 ⊢ -1 ≠ 0
81	80	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → -1 ≠ 0)
82	79, 81, 74	cxpne0d 26682	. . . . . . . 8 ⊢ (𝜑 → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
83	47	neeq1i 2997	. . . . . . . 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 14078	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑇↑𝑎) ∈ ℂ)
88	50, 87	eqeltrd 2837	. . . 4 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) ∈ ℂ)
89	39, 88	rexlimddv 3144	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑋‘𝑣) ∈ ℂ)
90		fveqeq2 6844	. . . . . 6 ⊢ (𝑣 = 𝑥 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))))
91	90	rexbidv 3161	. . . . 5 ⊢ (𝑣 = 𝑥 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))))
92	39	ralrimiva 3129	. . . . . 6 ⊢ (𝜑 → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
93	92	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
94		simprl 771	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
95	91, 93, 94	rspcdva 3578	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))
96		fveqeq2 6844	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼))))
97	96	rexbidv 3161	. . . . . 6 ⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼))))
98		oveq1 7367	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝑎 · (𝑊‘𝐼)) = (𝑏 · (𝑊‘𝐼)))
99	98	eqeq2d 2748	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
100	99	cbvrexvw 3216	. . . . . 6 ⊢ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
101	97, 100	bitrdi 287	. . . . 5 ⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
102		simprr 773	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
103	101, 93, 102	rspcdva 3578	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
104		reeanv 3209	. . . . 5 ⊢ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) ↔ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
105	77	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ∈ ℂ)
106	84	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ≠ 0)
107		simprll 779	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑎 ∈ ℤ)
108		simprlr 780	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑏 ∈ ℤ)
109		expaddz 14033	. . . . . . . . 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 2737	. . . . . . . . . . 11 ⊢ (._r‘𝑍) = (._r‘𝑍)
116	4, 115	unitmulcl 20320	. . . . . . . . . 10 ⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝑍)𝑦) ∈ 𝑈)
117	112, 113, 114, 116	syl3anc 1374	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑥(._r‘𝑍)𝑦) ∈ 𝑈)
118	107, 108	zaddcld 12604	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑎 + 𝑏) ∈ ℤ)
119		simprrl 781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))
120		simprrr 782	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
121	119, 120	oveq12d 7378	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
122	11, 17, 18, 19	dpjghm 19998	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃‘𝐼) ∈ ((𝐻 ↾_s (𝐻 DProd 𝑆)) GrpHom 𝐻))
123	21	oveq2d 7376	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻 ↾_s (𝐻 DProd 𝑆)) = (𝐻 ↾_s 𝑈))
124	42	ovexi 7394	. . . . . . . . . . . . . . . 16 ⊢ 𝐻 ∈ V
125	69	ressid 17175	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ V → (𝐻 ↾_s 𝑈) = 𝐻)
126	124, 125	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ↾_s 𝑈) = 𝐻
127	123, 126	eqtrdi 2788	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻 ↾_s (𝐻 DProd 𝑆)) = 𝐻)
128	127	oveq1d 7375	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐻 ↾_s (𝐻 DProd 𝑆)) GrpHom 𝐻) = (𝐻 GrpHom 𝐻))
129	122, 128	eleqtrd 2839	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻))
130	129	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻))
131	4	fvexi 6849	. . . . . . . . . . . . 13 ⊢ 𝑈 ∈ V
132		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
133	132, 115	mgpplusg 20083	. . . . . . . . . . . . . 14 ⊢ (._r‘𝑍) = (+_g‘(mulGrp‘𝑍))
134	42, 133	ressplusg 17215	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ V → (._r‘𝑍) = (+_g‘𝐻))
135	131, 134	ax-mp 5	. . . . . . . . . . . 12 ⊢ (._r‘𝑍) = (+_g‘𝐻)
136	69, 135, 135	ghmlin 19154	. . . . . . . . . . 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 19040	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ Grp ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ (𝑊‘𝐼) ∈ 𝑈)) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
141	138, 107, 108, 139, 140	syl13anc 1375	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
142	121, 137, 141	3eqtr4d 2782	. . . . . . . . 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 27235	. . . . . . . . 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 27235	. . . . . . . . . 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 27235	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑈) ∧ (𝑏 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) → (𝑋‘𝑦) = (𝑇↑𝑏))
148	111, 114, 108, 120, 147	syl22anc 839	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑦) = (𝑇↑𝑏))
149	146, 148	oveq12d 7378	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑋‘𝑥) · (𝑋‘𝑦)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
150	110, 144, 149	3eqtr4d 2782	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
151	150	expr 456	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
152	151	rexlimdvva 3194	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
153	104, 152	biimtrrid 243	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
154	95, 103, 153	mp2and 700	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
155		id 22	. . . . 5 ⊢ (𝜑 → 𝜑)
156		eqid 2737	. . . . . . 7 ⊢ (1_r‘𝑍) = (1_r‘𝑍)
157	4, 156	1unit 20314	. . . . . 6 ⊢ (𝑍 ∈ Ring → (1_r‘𝑍) ∈ 𝑈)
158	56, 157	syl 17	. . . . 5 ⊢ (𝜑 → (1_r‘𝑍) ∈ 𝑈)
159		0zd 12504	. . . . 5 ⊢ (𝜑 → 0 ∈ ℤ)
160		eqid 2737	. . . . . . . 8 ⊢ (0_g‘𝐻) = (0_g‘𝐻)
161	160, 160	ghmid 19155	. . . . . . 7 ⊢ ((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) → ((𝑃‘𝐼)‘(0_g‘𝐻)) = (0_g‘𝐻))
162	129, 161	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘(0_g‘𝐻)) = (0_g‘𝐻))
163	4, 42, 156	unitgrpid 20325	. . . . . . . 8 ⊢ (𝑍 ∈ Ring → (1_r‘𝑍) = (0_g‘𝐻))
164	56, 163	syl 17	. . . . . . 7 ⊢ (𝜑 → (1_r‘𝑍) = (0_g‘𝐻))
165	164	fveq2d 6839	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘(1_r‘𝑍)) = ((𝑃‘𝐼)‘(0_g‘𝐻)))
166	69, 160, 43	mulg0 19008	. . . . . . 7 ⊢ ((𝑊‘𝐼) ∈ 𝑈 → (0 · (𝑊‘𝐼)) = (0_g‘𝐻))
167	68, 166	syl 17	. . . . . 6 ⊢ (𝜑 → (0 · (𝑊‘𝐼)) = (0_g‘𝐻))
168	162, 165, 167	3eqtr4d 2782	. . . . 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 27235	. . . . 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 14067	. . . 4 ⊢ (𝜑 → (𝑇↑0) = 1)
172	170, 171	eqtrd 2772	. . 3 ⊢ (𝜑 → (𝑋‘(1_r‘𝑍)) = 1)
173	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 89, 154, 172	dchrelbasd 27210	. 2 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷)
174	61, 44	sselid 3932	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
175		eleq1 2825	. . . . . . 7 ⊢ (𝑣 = 𝐴 → (𝑣 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈))
176		fveq2 6835	. . . . . . 7 ⊢ (𝑣 = 𝐴 → (𝑋‘𝑣) = (𝑋‘𝐴))
177	175, 176	ifbieq1d 4505	. . . . . 6 ⊢ (𝑣 = 𝐴 → if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
178		eqid 2737	. . . . . 6 ⊢ (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))
179		fvex 6848	. . . . . . 7 ⊢ (𝑋‘𝑣) ∈ V
180		c0ex 11130	. . . . . . 7 ⊢ 0 ∈ V
181	179, 180	ifex 4531	. . . . . 6 ⊢ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) ∈ V
182	177, 178, 181	fvmpt3i 6948	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
183	174, 182	syl 17	. . . 4 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
184	44	iftrued 4488	. . . 4 ⊢ (𝜑 → if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0) = (𝑋‘𝐴))
185	183, 184	eqtrd 2772	. . 3 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = (𝑋‘𝐴))
186		fveqeq2 6844	. . . . . 6 ⊢ (𝑣 = 𝐴 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))))
187	186	rexbidv 3161	. . . . 5 ⊢ (𝑣 = 𝐴 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))))
188	187, 92, 44	rspcdva 3578	. . . 4 ⊢ (𝜑 → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))
189	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 27235	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = (𝑇↑𝑎))
190	47	oveq1i 7370	. . . . . . . 8 ⊢ (𝑇↑𝑎) = ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎)
191	189, 190	eqtrdi 2788	. . . . . . 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 19480	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ Grp ∧ (𝑊‘𝐼) ∈ 𝑈 ∧ 𝑎 ∈ ℤ) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
197	193, 194, 195, 196	syl3anc 1374	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
198	71	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
199		root1eq1 26725	. . . . . . . . . . 11 ⊢ (((𝑂‘(𝑊‘𝐼)) ∈ ℕ ∧ 𝑎 ∈ ℤ) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎))
200	198, 195, 199	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎))
201		simprr 773	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))
202	40, 164	eqtrid 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 = (0_g‘𝐻))
203	202	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 1 = (0_g‘𝐻))
204	201, 203	eqeq12d 2753	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((𝑃‘𝐼)‘𝐴) = 1 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
205	197, 200, 204	3bitr4d 311	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ ((𝑃‘𝐼)‘𝐴) = 1 ))
206	205	necon3bid 2977	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1 ↔ ((𝑃‘𝐼)‘𝐴) ≠ 1 ))
207	192, 206	mpbird 257	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1)
208	191, 207	eqnetrd 3000	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) ≠ 1)
209	208	rexlimdvaa 3139	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑈) → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1))
210	44, 209	mpdan 688	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1))
211	188, 210	mpd 15	. . 3 ⊢ (𝜑 → (𝑋‘𝐴) ≠ 1)
212	185, 211	eqnetrd 3000	. 2 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1)
213		fveq1 6834	. . . 4 ⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → (𝑥‘𝐴) = ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴))
214	213	neeq1d 2992	. . 3 ⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → ((𝑥‘𝐴) ≠ 1 ↔ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1))
215	214	rspcev 3577	. 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 2933 ∀wral 3052 ∃wrex 3061 Vcvv 3441 ⊆ wss 3902 ifcif 4480 class class class wbr 5099 ↦ cmpt 5180 dom cdm 5625 ran crn 5626 ℩cio 6447 ⟶wf 6489 ‘cfv 6493 (class class class)co 7360 Fincfn 8887 ℂcc 11028 ℝcr 11029 0cc0 11030 1c1 11031 + caddc 11033 · cmul 11035 -cneg 11369 / cdiv 11798 ℕcn 12149 2c2 12204 ℕ₀cn0 12405 ℤcz 12492 ..^cfzo 13574 ↑cexp 13988 ♯chash 14257 Word cword 14440 ∥ cdvds 16183 Basecbs 17140 ↾_s cress 17161 +_gcplusg 17181 ._rcmulr 17182 0_gc0g 17363 Grpcgrp 18867 ._gcmg 19001 GrpHom cghm 19145 odcod 19457 DProd cdprd 19928 dProjcdpj 19929 mulGrpcmgp 20079 1_rcur 20120 Ringcrg 20172 CRingccrg 20173 Unitcui 20295 ℤ/nℤczn 21461 ↑_𝑐ccxp 26524 DChrcdchr 27203

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 2185 ax-ext 2709 ax-rep 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682 ax-inf2 9554 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-pre-sup 11108 ax-addf 11109 ax-mulf 11110

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 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3351 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4904 df-iun 4949 df-iin 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-of 7624 df-om 7811 df-1st 7935 df-2nd 7936 df-supp 8105 df-tpos 8170 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-oadd 8403 df-omul 8404 df-er 8637 df-ec 8639 df-qs 8643 df-map 8769 df-pm 8770 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-fi 9318 df-sup 9349 df-inf 9350 df-oi 9419 df-card 9855 df-acn 9858 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12150 df-2 12212 df-3 12213 df-4 12214 df-5 12215 df-6 12216 df-7 12217 df-8 12218 df-9 12219 df-n0 12406 df-z 12493 df-dec 12612 df-uz 12756 df-q 12866 df-rp 12910 df-xneg 13030 df-xadd 13031 df-xmul 13032 df-ioo 13269 df-ioc 13270 df-ico 13271 df-icc 13272 df-fz 13428 df-fzo 13575 df-fl 13716 df-mod 13794 df-seq 13929 df-exp 13989 df-fac 14201 df-bc 14230 df-hash 14258 df-word 14441 df-shft 14994 df-cj 15026 df-re 15027 df-im 15028 df-sqrt 15162 df-abs 15163 df-limsup 15398 df-clim 15415 df-rlim 15416 df-sum 15614 df-ef 15994 df-sin 15996 df-cos 15997 df-pi 15999 df-dvds 16184 df-struct 17078 df-sets 17095 df-slot 17113 df-ndx 17125 df-base 17141 df-ress 17162 df-plusg 17194 df-mulr 17195 df-starv 17196 df-sca 17197 df-vsca 17198 df-ip 17199 df-tset 17200 df-ple 17201 df-ds 17203 df-unif 17204 df-hom 17205 df-cco 17206 df-rest 17346 df-topn 17347 df-0g 17365 df-gsum 17366 df-topgen 17367 df-pt 17368 df-prds 17371 df-xrs 17427 df-qtop 17432 df-imas 17433 df-qus 17434 df-xps 17435 df-mre 17509 df-mrc 17510 df-acs 17512 df-mgm 18569 df-sgrp 18648 df-mnd 18664 df-mhm 18712 df-submnd 18713 df-grp 18870 df-minusg 18871 df-sbg 18872 df-mulg 19002 df-subg 19057 df-nsg 19058 df-eqg 19059 df-ghm 19146 df-gim 19192 df-cntz 19250 df-oppg 19279 df-od 19461 df-lsm 19569 df-pj1 19570 df-cmn 19715 df-abl 19716 df-dprd 19930 df-dpj 19931 df-mgp 20080 df-rng 20092 df-ur 20121 df-ring 20174 df-cring 20175 df-oppr 20277 df-dvdsr 20297 df-unit 20298 df-rhm 20412 df-subrng 20483 df-subrg 20507 df-lmod 20817 df-lss 20887 df-lsp 20927 df-sra 21129 df-rgmod 21130 df-lidl 21167 df-rsp 21168 df-2idl 21209 df-psmet 21305 df-xmet 21306 df-met 21307 df-bl 21308 df-mopn 21309 df-fbas 21310 df-fg 21311 df-cnfld 21314 df-zring 21406 df-zrh 21462 df-zn 21465 df-top 22842 df-topon 22859 df-topsp 22881 df-bases 22894 df-cld 22967 df-ntr 22968 df-cls 22969 df-nei 23046 df-lp 23084 df-perf 23085 df-cn 23175 df-cnp 23176 df-haus 23263 df-tx 23510 df-hmeo 23703 df-fil 23794 df-fm 23886 df-flim 23887 df-flf 23888 df-xms 24268 df-ms 24269 df-tms 24270 df-cncf 24831 df-limc 25827 df-dv 25828 df-log 26525 df-cxp 26526 df-dchr 27204

This theorem is referenced by: dchrptlem3 27237

W3C validator