Metamath Proof Explorer

Theorem rprmdvdsprod

Description: If a prime element Q divides a product, then it divides one term. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmdvdsprod.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rprmdvdsprod.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
rprmdvdsprod.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
rprmdvdsprod.1 ⊢ 1 = ( 1r ‘ 𝑅 )
rprmdvdsprod.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
rprmdvdsprod.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
rprmdvdsprod.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
rprmdvdsprod.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
rprmdvdsprod.2 ⊢ ( 𝜑 → 𝐹 finSupp 1 )
rprmdvdsprod.f ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
rprmdvdsprod.3 ⊢ ( 𝜑 → 𝑄 ∥ ( 𝑀 Σg 𝐹 ) )
Assertion rprmdvdsprod ( 𝜑 → ∃ 𝑥 ∈ ( 𝐹 supp 1 ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 rprmdvdsprod.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rprmdvdsprod.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3 rprmdvdsprod.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
4 rprmdvdsprod.1 ⊢ 1 = ( 1r ‘ 𝑅 )
5 rprmdvdsprod.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
6 rprmdvdsprod.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
7 rprmdvdsprod.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
8 rprmdvdsprod.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
9 rprmdvdsprod.2 ⊢ ( 𝜑 → 𝐹 finSupp 1 )
10 rprmdvdsprod.f ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
11 rprmdvdsprod.3 ⊢ ( 𝜑 → 𝑄 ∥ ( 𝑀 Σg 𝐹 ) )
12 5 1 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑀 )
13 5 4 ringidval ⊢ 1 = ( 0g ‘ 𝑀 )
14 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
15 5 14 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
16 5 crngmgp ⊢ ( 𝑅 ∈ CRing → 𝑀 ∈ CMnd )
17 6 16 syl ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
18 disjdifr ⊢ ( ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ∩ ( 𝐹 supp 1 ) ) = ∅
19 18 a1i ⊢ ( 𝜑 → ( ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ∩ ( 𝐹 supp 1 ) ) = ∅ )
20 suppssdm ⊢ ( 𝐹 supp 1 ) ⊆ dom 𝐹
21 20 10 fssdm ⊢ ( 𝜑 → ( 𝐹 supp 1 ) ⊆ 𝐼 )
22 undifr ⊢ ( ( 𝐹 supp 1 ) ⊆ 𝐼 ↔ ( ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ∪ ( 𝐹 supp 1 ) ) = 𝐼 )
23 21 22 sylib ⊢ ( 𝜑 → ( ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ∪ ( 𝐹 supp 1 ) ) = 𝐼 )
24 23 eqcomd ⊢ ( 𝜑 → 𝐼 = ( ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ∪ ( 𝐹 supp 1 ) ) )
25 12 13 15 17 8 10 9 19 24 gsumsplit ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) = ( ( 𝑀 Σg ( 𝐹 ↾ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) ) ( .r ‘ 𝑅 ) ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) ) )
26 difssd ⊢ ( 𝜑 → ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ⊆ 𝐼 )
27 10 26 feqresmpt ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) = ( 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ↦ ( 𝐹 ‘ 𝑧 ) ) )
28 10 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐼 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) → 𝐹 Fn 𝐼 )
30 8 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) → 𝐼 ∈ 𝑉 )
31 6 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
32 1 4 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
33 31 32 syl ⊢ ( 𝜑 → 1 ∈ 𝐵 )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) → 1 ∈ 𝐵 )
35 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) → 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) )
36 29 30 34 35 fvdifsupp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) → ( 𝐹 ‘ 𝑧 ) = 1 )
37 36 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ↦ ( 𝐹 ‘ 𝑧 ) ) = ( 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ↦ 1 ) )
38 27 37 eqtrd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) = ( 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ↦ 1 ) )
39 38 oveq2d ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐹 ↾ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) ) = ( 𝑀 Σg ( 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ↦ 1 ) ) )
40 17 cmnmndd ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
41 8 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ∈ V )
42 13 gsumz ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ∈ V ) → ( 𝑀 Σg ( 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ↦ 1 ) ) = 1 )
43 40 41 42 syl2anc ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑧 ∈ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ↦ 1 ) ) = 1 )
44 39 43 eqtrd ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐹 ↾ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) ) = 1 )
45 44 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 Σg ( 𝐹 ↾ ( 𝐼 ∖ ( 𝐹 supp 1 ) ) ) ) ( .r ‘ 𝑅 ) ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) ) = ( 1 ( .r ‘ 𝑅 ) ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) ) )
46 ovexd ⊢ ( 𝜑 → ( 𝐹 supp 1 ) ∈ V )
47 10 21 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐹 supp 1 ) ) : ( 𝐹 supp 1 ) ⟶ 𝐵 )
48 9 33 fsuppres ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐹 supp 1 ) ) finSupp 1 )
49 12 13 17 46 47 48 gsumcl ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) ∈ 𝐵 )
50 1 14 4 31 49 ringlidmd ⊢ ( 𝜑 → ( 1 ( .r ‘ 𝑅 ) ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) ) = ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) )
51 25 45 50 3eqtrd ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) = ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) )
52 11 51 breqtrd ⊢ ( 𝜑 → 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) )
53 reseq2 ⊢ ( 𝑏 = ∅ → ( 𝐹 ↾ 𝑏 ) = ( 𝐹 ↾ ∅ ) )
54 53 oveq2d ⊢ ( 𝑏 = ∅ → ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) = ( 𝑀 Σg ( 𝐹 ↾ ∅ ) ) )
55 54 breq2d ⊢ ( 𝑏 = ∅ → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) ↔ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ∅ ) ) ) )
56 rexeq ⊢ ( 𝑏 = ∅ → ( ∃ 𝑥 ∈ 𝑏 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ ∅ 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) )
57 55 56 imbi12d ⊢ ( 𝑏 = ∅ → ( ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) → ∃ 𝑥 ∈ 𝑏 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ∅ ) ) → ∃ 𝑥 ∈ ∅ 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) )
58 reseq2 ⊢ ( 𝑏 = 𝑎 → ( 𝐹 ↾ 𝑏 ) = ( 𝐹 ↾ 𝑎 ) )
59 58 oveq2d ⊢ ( 𝑏 = 𝑎 → ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) = ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) )
60 59 breq2d ⊢ ( 𝑏 = 𝑎 → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) ↔ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) ) )
61 rexeq ⊢ ( 𝑏 = 𝑎 → ( ∃ 𝑥 ∈ 𝑏 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) )
62 60 61 imbi12d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) → ∃ 𝑥 ∈ 𝑏 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) )
63 reseq2 ⊢ ( 𝑏 = ( 𝑎 ∪ { 𝑦 } ) → ( 𝐹 ↾ 𝑏 ) = ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) )
64 63 oveq2d ⊢ ( 𝑏 = ( 𝑎 ∪ { 𝑦 } ) → ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) = ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) )
65 64 breq2d ⊢ ( 𝑏 = ( 𝑎 ∪ { 𝑦 } ) → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) ↔ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) )
66 rexeq ⊢ ( 𝑏 = ( 𝑎 ∪ { 𝑦 } ) → ( ∃ 𝑥 ∈ 𝑏 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ ( 𝑎 ∪ { 𝑦 } ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) )
67 65 66 imbi12d ⊢ ( 𝑏 = ( 𝑎 ∪ { 𝑦 } ) → ( ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) → ∃ 𝑥 ∈ 𝑏 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) → ∃ 𝑥 ∈ ( 𝑎 ∪ { 𝑦 } ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) )
68 reseq2 ⊢ ( 𝑏 = ( 𝐹 supp 1 ) → ( 𝐹 ↾ 𝑏 ) = ( 𝐹 ↾ ( 𝐹 supp 1 ) ) )
69 68 oveq2d ⊢ ( 𝑏 = ( 𝐹 supp 1 ) → ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) = ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) )
70 69 breq2d ⊢ ( 𝑏 = ( 𝐹 supp 1 ) → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) ↔ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) ) )
71 rexeq ⊢ ( 𝑏 = ( 𝐹 supp 1 ) → ( ∃ 𝑥 ∈ 𝑏 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ ( 𝐹 supp 1 ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) )
72 70 71 imbi12d ⊢ ( 𝑏 = ( 𝐹 supp 1 ) → ( ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑏 ) ) → ∃ 𝑥 ∈ 𝑏 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) → ∃ 𝑥 ∈ ( 𝐹 supp 1 ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) )
73 4 3 2 6 7 rprmndvdsr1 ⊢ ( 𝜑 → ¬ 𝑄 ∥ 1 )
74 res0 ⊢ ( 𝐹 ↾ ∅ ) = ∅
75 74 oveq2i ⊢ ( 𝑀 Σg ( 𝐹 ↾ ∅ ) ) = ( 𝑀 Σg ∅ )
76 13 gsum0 ⊢ ( 𝑀 Σg ∅ ) = 1
77 75 76 eqtri ⊢ ( 𝑀 Σg ( 𝐹 ↾ ∅ ) ) = 1
78 77 a1i ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐹 ↾ ∅ ) ) = 1 )
79 78 breq2d ⊢ ( 𝜑 → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ∅ ) ) ↔ 𝑄 ∥ 1 ) )
80 73 79 mtbird ⊢ ( 𝜑 → ¬ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ∅ ) ) )
81 80 pm2.21d ⊢ ( 𝜑 → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ∅ ) ) → ∃ 𝑥 ∈ ∅ 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) )
82 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) ) → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) )
83 82 syldbl2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) )
84 vex ⊢ 𝑦 ∈ V
85 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
86 85 breq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ↔ 𝑄 ∥ ( 𝐹 ‘ 𝑦 ) ) )
87 84 86 rexsn ⊢ ( ∃ 𝑥 ∈ { 𝑦 } 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ↔ 𝑄 ∥ ( 𝐹 ‘ 𝑦 ) )
88 87 bilanri ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) ∧ 𝑄 ∥ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ { 𝑦 } 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) )
89 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑅 ∈ CRing )
90 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑄 ∈ 𝑃 )
91 89 16 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑀 ∈ CMnd )
92 vex ⊢ 𝑎 ∈ V
93 92 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑎 ∈ V )
94 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝐹 : 𝐼 ⟶ 𝐵 )
95 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑎 ⊆ ( 𝐹 supp 1 ) )
96 21 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( 𝐹 supp 1 ) ⊆ 𝐼 )
97 95 96 sstrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑎 ⊆ 𝐼 )
98 94 97 fssresd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( 𝐹 ↾ 𝑎 ) : 𝑎 ⟶ 𝐵 )
99 9 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 1 ) ∈ Fin )
100 99 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( 𝐹 supp 1 ) ∈ Fin )
101 100 95 ssfid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑎 ∈ Fin )
102 33 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 1 ∈ 𝐵 )
103 98 101 102 fdmfifsupp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( 𝐹 ↾ 𝑎 ) finSupp 1 )
104 12 13 91 93 98 103 gsumcl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) ∈ 𝐵 )
105 96 ssdifssd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ⊆ 𝐼 )
106 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) )
107 105 106 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑦 ∈ 𝐼 )
108 94 107 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
109 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) )
110 eqid ⊢ ( Cntz ‘ 𝑀 ) = ( Cntz ‘ 𝑀 )
111 eqid ⊢ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 )
112 40 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑀 ∈ Mnd )
113 106 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ¬ 𝑦 ∈ 𝑎 )
114 94 fimassd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( 𝐹 “ ( 𝑎 ∪ { 𝑦 } ) ) ⊆ 𝐵 )
115 12 110 cntzcmn ⊢ ( ( 𝑀 ∈ CMnd ∧ ( 𝐹 “ ( 𝑎 ∪ { 𝑦 } ) ) ⊆ 𝐵 ) → ( ( Cntz ‘ 𝑀 ) ‘ ( 𝐹 “ ( 𝑎 ∪ { 𝑦 } ) ) ) = 𝐵 )
116 91 114 115 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( ( Cntz ‘ 𝑀 ) ‘ ( 𝐹 “ ( 𝑎 ∪ { 𝑦 } ) ) ) = 𝐵 )
117 114 116 sseqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( 𝐹 “ ( 𝑎 ∪ { 𝑦 } ) ) ⊆ ( ( Cntz ‘ 𝑀 ) ‘ ( 𝐹 “ ( 𝑎 ∪ { 𝑦 } ) ) ) )
118 12 15 110 111 94 97 112 101 113 107 108 117 gsumzresunsn ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) = ( ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
119 109 118 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → 𝑄 ∥ ( ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
120 1 2 3 14 89 90 104 108 119 rprmdvds ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) ∨ 𝑄 ∥ ( 𝐹 ‘ 𝑦 ) ) )
121 83 88 120 orim12da ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ( ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ∨ ∃ 𝑥 ∈ { 𝑦 } 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) )
122 rexun ⊢ ( ∃ 𝑥 ∈ ( 𝑎 ∪ { 𝑦 } ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ↔ ( ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ∨ ∃ 𝑥 ∈ { 𝑦 } 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) )
123 121 122 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ∧ ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) ) → ∃ 𝑥 ∈ ( 𝑎 ∪ { 𝑦 } ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) )
124 123 exp31 ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ ( 𝐹 supp 1 ) ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) → ( ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) → ∃ 𝑥 ∈ ( 𝑎 ∪ { 𝑦 } ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) )
125 124 anasss ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( 𝐹 supp 1 ) ∧ 𝑦 ∈ ( ( 𝐹 supp 1 ) ∖ 𝑎 ) ) ) → ( ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ 𝑎 ) ) → ∃ 𝑥 ∈ 𝑎 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝑎 ∪ { 𝑦 } ) ) ) → ∃ 𝑥 ∈ ( 𝑎 ∪ { 𝑦 } ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) ) )
126 57 62 67 72 81 125 99 findcard2d ⊢ ( 𝜑 → ( 𝑄 ∥ ( 𝑀 Σg ( 𝐹 ↾ ( 𝐹 supp 1 ) ) ) → ∃ 𝑥 ∈ ( 𝐹 supp 1 ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) ) )
127 52 126 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐹 supp 1 ) 𝑄 ∥ ( 𝐹 ‘ 𝑥 ) )