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 27499

Description: Lemma for dchrpt 27501. (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 6882	. . 3 ⊢ (𝑣 = 𝑥 → (𝑋‘𝑣) = (𝑋‘𝑥))
8		fveq2 6882	. . 3 ⊢ (𝑣 = 𝑦 → (𝑋‘𝑣) = (𝑋‘𝑦))
9		fveq2 6882	. . 3 ⊢ (𝑣 = (𝑥(._r‘𝑍)𝑦) → (𝑋‘𝑣) = (𝑋‘(𝑥(._r‘𝑍)𝑦)))
10		fveq2 6882	. . 3 ⊢ (𝑣 = (1_r‘𝑍) → (𝑋‘𝑣) = (𝑋‘(1_r‘𝑍)))
11		dchrpt.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐻dom DProd 𝑆)
12		zex 12627	. . . . . . . . . . . . 13 ⊢ ℤ ∈ V
13	12	mptex 7225	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
14	13	rnex 7910	. . . . . . . . . . 11 ⊢ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
15		dchrpt.s	. . . . . . . . . . 11 ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))
16	14, 15	dmmpti 6680	. . . . . . . . . 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 20187	. . . . . . . 8 ⊢ (𝜑 → (𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼))
21		dchrpt.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)
22	21	feq2d 6690	. . . . . . . 8 ⊢ (𝜑 → ((𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼) ↔ (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼)))
23	20, 22	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼))
24	23	ffvelcdmda 7080	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ (𝑆‘𝐼))
25	19	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → 𝐼 ∈ dom 𝑊)
26		oveq1 7423	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑎 → (𝑛 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝑘)))
27	26	cbvmptv 5213	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘)))
28		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐼 → (𝑊‘𝑘) = (𝑊‘𝐼))
29	28	oveq2d 7432	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐼 → (𝑎 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝐼)))
30	29	mpteq2dv 5203	. . . . . . . . . 10 ⊢ (𝑘 = 𝐼 → (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
31	27, 30	eqtrid 2809	. . . . . . . . 9 ⊢ (𝑘 = 𝐼 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
32	31	rneqd 5926	. . . . . . . 8 ⊢ (𝑘 = 𝐼 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
33	32, 15, 14	fvmpt3i 6996	. . . . . . 7 ⊢ (𝐼 ∈ dom 𝑊 → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
34	25, 33	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
35	24, 34	eleqtrd 2864	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
36		eqid 2762	. . . . . 6 ⊢ (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))
37		ovex 7449	. . . . . 6 ⊢ (𝑎 · (𝑊‘𝐼)) ∈ V
38	36, 37	elrnmpti 5950	. . . . 5 ⊢ (((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
39	35, 38	sylib 221	. . . 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 27498	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) = (𝑇↑𝑎))
51		neg1cn 12230	. . . . . . . . 9 ⊢ -1 ∈ ℂ
52		2re 12342	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
53	5	nnnn0d 12592	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
54	2	zncrng 21758	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing)
55		crngring 20385	. . . . . . . . . . . . . 14 ⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring)
56	53, 54, 55	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ Ring)
57	4, 42	unitgrp 20525	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp)
58	56, 57	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 ∈ Grp)
59	2, 3	znfi 21773	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
60	5, 59	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ Fin)
61	3, 4	unitss 20518	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ 𝐵
62		ssfi 9170	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin)
63	60, 61, 62	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ Fin)
64		wrdf 14585	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ Word 𝑈 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
65	45, 64	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
66	65	fdmd 6717	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
67	19, 66	eleqtrd 2864	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝑊)))
68	65, 67	ffvelcdmd 7081	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑈)
69	4, 42	unitgrpbas 20524	. . . . . . . . . . . . 13 ⊢ 𝑈 = (Base‘𝐻)
70	69, 46	odcl2 19693	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊‘𝐼) ∈ 𝑈) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
71	58, 63, 68, 70	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
72		nndivre 12304	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (𝑂‘(𝑊‘𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
73	52, 71, 72	sylancr 599	. . . . . . . . . 10 ⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
74	73	recnd 11264	. . . . . . . . 9 ⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ)
75		cxpcl 26909	. . . . . . . . 9 ⊢ ((-1 ∈ ℂ ∧ (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
76	51, 74, 75	sylancr 599	. . . . . . . 8 ⊢ (𝜑 → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
77	47, 76	eqeltrid 2866	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℂ)
78	77	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ∈ ℂ)
79	51	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → -1 ∈ ℂ)
80		neg1ne0 12232	. . . . . . . . . 10 ⊢ -1 ≠ 0
81	80	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → -1 ≠ 0)
82	79, 81, 74	cxpne0d 26948	. . . . . . . 8 ⊢ (𝜑 → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
83	47	neeq1i 3021	. . . . . . . 8 ⊢ (𝑇 ≠ 0 ↔ (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
84	82, 83	sylibr 237	. . . . . . 7 ⊢ (𝜑 → 𝑇 ≠ 0)
85	84	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ≠ 0)
86		simprl 783	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ)
87	78, 85, 86	expclzd 14217	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑇↑𝑎) ∈ ℂ)
88	50, 87	eqeltrd 2862	. . . 4 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) ∈ ℂ)
89	39, 88	rexlimddv 3171	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑋‘𝑣) ∈ ℂ)
90		fveqeq2 6891	. . . . . 6 ⊢ (𝑣 = 𝑥 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))))
91	90	rexbidv 3188	. . . . 5 ⊢ (𝑣 = 𝑥 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))))
92	39	ralrimiva 3156	. . . . . 6 ⊢ (𝜑 → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
93	92	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
94		simprl 783	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
95	91, 93, 94	rspcdva 3580	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))
96		fveqeq2 6891	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼))))
97	96	rexbidv 3188	. . . . . 6 ⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼))))
98		oveq1 7423	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝑎 · (𝑊‘𝐼)) = (𝑏 · (𝑊‘𝐼)))
99	98	eqeq2d 2773	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
100	99	cbvrexvw 3243	. . . . . 6 ⊢ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
101	97, 100	bitrdi 290	. . . . 5 ⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
102		simprr 785	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
103	101, 93, 102	rspcdva 3580	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
104		reeanv 3236	. . . . 5 ⊢ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) ↔ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
105	77	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ∈ ℂ)
106	84	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ≠ 0)
107		simprll 791	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑎 ∈ ℤ)
108		simprlr 792	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑏 ∈ ℤ)
109		expaddz 14172	. . . . . . . . 9 ⊢ (((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
110	105, 106, 107, 108, 109	syl22anc 852	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
111		simpll 779	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝜑)
112	56	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑍 ∈ Ring)
113	94	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑥 ∈ 𝑈)
114	102	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑦 ∈ 𝑈)
115		eqid 2762	. . . . . . . . . . 11 ⊢ (._r‘𝑍) = (._r‘𝑍)
116	4, 115	unitmulcl 20522	. . . . . . . . . 10 ⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝑍)𝑦) ∈ 𝑈)
117	112, 113, 114, 116	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑥(._r‘𝑍)𝑦) ∈ 𝑈)
118	107, 108	zaddcld 12732	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑎 + 𝑏) ∈ ℤ)
119		simprrl 793	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))
120		simprrr 794	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
121	119, 120	oveq12d 7434	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
122	11, 17, 18, 19	dpjghm 20193	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃‘𝐼) ∈ ((𝐻 ↾_s (𝐻 DProd 𝑆)) GrpHom 𝐻))
123	21	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻 ↾_s (𝐻 DProd 𝑆)) = (𝐻 ↾_s 𝑈))
124	42	ovexi 7450	. . . . . . . . . . . . . . . 16 ⊢ 𝐻 ∈ V
125	69	ressid 17340	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ V → (𝐻 ↾_s 𝑈) = 𝐻)
126	124, 125	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ↾_s 𝑈) = 𝐻
127	123, 126	eqtrdi 2813	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻 ↾_s (𝐻 DProd 𝑆)) = 𝐻)
128	127	oveq1d 7431	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐻 ↾_s (𝐻 DProd 𝑆)) GrpHom 𝐻) = (𝐻 GrpHom 𝐻))
129	122, 128	eleqtrd 2864	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻))
130	129	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻))
131	4	fvexi 6896	. . . . . . . . . . . . 13 ⊢ 𝑈 ∈ V
132		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
133	132, 115	mgpplusg 20278	. . . . . . . . . . . . . 14 ⊢ (._r‘𝑍) = (+_g‘(mulGrp‘𝑍))
134	42, 133	ressplusg 17380	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ V → (._r‘𝑍) = (+_g‘𝐻))
135	131, 134	ax-mp 5	. . . . . . . . . . . 12 ⊢ (._r‘𝑍) = (+_g‘𝐻)
136	69, 135, 135	ghmlin 19349	. . . . . . . . . . 11 ⊢ (((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)))
137	130, 113, 114, 136	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)))
138	58	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝐻 ∈ Grp)
139	68	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑊‘𝐼) ∈ 𝑈)
140	69, 43, 135	mulgdir 19230	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ Grp ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ (𝑊‘𝐼) ∈ 𝑈)) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
141	138, 107, 108, 139, 140	syl13anc 1399	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
142	121, 137, 141	3eqtr4d 2807	. . . . . . . . 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 27498	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥(._r‘𝑍)𝑦) ∈ 𝑈) ∧ ((𝑎 + 𝑏) ∈ ℤ ∧ ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊‘𝐼)))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏)))
144	111, 117, 118, 142, 143	syl22anc 852	. . . . . . . 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 27498	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑥) = (𝑇↑𝑎))
146	111, 113, 107, 119, 145	syl22anc 852	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑥) = (𝑇↑𝑎))
147	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 27498	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑈) ∧ (𝑏 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) → (𝑋‘𝑦) = (𝑇↑𝑏))
148	111, 114, 108, 120, 147	syl22anc 852	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑦) = (𝑇↑𝑏))
149	146, 148	oveq12d 7434	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑋‘𝑥) · (𝑋‘𝑦)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
150	110, 144, 149	3eqtr4d 2807	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
151	150	expr 462	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
152	151	rexlimdvva 3221	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
153	104, 152	biimtrrid 246	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
154	95, 103, 153	mp2and 712	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
155		id 23	. . . . 5 ⊢ (𝜑 → 𝜑)
156		eqid 2762	. . . . . . 7 ⊢ (1_r‘𝑍) = (1_r‘𝑍)
157	4, 156	1unit 20516	. . . . . 6 ⊢ (𝑍 ∈ Ring → (1_r‘𝑍) ∈ 𝑈)
158	56, 157	syl 18	. . . . 5 ⊢ (𝜑 → (1_r‘𝑍) ∈ 𝑈)
159		0zd 12630	. . . . 5 ⊢ (𝜑 → 0 ∈ ℤ)
160		eqid 2762	. . . . . . . 8 ⊢ (0_g‘𝐻) = (0_g‘𝐻)
161	160, 160	ghmid 19350	. . . . . . 7 ⊢ ((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) → ((𝑃‘𝐼)‘(0_g‘𝐻)) = (0_g‘𝐻))
162	129, 161	syl 18	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘(0_g‘𝐻)) = (0_g‘𝐻))
163	4, 42, 156	unitgrpid 20527	. . . . . . . 8 ⊢ (𝑍 ∈ Ring → (1_r‘𝑍) = (0_g‘𝐻))
164	56, 163	syl 18	. . . . . . 7 ⊢ (𝜑 → (1_r‘𝑍) = (0_g‘𝐻))
165	164	fveq2d 6886	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘(1_r‘𝑍)) = ((𝑃‘𝐼)‘(0_g‘𝐻)))
166	69, 160, 43	mulg0 19198	. . . . . . 7 ⊢ ((𝑊‘𝐼) ∈ 𝑈 → (0 · (𝑊‘𝐼)) = (0_g‘𝐻))
167	68, 166	syl 18	. . . . . 6 ⊢ (𝜑 → (0 · (𝑊‘𝐼)) = (0_g‘𝐻))
168	162, 165, 167	3eqtr4d 2807	. . . . 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 27498	. . . . 5 ⊢ (((𝜑 ∧ (1_r‘𝑍) ∈ 𝑈) ∧ (0 ∈ ℤ ∧ ((𝑃‘𝐼)‘(1_r‘𝑍)) = (0 · (𝑊‘𝐼)))) → (𝑋‘(1_r‘𝑍)) = (𝑇↑0))
170	155, 158, 159, 168, 169	syl22anc 852	. . . 4 ⊢ (𝜑 → (𝑋‘(1_r‘𝑍)) = (𝑇↑0))
171	77	exp0d 14206	. . . 4 ⊢ (𝜑 → (𝑇↑0) = 1)
172	170, 171	eqtrd 2797	. . 3 ⊢ (𝜑 → (𝑋‘(1_r‘𝑍)) = 1)
173	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 89, 154, 172	dchrelbasd 27473	. 2 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷)
174	61, 44	sselid 3932	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
175		eleq1 2850	. . . . . . 7 ⊢ (𝑣 = 𝐴 → (𝑣 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈))
176		fveq2 6882	. . . . . . 7 ⊢ (𝑣 = 𝐴 → (𝑋‘𝑣) = (𝑋‘𝐴))
177	175, 176	ifbieq1d 4510	. . . . . 6 ⊢ (𝑣 = 𝐴 → if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
178		eqid 2762	. . . . . 6 ⊢ (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))
179		fvex 6895	. . . . . . 7 ⊢ (𝑋‘𝑣) ∈ V
180		c0ex 11227	. . . . . . 7 ⊢ 0 ∈ V
181	179, 180	ifex 4536	. . . . . 6 ⊢ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) ∈ V
182	177, 178, 181	fvmpt3i 6996	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
183	174, 182	syl 18	. . . 4 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
184	44	iftrued 4493	. . . 4 ⊢ (𝜑 → if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0) = (𝑋‘𝐴))
185	183, 184	eqtrd 2797	. . 3 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = (𝑋‘𝐴))
186		fveqeq2 6891	. . . . . 6 ⊢ (𝑣 = 𝐴 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))))
187	186	rexbidv 3188	. . . . 5 ⊢ (𝑣 = 𝐴 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))))
188	187, 92, 44	rspcdva 3580	. . . 4 ⊢ (𝜑 → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))
189	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 27498	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = (𝑇↑𝑎))
190	47	oveq1i 7426	. . . . . . . 8 ⊢ (𝑇↑𝑎) = ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎)
191	189, 190	eqtrdi 2813	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎))
192	48	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) ≠ 1 )
193	58	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝐻 ∈ Grp)
194	68	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑊‘𝐼) ∈ 𝑈)
195		simprl 783	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ)
196	69, 46, 43, 160	oddvds 19675	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ Grp ∧ (𝑊‘𝐼) ∈ 𝑈 ∧ 𝑎 ∈ ℤ) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
197	193, 194, 195, 196	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
198	71	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
199		root1eq1 26990	. . . . . . . . . . 11 ⊢ (((𝑂‘(𝑊‘𝐼)) ∈ ℕ ∧ 𝑎 ∈ ℤ) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎))
200	198, 195, 199	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎))
201		simprr 785	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))
202	40, 164	eqtrid 2809	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 = (0_g‘𝐻))
203	202	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 1 = (0_g‘𝐻))
204	201, 203	eqeq12d 2778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((𝑃‘𝐼)‘𝐴) = 1 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
205	197, 200, 204	3bitr4d 314	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ ((𝑃‘𝐼)‘𝐴) = 1 ))
206	205	necon3bid 3001	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1 ↔ ((𝑃‘𝐼)‘𝐴) ≠ 1 ))
207	192, 206	mpbird 260	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1)
208	191, 207	eqnetrd 3024	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) ≠ 1)
209	208	rexlimdvaa 3166	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑈) → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1))
210	44, 209	mpdan 700	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1))
211	188, 210	mpd 16	. . 3 ⊢ (𝜑 → (𝑋‘𝐴) ≠ 1)
212	185, 211	eqnetrd 3024	. 2 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1)
213		fveq1 6881	. . . 4 ⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → (𝑥‘𝐴) = ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴))
214	213	neeq1d 3016	. . 3 ⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → ((𝑥‘𝐴) ≠ 1 ↔ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1))
215	214	rspcev 3579	. 2 ⊢ (((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷 ∧ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
216	173, 212, 215	syl2anc 596	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 Vcvv 3453 ⊆ wss 3902 ifcif 4485 class class class wbr 5107 ↦ cmpt 5190 dom cdm 5659 ran crn 5660 ℩cio 6491 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 Fincfn 8955 ℂcc 11125 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 -cneg 11469 / cdiv 11898 ℕcn 12260 2c2 12322 ℕ₀cn0 12531 ℤcz 12618 ..^cfzo 13711 ↑cexp 14127 ♯chash 14396 Word cword 14580 ∥ cdvds 16346 Basecbs 17305 ↾_s cress 17326 +_gcplusg 17346 ._rcmulr 17347 0_gc0g 17528 Grpcgrp 19058 ._gcmg 19191 GrpHom cghm 19341 odcod 19652 DProd cdprd 20123 dProjcdpj 20124 mulGrpcmgp 20274 1_rcur 20321 Ringcrg 20373 CRingccrg 20374 Unitcui 20497 ℤ/nℤczn 21716 ↑_𝑐ccxp 26790 DChrcdchr 27466

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205 ax-addf 11206 ax-mulf 11207

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7681 df-om 7866 df-1st 7989 df-2nd 7990 df-supp 8162 df-tpos 8227 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-2o 8459 df-oadd 8462 df-omul 8463 df-er 8699 df-ec 8701 df-qs 8705 df-map 8831 df-pm 8832 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9335 df-fi 9384 df-sup 9415 df-inf 9416 df-oi 9485 df-card 9947 df-acn 9950 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-q 13001 df-rp 13045 df-xneg 13165 df-xadd 13166 df-xmul 13167 df-ioo 13404 df-ioc 13405 df-ico 13406 df-icc 13407 df-fz 13564 df-fzo 13712 df-fl 13855 df-mod 13933 df-seq 14068 df-exp 14128 df-fac 14340 df-bc 14369 df-hash 14397 df-word 14581 df-shft 15142 df-cj 15188 df-re 15189 df-im 15190 df-sqrt 15324 df-abs 15325 df-limsup 15560 df-clim 15577 df-rlim 15578 df-sum 15776 df-ef 16157 df-sin 16159 df-cos 16160 df-pi 16162 df-dvds 16347 df-struct 17243 df-sets 17260 df-slot 17278 df-ndx 17290 df-base 17306 df-ress 17327 df-plusg 17359 df-mulr 17360 df-starv 17361 df-sca 17362 df-vsca 17363 df-ip 17364 df-tset 17365 df-ple 17366 df-ds 17368 df-unif 17369 df-hom 17370 df-cco 17371 df-rest 17511 df-topn 17512 df-0g 17530 df-gsum 17531 df-topgen 17532 df-pt 17533 df-prds 17536 df-xrs 17592 df-qtop 17597 df-imas 17598 df-qus 17599 df-xps 17600 df-mre 17674 df-mrc 17675 df-acs 17677 df-mgm 18734 df-sgrp 18823 df-mnd 18839 df-mhm 18892 df-submnd 18893 df-grp 19061 df-minusg 19062 df-sbg 19063 df-mulg 19192 df-subg 19247 df-nsg 19248 df-eqg 19249 df-ghm 19342 df-gim 19387 df-cntz 19445 df-oppg 19474 df-od 19656 df-lsm 19764 df-pj1 19765 df-cmn 19910 df-abl 19911 df-dprd 20125 df-dpj 20126 df-mgp 20275 df-rng 20289 df-ur 20322 df-ring 20375 df-cring 20376 df-oppr 20479 df-dvdsr 20499 df-unit 20500 df-rhm 20614 df-subrng 20709 df-subrg 20733 df-lmod 21047 df-lss 21117 df-lsp 21157 df-sra 21358 df-rgmod 21359 df-lidl 21396 df-rsp 21397 df-2idl 21453 df-psmet 21578 df-xmet 21579 df-met 21580 df-bl 21581 df-mopn 21582 df-fbas 21583 df-fg 21584 df-cnfld 21587 df-zring 21661 df-zrh 21717 df-zn 21720 df-top 23120 df-topon 23137 df-topsp 23159 df-bases 23172 df-cld 23245 df-ntr 23246 df-cls 23247 df-nei 23324 df-lp 23362 df-perf 23363 df-cn 23453 df-cnp 23454 df-haus 23541 df-tx 23789 df-hmeo 23982 df-fil 24073 df-fm 24165 df-flim 24166 df-flf 24167 df-xms 24547 df-ms 24548 df-tms 24549 df-cncf 25107 df-limc 26095 df-dv 26096 df-log 26791 df-cxp 26792 df-dchr 27467

This theorem is used by: dchrptlem3 27500

W3C validator