Metamath Proof Explorer

Theorem dchrptlem2

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

Ref Expression
Hypotheses dchrpt.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrpt.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrpt.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrpt.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
dchrpt.1 ⊢ 1 = ( 1r ‘ 𝑍 )
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 dchrptlem2 ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )

Proof

Step Hyp Ref Expression
1 dchrpt.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrpt.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrpt.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchrpt.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
5 dchrpt.1 ⊢ 1 = ( 1r ‘ 𝑍 )
6 dchrpt.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 dchrpt.n1 ⊢ ( 𝜑 → 𝐴 ≠ 1 )
8 dchrpt.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
9 dchrpt.h ⊢ 𝐻 = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
10 dchrpt.m ⊢ · = ( .g ‘ 𝐻 )
11 dchrpt.s ⊢ 𝑆 = ( 𝑘 ∈ dom 𝑊 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) )
12 dchrpt.au ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
13 dchrpt.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑈 )
14 dchrpt.2 ⊢ ( 𝜑 → 𝐻 dom DProd 𝑆 )
15 dchrpt.3 ⊢ ( 𝜑 → ( 𝐻 DProd 𝑆 ) = 𝑈 )
16 dchrpt.p ⊢ 𝑃 = ( 𝐻 dProj 𝑆 )
17 dchrpt.o ⊢ 𝑂 = ( od ‘ 𝐻 )
18 dchrpt.t ⊢ 𝑇 = ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) )
19 dchrpt.i ⊢ ( 𝜑 → 𝐼 ∈ dom 𝑊 )
20 dchrpt.4 ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) ≠ 1 )
21 dchrpt.5 ⊢ 𝑋 = ( 𝑢 ∈ 𝑈 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) )
22 fveq2 ⊢ ( 𝑣 = 𝑥 → ( 𝑋 ‘ 𝑣 ) = ( 𝑋 ‘ 𝑥 ) )
23 fveq2 ⊢ ( 𝑣 = 𝑦 → ( 𝑋 ‘ 𝑣 ) = ( 𝑋 ‘ 𝑦 ) )
24 fveq2 ⊢ ( 𝑣 = ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) → ( 𝑋 ‘ 𝑣 ) = ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) )
25 fveq2 ⊢ ( 𝑣 = ( 1r ‘ 𝑍 ) → ( 𝑋 ‘ 𝑣 ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
26 zex ⊢ ℤ ∈ V
27 26 mptex ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) ∈ V
28 27 rnex ⊢ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) ∈ V
29 28 11 dmmpti ⊢ dom 𝑆 = dom 𝑊
30 29 a1i ⊢ ( 𝜑 → dom 𝑆 = dom 𝑊 )
31 14 30 16 19 dpjf ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) : ( 𝐻 DProd 𝑆 ) ⟶ ( 𝑆 ‘ 𝐼 ) )
32 15 feq2d ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝐼 ) : ( 𝐻 DProd 𝑆 ) ⟶ ( 𝑆 ‘ 𝐼 ) ↔ ( 𝑃 ‘ 𝐼 ) : 𝑈 ⟶ ( 𝑆 ‘ 𝐼 ) ) )
33 31 32 mpbid ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) : 𝑈 ⟶ ( 𝑆 ‘ 𝐼 ) )
34 33 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) ∈ ( 𝑆 ‘ 𝐼 ) )
35 19 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) → 𝐼 ∈ dom 𝑊 )
36 oveq1 ⊢ ( 𝑛 = 𝑎 → ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) = ( 𝑎 · ( 𝑊 ‘ 𝑘 ) ) )
37 36 cbvmptv ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) = ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝑘 ) ) )
38 fveq2 ⊢ ( 𝑘 = 𝐼 → ( 𝑊 ‘ 𝑘 ) = ( 𝑊 ‘ 𝐼 ) )
39 38 oveq2d ⊢ ( 𝑘 = 𝐼 → ( 𝑎 · ( 𝑊 ‘ 𝑘 ) ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) )
40 39 mpteq2dv ⊢ ( 𝑘 = 𝐼 → ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝑘 ) ) ) = ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
41 37 40 syl5eq ⊢ ( 𝑘 = 𝐼 → ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) = ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
42 41 rneqd ⊢ ( 𝑘 = 𝐼 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) = ran ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
43 42 11 28 fvmpt3i ⊢ ( 𝐼 ∈ dom 𝑊 → ( 𝑆 ‘ 𝐼 ) = ran ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
44 35 43 syl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) → ( 𝑆 ‘ 𝐼 ) = ran ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
45 34 44 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) ∈ ran ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
46 eqid ⊢ ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) = ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) )
47 ovex ⊢ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∈ V
48 46 47 elrnmpti ⊢ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) ∈ ran ( 𝑎 ∈ ℤ ↦ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ↔ ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) )
49 45 48 sylib ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) )
50 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ 𝑣 ) = ( 𝑇 ↑ 𝑎 ) )
51 neg1cn ⊢ - 1 ∈ ℂ
52 2re ⊢ 2 ∈ ℝ
53 6 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
54 2 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
55 crngring ⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
56 53 54 55 3syl ⊢ ( 𝜑 → 𝑍 ∈ Ring )
57 8 9 unitgrp ⊢ ( 𝑍 ∈ Ring → 𝐻 ∈ Grp )
58 56 57 syl ⊢ ( 𝜑 → 𝐻 ∈ Grp )
59 2 4 znfi ⊢ ( 𝑁 ∈ ℕ → 𝐵 ∈ Fin )
60 6 59 syl ⊢ ( 𝜑 → 𝐵 ∈ Fin )
61 4 8 unitss ⊢ 𝑈 ⊆ 𝐵
62 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵 ) → 𝑈 ∈ Fin )
63 60 61 62 sylancl ⊢ ( 𝜑 → 𝑈 ∈ Fin )
64 wrdf ⊢ ( 𝑊 ∈ Word 𝑈 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑈 )
65 13 64 syl ⊢ ( 𝜑 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑈 )
66 65 fdmd ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
67 19 66 eleqtrd ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
68 65 67 ffvelrnd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 )
69 8 9 unitgrpbas ⊢ 𝑈 = ( Base ‘ 𝐻 )
70 69 17 odcl2 ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 ) → ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∈ ℕ )
71 58 63 68 70 syl3anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∈ ℕ )
72 nndivre ⊢ ( ( 2 ∈ ℝ ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∈ ℕ ) → ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ∈ ℝ )
73 52 71 72 sylancr ⊢ ( 𝜑 → ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ∈ ℝ )
74 73 recnd ⊢ ( 𝜑 → ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ∈ ℂ )
75 cxpcl ⊢ ( ( - 1 ∈ ℂ ∧ ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ∈ ℂ ) → ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ∈ ℂ )
76 51 74 75 sylancr ⊢ ( 𝜑 → ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ∈ ℂ )
77 18 76 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
78 77 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → 𝑇 ∈ ℂ )
79 51 a1i ⊢ ( 𝜑 → - 1 ∈ ℂ )
80 neg1ne0 ⊢ - 1 ≠ 0
81 80 a1i ⊢ ( 𝜑 → - 1 ≠ 0 )
82 79 81 74 cxpne0d ⊢ ( 𝜑 → ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ≠ 0 )
83 18 neeq1i ⊢ ( 𝑇 ≠ 0 ↔ ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ≠ 0 )
84 82 83 sylibr ⊢ ( 𝜑 → 𝑇 ≠ 0 )
85 84 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → 𝑇 ≠ 0 )
86 simprl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → 𝑎 ∈ ℤ )
87 78 85 86 expclzd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑇 ↑ 𝑎 ) ∈ ℂ )
88 50 87 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ 𝑣 ) ∈ ℂ )
89 49 88 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑣 ) ∈ ℂ )
90 fveqeq2 ⊢ ( 𝑣 = 𝑥 → ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ↔ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
91 90 rexbidv ⊢ ( 𝑣 = 𝑥 → ( ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ↔ ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
92 49 ralrimiva ⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) )
93 92 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) )
94 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝑈 )
95 91 93 94 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) )
96 fveqeq2 ⊢ ( 𝑣 = 𝑦 → ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ↔ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
97 96 rexbidv ⊢ ( 𝑣 = 𝑦 → ( ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ↔ ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
98 oveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) )
99 98 eqeq2d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ↔ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) )
100 99 cbvrexvw ⊢ ( ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ↔ ∃ 𝑏 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) )
101 97 100 bitrdi ⊢ ( 𝑣 = 𝑦 → ( ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ↔ ∃ 𝑏 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) )
102 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
103 101 93 102 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ∃ 𝑏 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) )
104 reeanv ⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ↔ ( ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ∃ 𝑏 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) )
105 77 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → 𝑇 ∈ ℂ )
106 84 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → 𝑇 ≠ 0 )
107 simprll ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → 𝑎 ∈ ℤ )
108 simprlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → 𝑏 ∈ ℤ )
109 expaddz ⊢ ( ( ( 𝑇 ∈ ℂ ∧ 𝑇 ≠ 0 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑇 ↑ ( 𝑎 + 𝑏 ) ) = ( ( 𝑇 ↑ 𝑎 ) · ( 𝑇 ↑ 𝑏 ) ) )
110 105 106 107 108 109 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( 𝑇 ↑ ( 𝑎 + 𝑏 ) ) = ( ( 𝑇 ↑ 𝑎 ) · ( 𝑇 ↑ 𝑏 ) ) )
111 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → 𝜑 )
112 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → 𝑍 ∈ Ring )
113 94 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → 𝑥 ∈ 𝑈 )
114 102 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → 𝑦 ∈ 𝑈 )
115 eqid ⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 )
116 8 115 unitmulcl ⊢ ( ( 𝑍 ∈ Ring ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 )
117 112 113 114 116 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 )
118 107 108 zaddcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
119 simprrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) )
120 simprrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) )
121 119 120 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) ( .r ‘ 𝑍 ) ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) ) = ( ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ( .r ‘ 𝑍 ) ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) )
122 14 30 16 19 dpjghm ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) ∈ ( ( 𝐻 ↾s ( 𝐻 DProd 𝑆 ) ) GrpHom 𝐻 ) )
123 15 oveq2d ⊢ ( 𝜑 → ( 𝐻 ↾s ( 𝐻 DProd 𝑆 ) ) = ( 𝐻 ↾s 𝑈 ) )
124 9 ovexi ⊢ 𝐻 ∈ V
125 69 ressid ⊢ ( 𝐻 ∈ V → ( 𝐻 ↾s 𝑈 ) = 𝐻 )
126 124 125 ax-mp ⊢ ( 𝐻 ↾s 𝑈 ) = 𝐻
127 123 126 eqtrdi ⊢ ( 𝜑 → ( 𝐻 ↾s ( 𝐻 DProd 𝑆 ) ) = 𝐻 )
128 127 oveq1d ⊢ ( 𝜑 → ( ( 𝐻 ↾s ( 𝐻 DProd 𝑆 ) ) GrpHom 𝐻 ) = ( 𝐻 GrpHom 𝐻 ) )
129 122 128 eleqtrd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) ∈ ( 𝐻 GrpHom 𝐻 ) )
130 129 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( 𝑃 ‘ 𝐼 ) ∈ ( 𝐻 GrpHom 𝐻 ) )
131 8 fvexi ⊢ 𝑈 ∈ V
132 eqid ⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
133 132 115 mgpplusg ⊢ ( .r ‘ 𝑍 ) = ( +g ‘ ( mulGrp ‘ 𝑍 ) )
134 9 133 ressplusg ⊢ ( 𝑈 ∈ V → ( .r ‘ 𝑍 ) = ( +g ‘ 𝐻 ) )
135 131 134 ax-mp ⊢ ( .r ‘ 𝑍 ) = ( +g ‘ 𝐻 )
136 69 135 135 ghmlin ⊢ ( ( ( 𝑃 ‘ 𝐼 ) ∈ ( 𝐻 GrpHom 𝐻 ) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → ( ( 𝑃 ‘ 𝐼 ) ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) ( .r ‘ 𝑍 ) ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) ) )
137 130 113 114 136 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( ( 𝑃 ‘ 𝐼 ) ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) ( .r ‘ 𝑍 ) ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) ) )
138 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → 𝐻 ∈ Grp )
139 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 )
140 69 10 135 mulgdir ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 ) ) → ( ( 𝑎 + 𝑏 ) · ( 𝑊 ‘ 𝐼 ) ) = ( ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ( .r ‘ 𝑍 ) ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) )
141 138 107 108 139 140 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( ( 𝑎 + 𝑏 ) · ( 𝑊 ‘ 𝐼 ) ) = ( ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ( .r ‘ 𝑍 ) ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) )
142 121 137 141 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( ( 𝑃 ‘ 𝐼 ) ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑎 + 𝑏 ) · ( 𝑊 ‘ 𝐼 ) ) )
143 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ∈ 𝑈 ) ∧ ( ( 𝑎 + 𝑏 ) ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑎 + 𝑏 ) · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( 𝑇 ↑ ( 𝑎 + 𝑏 ) ) )
144 111 117 118 142 143 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( 𝑇 ↑ ( 𝑎 + 𝑏 ) ) )
145 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ 𝑥 ) = ( 𝑇 ↑ 𝑎 ) )
146 111 113 107 119 145 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( 𝑋 ‘ 𝑥 ) = ( 𝑇 ↑ 𝑎 ) )
147 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) ∧ ( 𝑏 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ 𝑦 ) = ( 𝑇 ↑ 𝑏 ) )
148 111 114 108 120 147 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( 𝑋 ‘ 𝑦 ) = ( 𝑇 ↑ 𝑏 ) )
149 146 148 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) = ( ( 𝑇 ↑ 𝑎 ) · ( 𝑇 ↑ 𝑏 ) ) )
150 110 144 149 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
151 150 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
152 151 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
153 104 152 syl5bir ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( ( ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑥 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ∧ ∃ 𝑏 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑦 ) = ( 𝑏 · ( 𝑊 ‘ 𝐼 ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
154 95 103 153 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
155 id ⊢ ( 𝜑 → 𝜑 )
156 eqid ⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
157 8 156 1unit ⊢ ( 𝑍 ∈ Ring → ( 1r ‘ 𝑍 ) ∈ 𝑈 )
158 56 157 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑍 ) ∈ 𝑈 )
159 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
160 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
161 160 160 ghmid ⊢ ( ( 𝑃 ‘ 𝐼 ) ∈ ( 𝐻 GrpHom 𝐻 ) → ( ( 𝑃 ‘ 𝐼 ) ‘ ( 0g ‘ 𝐻 ) ) = ( 0g ‘ 𝐻 ) )
162 129 161 syl ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝐼 ) ‘ ( 0g ‘ 𝐻 ) ) = ( 0g ‘ 𝐻 ) )
163 8 9 156 unitgrpid ⊢ ( 𝑍 ∈ Ring → ( 1r ‘ 𝑍 ) = ( 0g ‘ 𝐻 ) )
164 56 163 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑍 ) = ( 0g ‘ 𝐻 ) )
165 164 fveq2d ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝐼 ) ‘ ( 1r ‘ 𝑍 ) ) = ( ( 𝑃 ‘ 𝐼 ) ‘ ( 0g ‘ 𝐻 ) ) )
166 69 160 10 mulg0 ⊢ ( ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 → ( 0 · ( 𝑊 ‘ 𝐼 ) ) = ( 0g ‘ 𝐻 ) )
167 68 166 syl ⊢ ( 𝜑 → ( 0 · ( 𝑊 ‘ 𝐼 ) ) = ( 0g ‘ 𝐻 ) )
168 162 165 167 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝐼 ) ‘ ( 1r ‘ 𝑍 ) ) = ( 0 · ( 𝑊 ‘ 𝐼 ) ) )
169 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 ⊢ ( ( ( 𝜑 ∧ ( 1r ‘ 𝑍 ) ∈ 𝑈 ) ∧ ( 0 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ ( 1r ‘ 𝑍 ) ) = ( 0 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = ( 𝑇 ↑ 0 ) )
170 155 158 159 168 169 syl22anc ⊢ ( 𝜑 → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = ( 𝑇 ↑ 0 ) )
171 77 exp0d ⊢ ( 𝜑 → ( 𝑇 ↑ 0 ) = 1 )
172 170 171 eqtrd ⊢ ( 𝜑 → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
173 1 2 4 8 6 3 22 23 24 25 89 154 172 dchrelbasd ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) ∈ 𝐷 )
174 61 12 sselid ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
175 eleq1 ⊢ ( 𝑣 = 𝐴 → ( 𝑣 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈 ) )
176 fveq2 ⊢ ( 𝑣 = 𝐴 → ( 𝑋 ‘ 𝑣 ) = ( 𝑋 ‘ 𝐴 ) )
177 175 176 ifbieq1d ⊢ ( 𝑣 = 𝐴 → if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) = if ( 𝐴 ∈ 𝑈 , ( 𝑋 ‘ 𝐴 ) , 0 ) )
178 eqid ⊢ ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) = ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) )
179 fvex ⊢ ( 𝑋 ‘ 𝑣 ) ∈ V
180 c0ex ⊢ 0 ∈ V
181 179 180 ifex ⊢ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ∈ V
182 177 178 181 fvmpt3i ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) ‘ 𝐴 ) = if ( 𝐴 ∈ 𝑈 , ( 𝑋 ‘ 𝐴 ) , 0 ) )
183 174 182 syl ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) ‘ 𝐴 ) = if ( 𝐴 ∈ 𝑈 , ( 𝑋 ‘ 𝐴 ) , 0 ) )
184 12 iftrued ⊢ ( 𝜑 → if ( 𝐴 ∈ 𝑈 , ( 𝑋 ‘ 𝐴 ) , 0 ) = ( 𝑋 ‘ 𝐴 ) )
185 183 184 eqtrd ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) ‘ 𝐴 ) = ( 𝑋 ‘ 𝐴 ) )
186 fveqeq2 ⊢ ( 𝑣 = 𝐴 → ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ↔ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
187 186 rexbidv ⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑣 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ↔ ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) )
188 187 92 12 rspcdva ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) )
189 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ 𝐴 ) = ( 𝑇 ↑ 𝑎 ) )
190 18 oveq1i ⊢ ( 𝑇 ↑ 𝑎 ) = ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ 𝑎 )
191 189 190 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ 𝐴 ) = ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ 𝑎 ) )
192 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) ≠ 1 )
193 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → 𝐻 ∈ Grp )
194 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 )
195 simprl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → 𝑎 ∈ ℤ )
196 69 17 10 160 oddvds ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 ∧ 𝑎 ∈ ℤ ) → ( ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ 𝑎 ↔ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) = ( 0g ‘ 𝐻 ) ) )
197 193 194 195 196 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ 𝑎 ↔ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) = ( 0g ‘ 𝐻 ) ) )
198 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∈ ℕ )
199 root1eq1 ⊢ ( ( ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∈ ℕ ∧ 𝑎 ∈ ℤ ) → ( ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ 𝑎 ) = 1 ↔ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ 𝑎 ) )
200 198 195 199 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ 𝑎 ) = 1 ↔ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ 𝑎 ) )
201 simprr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) )
202 5 164 syl5eq ⊢ ( 𝜑 → 1 = ( 0g ‘ 𝐻 ) )
203 202 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → 1 = ( 0g ‘ 𝐻 ) )
204 201 203 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = 1 ↔ ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) = ( 0g ‘ 𝐻 ) ) )
205 197 200 204 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ 𝑎 ) = 1 ↔ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = 1 ) )
206 205 necon3bid ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ 𝑎 ) ≠ 1 ↔ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) ≠ 1 ) )
207 192 206 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ 𝑎 ) ≠ 1 )
208 191 207 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ 𝐴 ) ≠ 1 )
209 208 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) → ( 𝑋 ‘ 𝐴 ) ≠ 1 ) )
210 12 209 mpdan ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℤ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) = ( 𝑎 · ( 𝑊 ‘ 𝐼 ) ) → ( 𝑋 ‘ 𝐴 ) ≠ 1 ) )
211 188 210 mpd ⊢ ( 𝜑 → ( 𝑋 ‘ 𝐴 ) ≠ 1 )
212 185 211 eqnetrd ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) ‘ 𝐴 ) ≠ 1 )
213 fveq1 ⊢ ( 𝑥 = ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) → ( 𝑥 ‘ 𝐴 ) = ( ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) ‘ 𝐴 ) )
214 213 neeq1d ⊢ ( 𝑥 = ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) → ( ( 𝑥 ‘ 𝐴 ) ≠ 1 ↔ ( ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) ‘ 𝐴 ) ≠ 1 ) )
215 214 rspcev ⊢ ( ( ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) ∈ 𝐷 ∧ ( ( 𝑣 ∈ 𝐵 ↦ if ( 𝑣 ∈ 𝑈 , ( 𝑋 ‘ 𝑣 ) , 0 ) ) ‘ 𝐴 ) ≠ 1 ) → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )
216 173 212 215 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )