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 25841

Description: Lemma for dchrpt 25843. (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 6670	. . 3 ⊢ (𝑣 = 𝑥 → (𝑋‘𝑣) = (𝑋‘𝑥))
8		fveq2 6670	. . 3 ⊢ (𝑣 = 𝑦 → (𝑋‘𝑣) = (𝑋‘𝑦))
9		fveq2 6670	. . 3 ⊢ (𝑣 = (𝑥(._r‘𝑍)𝑦) → (𝑋‘𝑣) = (𝑋‘(𝑥(._r‘𝑍)𝑦)))
10		fveq2 6670	. . 3 ⊢ (𝑣 = (1_r‘𝑍) → (𝑋‘𝑣) = (𝑋‘(1_r‘𝑍)))
11		dchrpt.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐻dom DProd 𝑆)
12		zex 11991	. . . . . . . . . . . . 13 ⊢ ℤ ∈ V
13	12	mptex 6986	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
14	13	rnex 7617	. . . . . . . . . . 11 ⊢ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
15		dchrpt.s	. . . . . . . . . . 11 ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))
16	14, 15	dmmpti 6492	. . . . . . . . . 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 19179	. . . . . . . 8 ⊢ (𝜑 → (𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼))
21		dchrpt.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)
22	21	feq2d 6500	. . . . . . . 8 ⊢ (𝜑 → ((𝑃‘𝐼):(𝐻 DProd 𝑆)⟶(𝑆‘𝐼) ↔ (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼)))
23	20, 22	mpbid 234	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝐼):𝑈⟶(𝑆‘𝐼))
24	23	ffvelrnda 6851	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ (𝑆‘𝐼))
25	19	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → 𝐼 ∈ dom 𝑊)
26		oveq1 7163	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑎 → (𝑛 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝑘)))
27	26	cbvmptv 5169	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘)))
28		fveq2 6670	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐼 → (𝑊‘𝑘) = (𝑊‘𝐼))
29	28	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐼 → (𝑎 · (𝑊‘𝑘)) = (𝑎 · (𝑊‘𝐼)))
30	29	mpteq2dv 5162	. . . . . . . . . 10 ⊢ (𝑘 = 𝐼 → (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
31	27, 30	syl5eq 2868	. . . . . . . . 9 ⊢ (𝑘 = 𝐼 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
32	31	rneqd 5808	. . . . . . . 8 ⊢ (𝑘 = 𝐼 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
33	32, 15, 14	fvmpt3i 6773	. . . . . . 7 ⊢ (𝐼 ∈ dom 𝑊 → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
34	25, 33	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑆‘𝐼) = ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
35	24, 34	eleqtrd 2915	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → ((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))))
36		eqid 2821	. . . . . 6 ⊢ (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) = (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼)))
37		ovex 7189	. . . . . 6 ⊢ (𝑎 · (𝑊‘𝐼)) ∈ V
38	36, 37	elrnmpti 5832	. . . . 5 ⊢ (((𝑃‘𝐼)‘𝑣) ∈ ran (𝑎 ∈ ℤ ↦ (𝑎 · (𝑊‘𝐼))) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
39	35, 38	sylib 220	. . . 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 25840	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) = (𝑇↑𝑎))
51		neg1cn 11752	. . . . . . . . 9 ⊢ -1 ∈ ℂ
52		2re 11712	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
53	5	nnnn0d 11956	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
54	2	zncrng 20691	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing)
55		crngring 19308	. . . . . . . . . . . . . 14 ⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring)
56	53, 54, 55	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ Ring)
57	4, 42	unitgrp 19417	. . . . . . . . . . . . 13 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp)
58	56, 57	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 ∈ Grp)
59	2, 3	znfi 20706	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
60	5, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ Fin)
61	3, 4	unitss 19410	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ 𝐵
62		ssfi 8738	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin)
63	60, 61, 62	sylancl 588	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ Fin)
64		wrdf 13867	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ Word 𝑈 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
65	45, 64	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
66	65	fdmd 6523	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
67	19, 66	eleqtrd 2915	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝑊)))
68	65, 67	ffvelrnd 6852	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑈)
69	4, 42	unitgrpbas 19416	. . . . . . . . . . . . 13 ⊢ 𝑈 = (Base‘𝐻)
70	69, 46	odcl2 18692	. . . . . . . . . . . 12 ⊢ ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊‘𝐼) ∈ 𝑈) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
71	58, 63, 68, 70	syl3anc 1367	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
72		nndivre 11679	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ (𝑂‘(𝑊‘𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
73	52, 71, 72	sylancr 589	. . . . . . . . . 10 ⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
74	73	recnd 10669	. . . . . . . . 9 ⊢ (𝜑 → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ)
75		cxpcl 25257	. . . . . . . . 9 ⊢ ((-1 ∈ ℂ ∧ (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
76	51, 74, 75	sylancr 589	. . . . . . . 8 ⊢ (𝜑 → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
77	47, 76	eqeltrid 2917	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℂ)
78	77	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ∈ ℂ)
79	51	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → -1 ∈ ℂ)
80		neg1ne0 11754	. . . . . . . . . 10 ⊢ -1 ≠ 0
81	80	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → -1 ≠ 0)
82	79, 81, 74	cxpne0d 25296	. . . . . . . 8 ⊢ (𝜑 → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
83	47	neeq1i 3080	. . . . . . . 8 ⊢ (𝑇 ≠ 0 ↔ (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
84	82, 83	sylibr 236	. . . . . . 7 ⊢ (𝜑 → 𝑇 ≠ 0)
85	84	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑇 ≠ 0)
86		simprl 769	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ)
87	78, 85, 86	expclzd 13516	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑇↑𝑎) ∈ ℂ)
88	50, 87	eqeltrd 2913	. . . 4 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑣) ∈ ℂ)
89	39, 88	rexlimddv 3291	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑈) → (𝑋‘𝑣) ∈ ℂ)
90		fveqeq2 6679	. . . . . 6 ⊢ (𝑣 = 𝑥 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))))
91	90	rexbidv 3297	. . . . 5 ⊢ (𝑣 = 𝑥 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼))))
92	39	ralrimiva 3182	. . . . . 6 ⊢ (𝜑 → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
93	92	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∀𝑣 ∈ 𝑈 ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)))
94		simprl 769	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
95	91, 93, 94	rspcdva 3625	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))
96		fveqeq2 6679	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼))))
97	96	rexbidv 3297	. . . . . 6 ⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼))))
98		oveq1 7163	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝑎 · (𝑊‘𝐼)) = (𝑏 · (𝑊‘𝐼)))
99	98	eqeq2d 2832	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
100	99	cbvrexvw 3450	. . . . . 6 ⊢ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
101	97, 100	syl6bb 289	. . . . 5 ⊢ (𝑣 = 𝑦 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
102		simprr 771	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
103	101, 93, 102	rspcdva 3625	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
104		reeanv 3367	. . . . 5 ⊢ (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) ↔ (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))
105	77	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ∈ ℂ)
106	84	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑇 ≠ 0)
107		simprll 777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑎 ∈ ℤ)
108		simprlr 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑏 ∈ ℤ)
109		expaddz 13474	. . . . . . . . 9 ⊢ (((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
110	105, 106, 107, 108, 109	syl22anc 836	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑇↑(𝑎 + 𝑏)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
111		simpll 765	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝜑)
112	56	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑍 ∈ Ring)
113	94	adantr 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑥 ∈ 𝑈)
114	102	adantr 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝑦 ∈ 𝑈)
115		eqid 2821	. . . . . . . . . . 11 ⊢ (._r‘𝑍) = (._r‘𝑍)
116	4, 115	unitmulcl 19414	. . . . . . . . . 10 ⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥(._r‘𝑍)𝑦) ∈ 𝑈)
117	112, 113, 114, 116	syl3anc 1367	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑥(._r‘𝑍)𝑦) ∈ 𝑈)
118	107, 108	zaddcld 12092	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑎 + 𝑏) ∈ ℤ)
119		simprrl 779	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))
120		simprrr 780	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))
121	119, 120	oveq12d 7174	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
122	11, 17, 18, 19	dpjghm 19185	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃‘𝐼) ∈ ((𝐻 ↾_s (𝐻 DProd 𝑆)) GrpHom 𝐻))
123	21	oveq2d 7172	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻 ↾_s (𝐻 DProd 𝑆)) = (𝐻 ↾_s 𝑈))
124	42	ovexi 7190	. . . . . . . . . . . . . . . 16 ⊢ 𝐻 ∈ V
125	69	ressid 16559	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ V → (𝐻 ↾_s 𝑈) = 𝐻)
126	124, 125	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ↾_s 𝑈) = 𝐻
127	123, 126	syl6eq 2872	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻 ↾_s (𝐻 DProd 𝑆)) = 𝐻)
128	127	oveq1d 7171	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐻 ↾_s (𝐻 DProd 𝑆)) GrpHom 𝐻) = (𝐻 GrpHom 𝐻))
129	122, 128	eleqtrd 2915	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻))
130	129	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻))
131	4	fvexi 6684	. . . . . . . . . . . . 13 ⊢ 𝑈 ∈ V
132		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
133	132, 115	mgpplusg 19243	. . . . . . . . . . . . . 14 ⊢ (._r‘𝑍) = (+_g‘(mulGrp‘𝑍))
134	42, 133	ressplusg 16612	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ V → (._r‘𝑍) = (+_g‘𝐻))
135	131, 134	ax-mp 5	. . . . . . . . . . . 12 ⊢ (._r‘𝑍) = (+_g‘𝐻)
136	69, 135, 135	ghmlin 18363	. . . . . . . . . . 11 ⊢ (((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)))
137	130, 113, 114, 136	syl3anc 1367	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = (((𝑃‘𝐼)‘𝑥)(._r‘𝑍)((𝑃‘𝐼)‘𝑦)))
138	58	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → 𝐻 ∈ Grp)
139	68	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑊‘𝐼) ∈ 𝑈)
140	69, 43, 135	mulgdir 18259	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ Grp ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ (𝑊‘𝐼) ∈ 𝑈)) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
141	138, 107, 108, 139, 140	syl13anc 1368	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑎 + 𝑏) · (𝑊‘𝐼)) = ((𝑎 · (𝑊‘𝐼))(._r‘𝑍)(𝑏 · (𝑊‘𝐼))))
142	121, 137, 141	3eqtr4d 2866	. . . . . . . . 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 25840	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥(._r‘𝑍)𝑦) ∈ 𝑈) ∧ ((𝑎 + 𝑏) ∈ ℤ ∧ ((𝑃‘𝐼)‘(𝑥(._r‘𝑍)𝑦)) = ((𝑎 + 𝑏) · (𝑊‘𝐼)))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = (𝑇↑(𝑎 + 𝑏)))
144	111, 117, 118, 142, 143	syl22anc 836	. . . . . . . 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 25840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝑥) = (𝑇↑𝑎))
146	111, 113, 107, 119, 145	syl22anc 836	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑥) = (𝑇↑𝑎))
147	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 25840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑈) ∧ (𝑏 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼)))) → (𝑋‘𝑦) = (𝑇↑𝑏))
148	111, 114, 108, 120, 147	syl22anc 836	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘𝑦) = (𝑇↑𝑏))
149	146, 148	oveq12d 7174	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → ((𝑋‘𝑥) · (𝑋‘𝑦)) = ((𝑇↑𝑎) · (𝑇↑𝑏)))
150	110, 144, 149	3eqtr4d 2866	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) ∧ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
151	150	expr 459	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
152	151	rexlimdvva 3294	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
153	104, 152	syl5bir 245	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑥) = (𝑎 · (𝑊‘𝐼)) ∧ ∃𝑏 ∈ ℤ ((𝑃‘𝐼)‘𝑦) = (𝑏 · (𝑊‘𝐼))) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))
154	95, 103, 153	mp2and 697	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
155		id 22	. . . . 5 ⊢ (𝜑 → 𝜑)
156		eqid 2821	. . . . . . 7 ⊢ (1_r‘𝑍) = (1_r‘𝑍)
157	4, 156	1unit 19408	. . . . . 6 ⊢ (𝑍 ∈ Ring → (1_r‘𝑍) ∈ 𝑈)
158	56, 157	syl 17	. . . . 5 ⊢ (𝜑 → (1_r‘𝑍) ∈ 𝑈)
159		0zd 11994	. . . . 5 ⊢ (𝜑 → 0 ∈ ℤ)
160		eqid 2821	. . . . . . . 8 ⊢ (0_g‘𝐻) = (0_g‘𝐻)
161	160, 160	ghmid 18364	. . . . . . 7 ⊢ ((𝑃‘𝐼) ∈ (𝐻 GrpHom 𝐻) → ((𝑃‘𝐼)‘(0_g‘𝐻)) = (0_g‘𝐻))
162	129, 161	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘(0_g‘𝐻)) = (0_g‘𝐻))
163	4, 42, 156	unitgrpid 19419	. . . . . . . 8 ⊢ (𝑍 ∈ Ring → (1_r‘𝑍) = (0_g‘𝐻))
164	56, 163	syl 17	. . . . . . 7 ⊢ (𝜑 → (1_r‘𝑍) = (0_g‘𝐻))
165	164	fveq2d 6674	. . . . . 6 ⊢ (𝜑 → ((𝑃‘𝐼)‘(1_r‘𝑍)) = ((𝑃‘𝐼)‘(0_g‘𝐻)))
166	69, 160, 43	mulg0 18231	. . . . . . 7 ⊢ ((𝑊‘𝐼) ∈ 𝑈 → (0 · (𝑊‘𝐼)) = (0_g‘𝐻))
167	68, 166	syl 17	. . . . . 6 ⊢ (𝜑 → (0 · (𝑊‘𝐼)) = (0_g‘𝐻))
168	162, 165, 167	3eqtr4d 2866	. . . . 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 25840	. . . . 5 ⊢ (((𝜑 ∧ (1_r‘𝑍) ∈ 𝑈) ∧ (0 ∈ ℤ ∧ ((𝑃‘𝐼)‘(1_r‘𝑍)) = (0 · (𝑊‘𝐼)))) → (𝑋‘(1_r‘𝑍)) = (𝑇↑0))
170	155, 158, 159, 168, 169	syl22anc 836	. . . 4 ⊢ (𝜑 → (𝑋‘(1_r‘𝑍)) = (𝑇↑0))
171	77	exp0d 13505	. . . 4 ⊢ (𝜑 → (𝑇↑0) = 1)
172	170, 171	eqtrd 2856	. . 3 ⊢ (𝜑 → (𝑋‘(1_r‘𝑍)) = 1)
173	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 89, 154, 172	dchrelbasd 25815	. 2 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷)
174	61, 44	sseldi 3965	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
175		eleq1 2900	. . . . . . 7 ⊢ (𝑣 = 𝐴 → (𝑣 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈))
176		fveq2 6670	. . . . . . 7 ⊢ (𝑣 = 𝐴 → (𝑋‘𝑣) = (𝑋‘𝐴))
177	175, 176	ifbieq1d 4490	. . . . . 6 ⊢ (𝑣 = 𝐴 → if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
178		eqid 2821	. . . . . 6 ⊢ (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))
179		fvex 6683	. . . . . . 7 ⊢ (𝑋‘𝑣) ∈ V
180		c0ex 10635	. . . . . . 7 ⊢ 0 ∈ V
181	179, 180	ifex 4515	. . . . . 6 ⊢ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0) ∈ V
182	177, 178, 181	fvmpt3i 6773	. . . . 5 ⊢ (𝐴 ∈ 𝐵 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
183	174, 182	syl 17	. . . 4 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0))
184	44	iftrued 4475	. . . 4 ⊢ (𝜑 → if(𝐴 ∈ 𝑈, (𝑋‘𝐴), 0) = (𝑋‘𝐴))
185	183, 184	eqtrd 2856	. . 3 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) = (𝑋‘𝐴))
186		fveqeq2 6679	. . . . . 6 ⊢ (𝑣 = 𝐴 → (((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))))
187	186	rexbidv 3297	. . . . 5 ⊢ (𝑣 = 𝐴 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝑣) = (𝑎 · (𝑊‘𝐼)) ↔ ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼))))
188	187, 92, 44	rspcdva 3625	. . . 4 ⊢ (𝜑 → ∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))
189	1, 2, 6, 3, 40, 5, 41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49	dchrptlem1 25840	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = (𝑇↑𝑎))
190	47	oveq1i 7166	. . . . . . . 8 ⊢ (𝑇↑𝑎) = ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎)
191	189, 190	syl6eq 2872	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) = ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎))
192	48	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) ≠ 1 )
193	58	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝐻 ∈ Grp)
194	68	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑊‘𝐼) ∈ 𝑈)
195		simprl 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 𝑎 ∈ ℤ)
196	69, 46, 43, 160	oddvds 18675	. . . . . . . . . . 11 ⊢ ((𝐻 ∈ Grp ∧ (𝑊‘𝐼) ∈ 𝑈 ∧ 𝑎 ∈ ℤ) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
197	193, 194, 195, 196	syl3anc 1367	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑂‘(𝑊‘𝐼)) ∥ 𝑎 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
198	71	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
199		root1eq1 25336	. . . . . . . . . . 11 ⊢ (((𝑂‘(𝑊‘𝐼)) ∈ ℕ ∧ 𝑎 ∈ ℤ) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎))
200	198, 195, 199	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ 𝑎))
201		simprr 771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))
202	40, 164	syl5eq 2868	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 = (0_g‘𝐻))
203	202	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → 1 = (0_g‘𝐻))
204	201, 203	eqeq12d 2837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((𝑃‘𝐼)‘𝐴) = 1 ↔ (𝑎 · (𝑊‘𝐼)) = (0_g‘𝐻)))
205	197, 200, 204	3bitr4d 313	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) = 1 ↔ ((𝑃‘𝐼)‘𝐴) = 1 ))
206	205	necon3bid 3060	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1 ↔ ((𝑃‘𝐼)‘𝐴) ≠ 1 ))
207	192, 206	mpbird 259	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑𝑎) ≠ 1)
208	191, 207	eqnetrd 3083	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ 𝑈) ∧ (𝑎 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)))) → (𝑋‘𝐴) ≠ 1)
209	208	rexlimdvaa 3285	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑈) → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1))
210	44, 209	mpdan 685	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ ℤ ((𝑃‘𝐼)‘𝐴) = (𝑎 · (𝑊‘𝐼)) → (𝑋‘𝐴) ≠ 1))
211	188, 210	mpd 15	. . 3 ⊢ (𝜑 → (𝑋‘𝐴) ≠ 1)
212	185, 211	eqnetrd 3083	. 2 ⊢ (𝜑 → ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1)
213		fveq1 6669	. . . 4 ⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → (𝑥‘𝐴) = ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴))
214	213	neeq1d 3075	. . 3 ⊢ (𝑥 = (𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) → ((𝑥‘𝐴) ≠ 1 ↔ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1))
215	214	rspcev 3623	. 2 ⊢ (((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0)) ∈ 𝐷 ∧ ((𝑣 ∈ 𝐵 ↦ if(𝑣 ∈ 𝑈, (𝑋‘𝑣), 0))‘𝐴) ≠ 1) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
216	173, 212, 215	syl2anc 586	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 Vcvv 3494 ⊆ wss 3936 ifcif 4467 class class class wbr 5066 ↦ cmpt 5146 dom cdm 5555 ran crn 5556 ℩cio 6312 ⟶wf 6351 ‘cfv 6355 (class class class)co 7156 Fincfn 8509 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 -cneg 10871 / cdiv 11297 ℕcn 11638 2c2 11693 ℕ₀cn0 11898 ℤcz 11982 ..^cfzo 13034 ↑cexp 13430 ♯chash 13691 Word cword 13862 ∥ cdvds 15607 Basecbs 16483 ↾_s cress 16484 +_gcplusg 16565 ._rcmulr 16566 0_gc0g 16713 Grpcgrp 18103 ._gcmg 18224 GrpHom cghm 18355 odcod 18652 DProd cdprd 19115 dProjcdpj 19116 mulGrpcmgp 19239 1_rcur 19251 Ringcrg 19297 CRingccrg 19298 Unitcui 19389 ℤ/nℤczn 20650 ↑_𝑐ccxp 25139 DChrcdchr 25808

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-inf2 9104 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615 ax-addf 10616 ax-mulf 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-om 7581 df-1st 7689 df-2nd 7690 df-supp 7831 df-tpos 7892 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-2o 8103 df-oadd 8106 df-omul 8107 df-er 8289 df-ec 8291 df-qs 8295 df-map 8408 df-pm 8409 df-ixp 8462 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fsupp 8834 df-fi 8875 df-sup 8906 df-inf 8907 df-oi 8974 df-card 9368 df-acn 9371 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-z 11983 df-dec 12100 df-uz 12245 df-q 12350 df-rp 12391 df-xneg 12508 df-xadd 12509 df-xmul 12510 df-ioo 12743 df-ioc 12744 df-ico 12745 df-icc 12746 df-fz 12894 df-fzo 13035 df-fl 13163 df-mod 13239 df-seq 13371 df-exp 13431 df-fac 13635 df-bc 13664 df-hash 13692 df-word 13863 df-shft 14426 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-limsup 14828 df-clim 14845 df-rlim 14846 df-sum 15043 df-ef 15421 df-sin 15423 df-cos 15424 df-pi 15426 df-dvds 15608 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-plusg 16578 df-mulr 16579 df-starv 16580 df-sca 16581 df-vsca 16582 df-ip 16583 df-tset 16584 df-ple 16585 df-ds 16587 df-unif 16588 df-hom 16589 df-cco 16590 df-rest 16696 df-topn 16697 df-0g 16715 df-gsum 16716 df-topgen 16717 df-pt 16718 df-prds 16721 df-xrs 16775 df-qtop 16780 df-imas 16781 df-qus 16782 df-xps 16783 df-mre 16857 df-mrc 16858 df-acs 16860 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-mhm 17956 df-submnd 17957 df-grp 18106 df-minusg 18107 df-sbg 18108 df-mulg 18225 df-subg 18276 df-nsg 18277 df-eqg 18278 df-ghm 18356 df-gim 18399 df-cntz 18447 df-oppg 18474 df-od 18656 df-lsm 18761 df-pj1 18762 df-cmn 18908 df-abl 18909 df-dprd 19117 df-dpj 19118 df-mgp 19240 df-ur 19252 df-ring 19299 df-cring 19300 df-oppr 19373 df-dvdsr 19391 df-unit 19392 df-rnghom 19467 df-subrg 19533 df-lmod 19636 df-lss 19704 df-lsp 19744 df-sra 19944 df-rgmod 19945 df-lidl 19946 df-rsp 19947 df-2idl 20005 df-psmet 20537 df-xmet 20538 df-met 20539 df-bl 20540 df-mopn 20541 df-fbas 20542 df-fg 20543 df-cnfld 20546 df-zring 20618 df-zrh 20651 df-zn 20654 df-top 21502 df-topon 21519 df-topsp 21541 df-bases 21554 df-cld 21627 df-ntr 21628 df-cls 21629 df-nei 21706 df-lp 21744 df-perf 21745 df-cn 21835 df-cnp 21836 df-haus 21923 df-tx 22170 df-hmeo 22363 df-fil 22454 df-fm 22546 df-flim 22547 df-flf 22548 df-xms 22930 df-ms 22931 df-tms 22932 df-cncf 23486 df-limc 24464 df-dv 24465 df-log 25140 df-cxp 25141 df-dchr 25809

This theorem is referenced by: dchrptlem3 25842

W3C validator