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 27324

Description: Lemma for dchrpt 27326. (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 6907	. . 3 ⊢ (𝑣 = 𝑥 → (𝑋‘𝑣) = (𝑋‘𝑥))
8		fveq2 6907	. . 3 ⊢ (𝑣 = 𝑦 → (𝑋‘𝑣) = (𝑋‘𝑦))
9		fveq2 6907	. . 3 ⊢ (𝑣 = (𝑥(._r‘𝑍)𝑦) → (𝑋‘𝑣) = (𝑋‘(𝑥(._r‘𝑍)𝑦)))
10		fveq2 6907	. . 3 ⊢ (𝑣 = (1_r‘𝑍) → (𝑋‘𝑣) = (𝑋‘(1_r‘𝑍)))
11		dchrpt.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐻dom DProd 𝑆)
12		zex 12620	. . . . . . . . . . . . 13 ⊢ ℤ ∈ V
13	12	mptex 7243	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
14	13	rnex 7933	. . . . . . . . . . 11 ⊢ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
15		dchrpt.s	. . . . . . . . . . 11 ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))
16	14, 15	dmmpti 6713	. . . . . . . . . 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 20092	. . . . . . . 8 ⊢ (𝜑 → (𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼))
21		dchrpt.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)
22	21	feq2d 6723	. . . . . . . 8 ⊢ (𝜑 → ((𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼) ↔ (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼)))
23	20, 22	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼))
24	23	ffvelcdmda 7104	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ (𝑆‘𝐼))
25	19	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → 𝐼 ∈ dom 𝑊)
26		oveq1 7438	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑎 → (𝑛 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝑘)))
27	26	cbvmptv 5261	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘)))
28		fveq2 6907	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐼 → (𝑊‘𝑘) = (𝑊‘𝐼))
29	28	oveq2d 7447	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐼 → (𝑎 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝐼)))
30	29	mpteq2dv 5250	. . . . . . . . . 10 ⊢ (𝑘 = 𝐼 → (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
31	27, 30	eqtrid 2787	. . . . . . . . 9 ⊢ (𝑘 = 𝐼 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
32	31	rneqd 5952	. . . . . . . 8 ⊢ (𝑘 = 𝐼 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
33	32, 15, 14	fvmpt3i 7021	. . . . . . 7 ⊢ (𝐼 ∈ dom 𝑊 → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
34	25, 33	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
35	24, 34	eleqtrd 2841	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
36		eqid 2735	. . . . . 6 ⊢ (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))
37		ovex 7464	. . . . . 6 ⊢ (𝑎 · (𝑊‘𝐼)) ∈ V
38	36, 37	elrnmpti 5976	. . . . 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 27323	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) = (𝑇↑𝑎))
51		neg1cn 12378	. . . . . . . . 9 ⊢ -1 ∈ ℂ
52		2re 12338	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
53	5	nnnn0d 12585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
54	2	zncrng 21581	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing)
55		crngring 20263	. . . . . . . . . . . . . 14 ⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring)
56	53, 54, 55	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ Ring)
57	4, 42	unitgrp 20400	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp)
58	56, 57	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 ∈ Grp)
59	2, 3	znfi 21596	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
60	5, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ Fin)
61	3, 4	unitss 20393	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ 𝐵
62		ssfi 9212	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin)
63	60, 61, 62	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ Fin)
64		wrdf 14554	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ Word 𝑈 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
65	45, 64	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
66	65	fdmd 6747	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
67	19, 66	eleqtrd 2841	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝑊)))
68	65, 67	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑈)
69	4, 42	unitgrpbas 20399	. . . . . . . . . . . . 13 ⊢ 𝑈 = (Base‘𝐻)
70	69, 46	odcl2 19598	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊‘𝐼) ∈ 𝑈) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
71	58, 63, 68, 70	syl3anc 1370	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
72		nndivre 12305	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (𝑂‘(𝑊‘𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
73	52, 71, 72	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
74	73	recnd 11287	. . . . . . . . 9 ⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ)
75		cxpcl 26731	. . . . . . . . 9 ⊢ ((-1 ∈ ℂ ∧ (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
76	51, 74, 75	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
77	47, 76	eqeltrid 2843	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℂ)
78	77	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ∈ ℂ)
79	51	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → -1 ∈ ℂ)
80		neg1ne0 12380	. . . . . . . . . 10 ⊢ -1 ≠ 0
81	80	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → -1 ≠ 0)
82	79, 81, 74	cxpne0d 26770	. . . . . . . 8 ⊢ (𝜑 → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
83	47	neeq1i 3003	. . . . . . . 8 ⊢ (𝑇 ≠ 0 ↔ (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
84	82, 83	sylibr 234	. . . . . . 7 ⊢ (𝜑 → 𝑇 ≠ 0)
85	84	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ≠ 0)
86		simprl 771	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ)
87	78, 85, 86	expclzd 14188	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑇↑𝑎) ∈ ℂ)
88	50, 87	eqeltrd 2839	. . . 4 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) ∈ ℂ)
89	39, 88	rexlimddv 3159	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑋‘𝑣) ∈ ℂ)
90		fveqeq2 6916	. . . . . 6 ⊢ (𝑣 = 𝑥 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))))
91	90	rexbidv 3177	. . . . 5 ⊢ (𝑣 = 𝑥 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))))
92	39	ralrimiva 3144	. . . . . 6 ⊢ (𝜑 → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
93	92	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
94		simprl 771	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
95	91, 93, 94	rspcdva 3623	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))
96		fveqeq2 6916	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼))))
97	96	rexbidv 3177	. . . . . 6 ⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼))))
98		oveq1 7438	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝑎 · (𝑊‘𝐼)) = (𝑏 · (𝑊‘𝐼)))
99	98	eqeq2d 2746	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
100	99	cbvrexvw 3236	. . . . . 6 ⊢ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
101	97, 100	bitrdi 287	. . . . 5 ⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
102		simprr 773	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
103	101, 93, 102	rspcdva 3623	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
104		reeanv 3227	. . . . 5 ⊢ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) ↔ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
105	77	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ∈ ℂ)
106	84	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ≠ 0)
107		simprll 779	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑎 ∈ ℤ)
108		simprlr 780	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑏 ∈ ℤ)
109		expaddz 14144	. . . . . . . . 9 ⊢ (((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
110	105, 106, 107, 108, 109	syl22anc 839	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
111		simpll 767	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝜑)
112	56	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑍 ∈ Ring)
113	94	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑥 ∈ 𝑈)
114	102	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑦 ∈ 𝑈)
115		eqid 2735	. . . . . . . . . . 11 ⊢ (._r‘𝑍) = (._r‘𝑍)
116	4, 115	unitmulcl 20397	. . . . . . . . . 10 ⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝑍)𝑦) ∈ 𝑈)
117	112, 113, 114, 116	syl3anc 1370	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑥(._r‘𝑍)𝑦) ∈ 𝑈)
118	107, 108	zaddcld 12724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑎 + 𝑏) ∈ ℤ)
119		simprrl 781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))
120		simprrr 782	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
121	119, 120	oveq12d 7449	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
122	11, 17, 18, 19	dpjghm 20098	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃‘𝐼) ∈ ((𝐻 ↾_s (𝐻 DProd 𝑆)) GrpHom 𝐻))
123	21	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻 ↾_s (𝐻 DProd 𝑆)) = (𝐻 ↾_s 𝑈))
124	42	ovexi 7465	. . . . . . . . . . . . . . . 16 ⊢ 𝐻 ∈ V
125	69	ressid 17290	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ V → (𝐻 ↾_s 𝑈) = 𝐻)
126	124, 125	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ↾_s 𝑈) = 𝐻
127	123, 126	eqtrdi 2791	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻 ↾_s (𝐻 DProd 𝑆)) = 𝐻)
128	127	oveq1d 7446	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐻 ↾_s (𝐻 DProd 𝑆)) GrpHom 𝐻) = (𝐻 GrpHom 𝐻))
129	122, 128	eleqtrd 2841	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻))
130	129	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻))
131	4	fvexi 6921	. . . . . . . . . . . . 13 ⊢ 𝑈 ∈ V
132		eqid 2735	. . . . . . . . . . . . . . 15 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
133	132, 115	mgpplusg 20156	. . . . . . . . . . . . . 14 ⊢ (._r‘𝑍) = (+_g‘(mulGrp‘𝑍))
134	42, 133	ressplusg 17336	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ V → (._r‘𝑍) = (+_g‘𝐻))
135	131, 134	ax-mp 5	. . . . . . . . . . . 12 ⊢ (._r‘𝑍) = (+_g‘𝐻)
136	69, 135, 135	ghmlin 19252	. . . . . . . . . . 11 ⊢ (((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)))
137	130, 113, 114, 136	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)))
138	58	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝐻 ∈ Grp)
139	68	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑊‘𝐼) ∈ 𝑈)
140	69, 43, 135	mulgdir 19137	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ Grp ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ (𝑊‘𝐼) ∈ 𝑈)) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
141	138, 107, 108, 139, 140	syl13anc 1371	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
142	121, 137, 141	3eqtr4d 2785	. . . . . . . . 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 27323	. . . . . . . . 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 27323	. . . . . . . . . 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 27323	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑈) ∧ (𝑏 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) → (𝑋‘𝑦) = (𝑇↑𝑏))
148	111, 114, 108, 120, 147	syl22anc 839	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑦) = (𝑇↑𝑏))
149	146, 148	oveq12d 7449	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑋‘𝑥) · (𝑋‘𝑦)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
150	110, 144, 149	3eqtr4d 2785	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
151	150	expr 456	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
152	151	rexlimdvva 3211	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
153	104, 152	biimtrrid 243	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
154	95, 103, 153	mp2and 699	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
155		id 22	. . . . 5 ⊢ (𝜑 → 𝜑)
156		eqid 2735	. . . . . . 7 ⊢ (1_r‘𝑍) = (1_r‘𝑍)
157	4, 156	1unit 20391	. . . . . 6 ⊢ (𝑍 ∈ Ring → (1_r‘𝑍) ∈ 𝑈)
158	56, 157	syl 17	. . . . 5 ⊢ (𝜑 → (1_r‘𝑍) ∈ 𝑈)
159		0zd 12623	. . . . 5 ⊢ (𝜑 → 0 ∈ ℤ)
160		eqid 2735	. . . . . . . 8 ⊢ (0_g‘𝐻) = (0_g‘𝐻)
161	160, 160	ghmid 19253	. . . . . . 7 ⊢ ((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) → ((𝑃‘𝐼)‘(0_g‘𝐻)) = (0_g‘𝐻))
162	129, 161	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘(0_g‘𝐻)) = (0_g‘𝐻))
163	4, 42, 156	unitgrpid 20402	. . . . . . . 8 ⊢ (𝑍 ∈ Ring → (1_r‘𝑍) = (0_g‘𝐻))
164	56, 163	syl 17	. . . . . . 7 ⊢ (𝜑 → (1_r‘𝑍) = (0_g‘𝐻))
165	164	fveq2d 6911	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘(1_r‘𝑍)) = ((𝑃‘𝐼)‘(0_g‘𝐻)))
166	69, 160, 43	mulg0 19105	. . . . . . 7 ⊢ ((𝑊‘𝐼) ∈ 𝑈 → (0 · (𝑊‘𝐼)) = (0_g‘𝐻))
167	68, 166	syl 17	. . . . . 6 ⊢ (𝜑 → (0 · (𝑊‘𝐼)) = (0_g‘𝐻))
168	162, 165, 167	3eqtr4d 2785	. . . . 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 27323	. . . . 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 14177	. . . 4 ⊢ (𝜑 → (𝑇↑0) = 1)
172	170, 171	eqtrd 2775	. . 3 ⊢ (𝜑 → (𝑋‘(1_r‘𝑍)) = 1)
173	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 89, 154, 172	dchrelbasd 27298	. 2 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷)
174	61, 44	sselid 3993	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
175		eleq1 2827	. . . . . . 7 ⊢ (𝑣 = 𝐴 → (𝑣 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈))
176		fveq2 6907	. . . . . . 7 ⊢ (𝑣 = 𝐴 → (𝑋‘𝑣) = (𝑋‘𝐴))
177	175, 176	ifbieq1d 4555	. . . . . 6 ⊢ (𝑣 = 𝐴 → if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
178		eqid 2735	. . . . . 6 ⊢ (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))
179		fvex 6920	. . . . . . 7 ⊢ (𝑋‘𝑣) ∈ V
180		c0ex 11253	. . . . . . 7 ⊢ 0 ∈ V
181	179, 180	ifex 4581	. . . . . 6 ⊢ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) ∈ V
182	177, 178, 181	fvmpt3i 7021	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
183	174, 182	syl 17	. . . 4 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
184	44	iftrued 4539	. . . 4 ⊢ (𝜑 → if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0) = (𝑋‘𝐴))
185	183, 184	eqtrd 2775	. . 3 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = (𝑋‘𝐴))
186		fveqeq2 6916	. . . . . 6 ⊢ (𝑣 = 𝐴 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))))
187	186	rexbidv 3177	. . . . 5 ⊢ (𝑣 = 𝐴 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))))
188	187, 92, 44	rspcdva 3623	. . . 4 ⊢ (𝜑 → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))
189	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 27323	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = (𝑇↑𝑎))
190	47	oveq1i 7441	. . . . . . . 8 ⊢ (𝑇↑𝑎) = ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎)
191	189, 190	eqtrdi 2791	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎))
192	48	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) ≠ 1 )
193	58	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝐻 ∈ Grp)
194	68	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑊‘𝐼) ∈ 𝑈)
195		simprl 771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ)
196	69, 46, 43, 160	oddvds 19580	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ Grp ∧ (𝑊‘𝐼) ∈ 𝑈 ∧ 𝑎 ∈ ℤ) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
197	193, 194, 195, 196	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
198	71	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
199		root1eq1 26813	. . . . . . . . . . 11 ⊢ (((𝑂‘(𝑊‘𝐼)) ∈ ℕ ∧ 𝑎 ∈ ℤ) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎))
200	198, 195, 199	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎))
201		simprr 773	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))
202	40, 164	eqtrid 2787	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 = (0_g‘𝐻))
203	202	ad2antrr 726	. . . . . . . . . . 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 2983	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1 ↔ ((𝑃‘𝐼)‘𝐴) ≠ 1 ))
207	192, 206	mpbird 257	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1)
208	191, 207	eqnetrd 3006	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) ≠ 1)
209	208	rexlimdvaa 3154	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑈) → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1))
210	44, 209	mpdan 687	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1))
211	188, 210	mpd 15	. . 3 ⊢ (𝜑 → (𝑋‘𝐴) ≠ 1)
212	185, 211	eqnetrd 3006	. 2 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1)
213		fveq1 6906	. . . 4 ⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → (𝑥‘𝐴) = ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴))
214	213	neeq1d 2998	. . 3 ⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → ((𝑥‘𝐴) ≠ 1 ↔ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1))
215	214	rspcev 3622	. 2 ⊢ (((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷 ∧ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
216	173, 212, 215	syl2anc 584	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 Vcvv 3478 ⊆ wss 3963 ifcif 4531 class class class wbr 5148 ↦ cmpt 5231 dom cdm 5689 ran crn 5690 ℩cio 6514 ⟶wf 6559 ‘cfv 6563 (class class class)co 7431 Fincfn 8984 ℂcc 11151 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 · cmul 11158 -cneg 11491 / cdiv 11918 ℕcn 12264 2c2 12319 ℕ₀cn0 12524 ℤcz 12611 ..^cfzo 13691 ↑cexp 14099 ♯chash 14366 Word cword 14549 ∥ cdvds 16287 Basecbs 17245 ↾_s cress 17274 +_gcplusg 17298 ._rcmulr 17299 0_gc0g 17486 Grpcgrp 18964 ._gcmg 19098 GrpHom cghm 19243 odcod 19557 DProd cdprd 20028 dProjcdpj 20029 mulGrpcmgp 20152 1_rcur 20199 Ringcrg 20251 CRingccrg 20252 Unitcui 20372 ℤ/nℤczn 21531 ↑_𝑐ccxp 26612 DChrcdchr 27291

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-inf2 9679 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231 ax-addf 11232 ax-mulf 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-tp 4636 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-iin 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-se 5642 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-isom 6572 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8013 df-2nd 8014 df-supp 8185 df-tpos 8250 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-2o 8506 df-oadd 8509 df-omul 8510 df-er 8744 df-ec 8746 df-qs 8750 df-map 8867 df-pm 8868 df-ixp 8937 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fsupp 9400 df-fi 9449 df-sup 9480 df-inf 9481 df-oi 9548 df-card 9977 df-acn 9980 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12525 df-z 12612 df-dec 12732 df-uz 12877 df-q 12989 df-rp 13033 df-xneg 13152 df-xadd 13153 df-xmul 13154 df-ioo 13388 df-ioc 13389 df-ico 13390 df-icc 13391 df-fz 13545 df-fzo 13692 df-fl 13829 df-mod 13907 df-seq 14040 df-exp 14100 df-fac 14310 df-bc 14339 df-hash 14367 df-word 14550 df-shft 15103 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-limsup 15504 df-clim 15521 df-rlim 15522 df-sum 15720 df-ef 16100 df-sin 16102 df-cos 16103 df-pi 16105 df-dvds 16288 df-struct 17181 df-sets 17198 df-slot 17216 df-ndx 17228 df-base 17246 df-ress 17275 df-plusg 17311 df-mulr 17312 df-starv 17313 df-sca 17314 df-vsca 17315 df-ip 17316 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-hom 17322 df-cco 17323 df-rest 17469 df-topn 17470 df-0g 17488 df-gsum 17489 df-topgen 17490 df-pt 17491 df-prds 17494 df-xrs 17549 df-qtop 17554 df-imas 17555 df-qus 17556 df-xps 17557 df-mre 17631 df-mrc 17632 df-acs 17634 df-mgm 18666 df-sgrp 18745 df-mnd 18761 df-mhm 18809 df-submnd 18810 df-grp 18967 df-minusg 18968 df-sbg 18969 df-mulg 19099 df-subg 19154 df-nsg 19155 df-eqg 19156 df-ghm 19244 df-gim 19290 df-cntz 19348 df-oppg 19377 df-od 19561 df-lsm 19669 df-pj1 19670 df-cmn 19815 df-abl 19816 df-dprd 20030 df-dpj 20031 df-mgp 20153 df-rng 20171 df-ur 20200 df-ring 20253 df-cring 20254 df-oppr 20351 df-dvdsr 20374 df-unit 20375 df-rhm 20489 df-subrng 20563 df-subrg 20587 df-lmod 20877 df-lss 20948 df-lsp 20988 df-sra 21190 df-rgmod 21191 df-lidl 21236 df-rsp 21237 df-2idl 21278 df-psmet 21374 df-xmet 21375 df-met 21376 df-bl 21377 df-mopn 21378 df-fbas 21379 df-fg 21380 df-cnfld 21383 df-zring 21476 df-zrh 21532 df-zn 21535 df-top 22916 df-topon 22933 df-topsp 22955 df-bases 22969 df-cld 23043 df-ntr 23044 df-cls 23045 df-nei 23122 df-lp 23160 df-perf 23161 df-cn 23251 df-cnp 23252 df-haus 23339 df-tx 23586 df-hmeo 23779 df-fil 23870 df-fm 23962 df-flim 23963 df-flf 23964 df-xms 24346 df-ms 24347 df-tms 24348 df-cncf 24918 df-limc 25916 df-dv 25917 df-log 26613 df-cxp 26614 df-dchr 27292

This theorem is referenced by: dchrptlem3 27325

W3C validator