Metamath Proof Explorer

Theorem dfufd2lem

Description: Lemma for dfufd2 . (Contributed by Thierry Arnoux, 6-Jun-2025)

Ref Expression
Hypotheses dfufd2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
dfufd2.0 ⊢ 0 = ( 0g ‘ 𝑅 )
dfufd2.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dfufd2.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
dfufd2.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
dfufd2lem.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
dfufd2lem.2 ⊢ ( 𝜑 → 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) )
dfufd2lem.3 ⊢ ( 𝜑 → 𝐹 ∈ Word 𝑃 )
dfufd2lem.4 ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ∈ 𝐼 )
dfufd2lem.5 ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ≠ 0 )
Assertion dfufd2lem ( 𝜑 → ( 𝐼 ∩ 𝑃 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 dfufd2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dfufd2.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 dfufd2.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
4 dfufd2.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
5 dfufd2.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
6 dfufd2lem.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
7 dfufd2lem.2 ⊢ ( 𝜑 → 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) )
8 dfufd2lem.3 ⊢ ( 𝜑 → 𝐹 ∈ Word 𝑃 )
9 dfufd2lem.4 ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ∈ 𝐼 )
10 dfufd2lem.5 ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) ≠ 0 )
11 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) → ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 )
12 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝐹 ) )
13 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) → 𝐹 ∈ Word 𝑃 )
14 12 13 wrdfd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑃 )
15 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
16 14 15 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) → ( 𝐹 ‘ 𝑖 ) ∈ 𝑃 )
17 inelcm ⊢ ( ( ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝑃 ) → ( 𝐼 ∩ 𝑃 ) ≠ ∅ )
18 11 16 17 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) → ( 𝐼 ∩ 𝑃 ) ≠ ∅ )
19 id ⊢ ( 𝜑 → 𝜑 )
20 oveq2 ⊢ ( 𝑔 = ∅ → ( 𝑀 Σg 𝑔 ) = ( 𝑀 Σg ∅ ) )
21 20 eleq1d ⊢ ( 𝑔 = ∅ → ( ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ↔ ( 𝑀 Σg ∅ ) ∈ 𝐼 ) )
22 20 neeq1d ⊢ ( 𝑔 = ∅ → ( ( 𝑀 Σg 𝑔 ) ≠ 0 ↔ ( 𝑀 Σg ∅ ) ≠ 0 ) )
23 21 22 3anbi23d ⊢ ( 𝑔 = ∅ → ( ( 𝜑 ∧ ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑔 ) ≠ 0 ) ↔ ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) ) )
24 fveq2 ⊢ ( 𝑔 = ∅ → ( ♯ ‘ 𝑔 ) = ( ♯ ‘ ∅ ) )
25 24 oveq2d ⊢ ( 𝑔 = ∅ → ( 0 ..^ ( ♯ ‘ 𝑔 ) ) = ( 0 ..^ ( ♯ ‘ ∅ ) ) )
26 fveq1 ⊢ ( 𝑔 = ∅ → ( 𝑔 ‘ 𝑖 ) = ( ∅ ‘ 𝑖 ) )
27 26 eleq1d ⊢ ( 𝑔 = ∅ → ( ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ↔ ( ∅ ‘ 𝑖 ) ∈ 𝐼 ) )
28 25 27 rexeqbidv ⊢ ( 𝑔 = ∅ → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ∅ ‘ 𝑖 ) ∈ 𝐼 ) )
29 23 28 imbi12d ⊢ ( 𝑔 = ∅ → ( ( ( 𝜑 ∧ ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑔 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ) ↔ ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ∅ ‘ 𝑖 ) ∈ 𝐼 ) ) )
30 oveq2 ⊢ ( 𝑔 = 𝑓 → ( 𝑀 Σg 𝑔 ) = ( 𝑀 Σg 𝑓 ) )
31 30 eleq1d ⊢ ( 𝑔 = 𝑓 → ( ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ↔ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) )
32 30 neeq1d ⊢ ( 𝑔 = 𝑓 → ( ( 𝑀 Σg 𝑔 ) ≠ 0 ↔ ( 𝑀 Σg 𝑓 ) ≠ 0 ) )
33 31 32 3anbi23d ⊢ ( 𝑔 = 𝑓 → ( ( 𝜑 ∧ ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑔 ) ≠ 0 ) ↔ ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) ) )
34 fveq2 ⊢ ( 𝑔 = 𝑓 → ( ♯ ‘ 𝑔 ) = ( ♯ ‘ 𝑓 ) )
35 34 oveq2d ⊢ ( 𝑔 = 𝑓 → ( 0 ..^ ( ♯ ‘ 𝑔 ) ) = ( 0 ..^ ( ♯ ‘ 𝑓 ) ) )
36 fveq1 ⊢ ( 𝑔 = 𝑓 → ( 𝑔 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
37 36 eleq1d ⊢ ( 𝑔 = 𝑓 → ( ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ↔ ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) )
38 35 37 rexeqbidv ⊢ ( 𝑔 = 𝑓 → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) )
39 33 38 imbi12d ⊢ ( 𝑔 = 𝑓 → ( ( ( 𝜑 ∧ ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑔 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ) ↔ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) )
40 oveq2 ⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) → ( 𝑀 Σg 𝑔 ) = ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) )
41 40 eleq1d ⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) → ( ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ↔ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) )
42 40 neeq1d ⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) → ( ( 𝑀 Σg 𝑔 ) ≠ 0 ↔ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) )
43 41 42 3anbi23d ⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) → ( ( 𝜑 ∧ ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑔 ) ≠ 0 ) ↔ ( 𝜑 ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ) )
44 fveq2 ⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) → ( ♯ ‘ 𝑔 ) = ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) )
45 44 oveq2d ⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) → ( 0 ..^ ( ♯ ‘ 𝑔 ) ) = ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) )
46 fveq1 ⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) → ( 𝑔 ‘ 𝑖 ) = ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) )
47 46 eleq1d ⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) → ( ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ↔ ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) )
48 45 47 rexeqbidv ⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) )
49 43 48 imbi12d ⊢ ( 𝑔 = ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) → ( ( ( 𝜑 ∧ ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑔 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ) ↔ ( ( 𝜑 ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) ) )
50 oveq2 ⊢ ( 𝑔 = 𝐹 → ( 𝑀 Σg 𝑔 ) = ( 𝑀 Σg 𝐹 ) )
51 50 eleq1d ⊢ ( 𝑔 = 𝐹 → ( ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ↔ ( 𝑀 Σg 𝐹 ) ∈ 𝐼 ) )
52 50 neeq1d ⊢ ( 𝑔 = 𝐹 → ( ( 𝑀 Σg 𝑔 ) ≠ 0 ↔ ( 𝑀 Σg 𝐹 ) ≠ 0 ) )
53 51 52 3anbi23d ⊢ ( 𝑔 = 𝐹 → ( ( 𝜑 ∧ ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑔 ) ≠ 0 ) ↔ ( 𝜑 ∧ ( 𝑀 Σg 𝐹 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝐹 ) ≠ 0 ) ) )
54 fveq2 ⊢ ( 𝑔 = 𝐹 → ( ♯ ‘ 𝑔 ) = ( ♯ ‘ 𝐹 ) )
55 54 oveq2d ⊢ ( 𝑔 = 𝐹 → ( 0 ..^ ( ♯ ‘ 𝑔 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
56 fveq1 ⊢ ( 𝑔 = 𝐹 → ( 𝑔 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) )
57 56 eleq1d ⊢ ( 𝑔 = 𝐹 → ( ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ↔ ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) )
58 55 57 rexeqbidv ⊢ ( 𝑔 = 𝐹 → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) )
59 53 58 imbi12d ⊢ ( 𝑔 = 𝐹 → ( ( ( 𝜑 ∧ ( 𝑀 Σg 𝑔 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑔 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( 𝑔 ‘ 𝑖 ) ∈ 𝐼 ) ↔ ( ( 𝜑 ∧ ( 𝑀 Σg 𝐹 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝐹 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) ) )
60 6 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
61 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
62 3 61 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
63 60 62 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
64 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
65 5 61 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
66 65 gsum0 ⊢ ( 𝑀 Σg ∅ ) = ( 1r ‘ 𝑅 )
67 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → ( 𝑀 Σg ∅ ) ∈ 𝐼 )
68 66 67 eqeltrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → ( 1r ‘ 𝑅 ) ∈ 𝐼 )
69 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → 𝑅 ∈ Ring )
70 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) )
71 prmidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
72 69 70 71 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
73 1 3 64 68 69 72 lidlunitel ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → 𝐼 = 𝐵 )
74 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
75 1 74 prmidlnr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝐼 ≠ 𝐵 )
76 69 70 75 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → 𝐼 ≠ 𝐵 )
77 73 76 pm2.21ddne ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ∅ ‘ 𝑖 ) ∈ 𝐼 )
78 77 3impa ⊢ ( ( 𝜑 ∧ ( 𝑀 Σg ∅ ) ∈ 𝐼 ∧ ( 𝑀 Σg ∅ ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ∅ ‘ 𝑖 ) ∈ 𝐼 )
79 simpllr ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → 𝜑 )
80 simp-4r ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( 𝑀 Σg 𝑓 ) ∈ 𝐼 )
81 6 idomdomd ⊢ ( 𝜑 → 𝑅 ∈ Domn )
82 81 ad3antlr ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → 𝑅 ∈ Domn )
83 6 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑅 ∈ IDomn )
84 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 )
85 1 4 83 84 rprmcl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝐵 )
86 4 2 83 84 rprmnz ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ≠ 0 )
87 85 86 eldifsnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ ( 𝐵 ∖ { 0 } ) )
88 87 ex ⊢ ( 𝜑 → ( 𝑝 ∈ 𝑃 → 𝑝 ∈ ( 𝐵 ∖ { 0 } ) ) )
89 88 ssrdv ⊢ ( 𝜑 → 𝑃 ⊆ ( 𝐵 ∖ { 0 } ) )
90 sswrd ⊢ ( 𝑃 ⊆ ( 𝐵 ∖ { 0 } ) → Word 𝑃 ⊆ Word ( 𝐵 ∖ { 0 } ) )
91 89 90 syl ⊢ ( 𝜑 → Word 𝑃 ⊆ Word ( 𝐵 ∖ { 0 } ) )
92 91 ad3antlr ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → Word 𝑃 ⊆ Word ( 𝐵 ∖ { 0 } ) )
93 simpll ⊢ ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝜑 ) → 𝑓 ∈ Word 𝑃 )
94 93 ad5ant13 ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → 𝑓 ∈ Word 𝑃 )
95 92 94 sseldd ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → 𝑓 ∈ Word ( 𝐵 ∖ { 0 } ) )
96 1 5 2 82 95 domnprodn0 ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( 𝑀 Σg 𝑓 ) ≠ 0 )
97 79 80 96 3jca ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) )
98 lencl ⊢ ( 𝑓 ∈ Word 𝑃 → ( ♯ ‘ 𝑓 ) ∈ ℕ0 )
99 fzossfzop1 ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) + 1 ) ) )
100 94 98 99 3syl ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) + 1 ) ) )
101 ccatws1len ⊢ ( 𝑓 ∈ Word 𝑃 → ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) = ( ( ♯ ‘ 𝑓 ) + 1 ) )
102 94 101 syl ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) = ( ( ♯ ‘ 𝑓 ) + 1 ) )
103 102 oveq2d ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑓 ) + 1 ) ) )
104 100 103 sseqtrrd ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ⊆ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) )
105 94 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) → 𝑓 ∈ Word 𝑃 )
106 simplr ⊢ ( ( ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) )
107 ccats1val1 ⊢ ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ) → ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
108 105 106 107 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) → ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
109 simpr ⊢ ( ( ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) → ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 )
110 108 109 eqeltrd ⊢ ( ( ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) → ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 )
111 110 ex ⊢ ( ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ) → ( ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 → ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) )
112 111 reximdva ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) )
113 ssrexv ⊢ ( ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ⊆ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) )
114 104 112 113 sylsyld ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) )
115 97 114 embantd ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) )
116 115 imp ⊢ ( ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 )
117 116 an62ds ⊢ ( ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 )
118 fveq2 ⊢ ( 𝑖 = ( ♯ ‘ 𝑓 ) → ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ ( ♯ ‘ 𝑓 ) ) )
119 118 eleq1d ⊢ ( 𝑖 = ( ♯ ‘ 𝑓 ) → ( ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ↔ ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ ( ♯ ‘ 𝑓 ) ) ∈ 𝐼 ) )
120 98 ad5antr ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ♯ ‘ 𝑓 ) ∈ ℕ0 )
121 fzonn0p1 ⊢ ( ( ♯ ‘ 𝑓 ) ∈ ℕ0 → ( ♯ ‘ 𝑓 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) + 1 ) ) )
122 120 121 syl ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ♯ ‘ 𝑓 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑓 ) + 1 ) ) )
123 101 ad5antr ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) = ( ( ♯ ‘ 𝑓 ) + 1 ) )
124 123 oveq2d ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑓 ) + 1 ) ) )
125 122 124 eleqtrrd ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ♯ ‘ 𝑓 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) )
126 ccatws1ls ⊢ ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ ( ♯ ‘ 𝑓 ) ) = 𝑝 )
127 126 ad4antr ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ ( ♯ ‘ 𝑓 ) ) = 𝑝 )
128 simp-4r ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → 𝑝 ∈ 𝐼 )
129 127 128 eqeltrd ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ ( ♯ ‘ 𝑓 ) ) ∈ 𝐼 )
130 119 125 129 rspcedvdw ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 )
131 130 adantr ⊢ ( ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐼 ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 )
132 131 an62ds ⊢ ( ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) ∧ 𝑝 ∈ 𝐼 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 )
133 6 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
134 133 ad3antlr ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → 𝑅 ∈ CRing )
135 7 ad3antlr ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) )
136 5 1 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑀 )
137 5 crngmgp ⊢ ( 𝑅 ∈ CRing → 𝑀 ∈ CMnd )
138 133 137 syl ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
139 138 adantl ⊢ ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) → 𝑀 ∈ CMnd )
140 ovexd ⊢ ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ∈ V )
141 eqidd ⊢ ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝑓 ) )
142 simplll ⊢ ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) → 𝑓 ∈ Word 𝑃 )
143 141 142 wrdfd ⊢ ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) → 𝑓 : ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ⟶ 𝑃 )
144 85 ex ⊢ ( 𝜑 → ( 𝑝 ∈ 𝑃 → 𝑝 ∈ 𝐵 ) )
145 144 ssrdv ⊢ ( 𝜑 → 𝑃 ⊆ 𝐵 )
146 145 adantl ⊢ ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) → 𝑃 ⊆ 𝐵 )
147 143 146 fssd ⊢ ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) → 𝑓 : ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ⟶ 𝐵 )
148 fvexd ⊢ ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) → ( 1r ‘ 𝑅 ) ∈ V )
149 148 142 wrdfsupp ⊢ ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) → 𝑓 finSupp ( 1r ‘ 𝑅 ) )
150 136 65 139 140 147 149 gsumcl ⊢ ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) → ( 𝑀 Σg 𝑓 ) ∈ 𝐵 )
151 150 ad2antrr ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( 𝑀 Σg 𝑓 ) ∈ 𝐵 )
152 145 adantl ⊢ ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝜑 ) → 𝑃 ⊆ 𝐵 )
153 simplr ⊢ ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝜑 ) → 𝑝 ∈ 𝑃 )
154 152 153 sseldd ⊢ ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝜑 ) → 𝑝 ∈ 𝐵 )
155 154 ad5ant13 ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → 𝑝 ∈ 𝐵 )
156 138 cmnmndd ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
157 156 adantl ⊢ ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝜑 ) → 𝑀 ∈ Mnd )
158 sswrd ⊢ ( 𝑃 ⊆ 𝐵 → Word 𝑃 ⊆ Word 𝐵 )
159 145 158 syl ⊢ ( 𝜑 → Word 𝑃 ⊆ Word 𝐵 )
160 159 adantl ⊢ ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝜑 ) → Word 𝑃 ⊆ Word 𝐵 )
161 160 93 sseldd ⊢ ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝜑 ) → 𝑓 ∈ Word 𝐵 )
162 5 74 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
163 136 162 gsumccatsn ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) = ( ( 𝑀 Σg 𝑓 ) ( .r ‘ 𝑅 ) 𝑝 ) )
164 157 161 154 163 syl3anc ⊢ ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝜑 ) → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) = ( ( 𝑀 Σg 𝑓 ) ( .r ‘ 𝑅 ) 𝑝 ) )
165 164 ad5ant13 ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) = ( ( 𝑀 Σg 𝑓 ) ( .r ‘ 𝑅 ) 𝑝 ) )
166 simplr ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 )
167 165 166 eqeltrrd ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ( 𝑀 Σg 𝑓 ) ( .r ‘ 𝑅 ) 𝑝 ) ∈ 𝐼 )
168 1 74 prmidlc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑀 Σg 𝑓 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ∧ ( ( 𝑀 Σg 𝑓 ) ( .r ‘ 𝑅 ) 𝑝 ) ∈ 𝐼 ) ) → ( ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∨ 𝑝 ∈ 𝐼 ) )
169 134 135 151 155 167 168 syl23anc ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ( ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∨ 𝑝 ∈ 𝐼 ) )
170 117 132 169 mpjaodan ⊢ ( ( ( ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) ∧ 𝜑 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ) ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 )
171 170 exp41 ⊢ ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) → ( 𝜑 → ( ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 → ( ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) ) ) )
172 171 3impd ⊢ ( ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) ) → ( ( 𝜑 ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) )
173 172 ex ⊢ ( ( 𝑓 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 𝜑 ∧ ( 𝑀 Σg 𝑓 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝑓 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝑓 ‘ 𝑖 ) ∈ 𝐼 ) → ( ( 𝜑 ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ∈ 𝐼 ∧ ( 𝑀 Σg ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ) ) ( ( 𝑓 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ∈ 𝐼 ) ) )
174 29 39 49 59 78 173 wrdind ⊢ ( 𝐹 ∈ Word 𝑃 → ( ( 𝜑 ∧ ( 𝑀 Σg 𝐹 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝐹 ) ≠ 0 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 ) )
175 174 imp ⊢ ( ( 𝐹 ∈ Word 𝑃 ∧ ( 𝜑 ∧ ( 𝑀 Σg 𝐹 ) ∈ 𝐼 ∧ ( 𝑀 Σg 𝐹 ) ≠ 0 ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 )
176 8 19 9 10 175 syl13anc ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑖 ) ∈ 𝐼 )
177 18 176 r19.29a ⊢ ( 𝜑 → ( 𝐼 ∩ 𝑃 ) ≠ ∅ )