Metamath Proof Explorer

Theorem evl1gprodd

Description: Polynomial evaluation builder for a finite group product of polynomials. (Contributed by metakunt, 29-Apr-2025)

Ref Expression
Hypotheses evl1gprodd.1 ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
evl1gprodd.2 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
evl1gprodd.3 ⊢ 𝑄 = ( mulGrp ‘ 𝑃 )
evl1gprodd.4 ⊢ 𝐵 = ( Base ‘ 𝑅 )
evl1gprodd.5 ⊢ 𝑈 = ( Base ‘ 𝑃 )
evl1gprodd.6 ⊢ 𝑆 = ( mulGrp ‘ 𝑅 )
evl1gprodd.7 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evl1gprodd.8 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
evl1gprodd.9 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝑈 )
evl1gprodd.10 ⊢ ( 𝜑 → 𝑁 ∈ Fin )
Assertion evl1gprodd ( 𝜑 → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 evl1gprodd.1 ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2 evl1gprodd.2 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 evl1gprodd.3 ⊢ 𝑄 = ( mulGrp ‘ 𝑃 )
4 evl1gprodd.4 ⊢ 𝐵 = ( Base ‘ 𝑅 )
5 evl1gprodd.5 ⊢ 𝑈 = ( Base ‘ 𝑃 )
6 evl1gprodd.6 ⊢ 𝑆 = ( mulGrp ‘ 𝑅 )
7 evl1gprodd.7 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
8 evl1gprodd.8 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 evl1gprodd.9 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝑈 )
10 evl1gprodd.10 ⊢ ( 𝜑 → 𝑁 ∈ Fin )
11 mpteq1 ⊢ ( 𝑎 = ∅ → ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) = ( 𝑥 ∈ ∅ ↦ 𝑀 ) )
12 11 oveq2d ⊢ ( 𝑎 = ∅ → ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) = ( 𝑄 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) )
13 12 fveq2d ⊢ ( 𝑎 = ∅ → ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) )
14 13 fveq1d ⊢ ( 𝑎 = ∅ → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) )
15 mpteq1 ⊢ ( 𝑎 = ∅ → ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) )
16 15 oveq2d ⊢ ( 𝑎 = ∅ → ( 𝑆 Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑆 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
17 14 16 eqeq12d ⊢ ( 𝑎 = ∅ → ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ↔ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) )
18 mpteq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) = ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) )
19 18 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) = ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) )
20 19 fveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) )
21 20 fveq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) )
22 mpteq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) )
23 22 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑆 Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
24 21 23 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ↔ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) )
25 mpteq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) = ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) )
26 25 oveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) = ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) )
27 26 fveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) ) )
28 27 fveq1d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) )
29 mpteq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) )
30 29 oveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( 𝑆 Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑆 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
31 28 30 eqeq12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑐 } ) → ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ↔ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) )
32 mpteq1 ⊢ ( 𝑎 = 𝑁 → ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) = ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) )
33 32 oveq2d ⊢ ( 𝑎 = 𝑁 → ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) = ( 𝑄 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) )
34 33 fveq2d ⊢ ( 𝑎 = 𝑁 → ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) )
35 34 fveq1d ⊢ ( 𝑎 = 𝑁 → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝑌 ) )
36 mpteq1 ⊢ ( 𝑎 = 𝑁 → ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) )
37 36 oveq2d ⊢ ( 𝑎 = 𝑁 → ( 𝑆 Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
38 35 37 eqeq12d ⊢ ( 𝑎 = 𝑁 → ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑎 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑎 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ↔ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) )
39 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ 𝑀 ) = ∅
40 39 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ∅ ↦ 𝑀 ) = ∅ )
41 40 oveq2d ⊢ ( 𝜑 → ( 𝑄 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) = ( 𝑄 Σg ∅ ) )
42 41 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑄 Σg ∅ ) ) )
43 42 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑄 Σg ∅ ) ) ‘ 𝑌 ) )
44 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ∅
45 44 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ∅ ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ∅ )
46 45 oveq2d ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑆 Σg ∅ ) )
47 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
48 47 gsum0 ⊢ ( 𝑆 Σg ∅ ) = ( 0g ‘ 𝑆 )
49 48 a1i ⊢ ( 𝜑 → ( 𝑆 Σg ∅ ) = ( 0g ‘ 𝑆 ) )
50 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
51 6 50 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑆 )
52 51 eqcomi ⊢ ( 0g ‘ 𝑆 ) = ( 1r ‘ 𝑅 )
53 52 a1i ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 1r ‘ 𝑅 ) )
54 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
55 7 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
56 6 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝑆 ∈ Mnd )
57 55 56 syl ⊢ ( 𝜑 → 𝑆 ∈ Mnd )
58 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
59 58 47 mndidcl ⊢ ( 𝑆 ∈ Mnd → ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
60 57 59 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
61 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
62 6 61 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 )
63 4 62 eqtri ⊢ 𝐵 = ( Base ‘ 𝑆 )
64 60 63 eleqtrrdi ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ 𝐵 )
65 51 a1i ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑆 ) )
66 65 eleq1d ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ↔ ( 0g ‘ 𝑆 ) ∈ 𝐵 ) )
67 64 66 mpbird ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
68 1 2 4 54 5 7 67 8 evl1scad ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝑌 ) = ( 1r ‘ 𝑅 ) ) )
69 68 simprd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝑌 ) = ( 1r ‘ 𝑅 ) )
70 69 eqcomd ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝑌 ) )
71 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
72 2 54 50 71 ply1scl1 ⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
73 55 72 syl ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
74 3 71 ringidval ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑄 )
75 74 a1i ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑄 ) )
76 73 75 eqtrd ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 0g ‘ 𝑄 ) )
77 76 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑂 ‘ ( 0g ‘ 𝑄 ) ) )
78 77 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 0g ‘ 𝑄 ) ) ‘ 𝑌 ) )
79 70 78 eqtrd ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( ( 𝑂 ‘ ( 0g ‘ 𝑄 ) ) ‘ 𝑌 ) )
80 53 79 eqtrd ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( ( 𝑂 ‘ ( 0g ‘ 𝑄 ) ) ‘ 𝑌 ) )
81 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
82 81 gsum0 ⊢ ( 𝑄 Σg ∅ ) = ( 0g ‘ 𝑄 )
83 82 a1i ⊢ ( 𝜑 → ( 𝑄 Σg ∅ ) = ( 0g ‘ 𝑄 ) )
84 83 eqcomd ⊢ ( 𝜑 → ( 0g ‘ 𝑄 ) = ( 𝑄 Σg ∅ ) )
85 84 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 0g ‘ 𝑄 ) ) = ( 𝑂 ‘ ( 𝑄 Σg ∅ ) ) )
86 85 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 0g ‘ 𝑄 ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑄 Σg ∅ ) ) ‘ 𝑌 ) )
87 49 80 86 3eqtrd ⊢ ( 𝜑 → ( 𝑆 Σg ∅ ) = ( ( 𝑂 ‘ ( 𝑄 Σg ∅ ) ) ‘ 𝑌 ) )
88 46 87 eqtr2d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑄 Σg ∅ ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
89 43 88 eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
90 nfcv ⊢ Ⅎ 𝑦 𝑀
91 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝑀
92 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝑀 = ⦋ 𝑦 / 𝑥 ⦌ 𝑀 )
93 90 91 92 cbvmpt ⊢ ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) = ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 )
94 93 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) = ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) )
95 94 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) = ( 𝑄 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) )
96 95 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑄 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ) )
97 96 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ) ‘ 𝑌 ) )
98 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
99 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
100 3 99 mgpplusg ⊢ ( .r ‘ 𝑃 ) = ( +g ‘ 𝑄 )
101 2 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
102 7 101 syl ⊢ ( 𝜑 → 𝑃 ∈ CRing )
103 3 crngmgp ⊢ ( 𝑃 ∈ CRing → 𝑄 ∈ CMnd )
104 102 103 syl ⊢ ( 𝜑 → 𝑄 ∈ CMnd )
105 104 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → 𝑄 ∈ CMnd )
106 105 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → 𝑄 ∈ CMnd )
107 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → 𝑁 ∈ Fin )
108 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → 𝑏 ⊆ 𝑁 )
109 107 108 ssfid ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → 𝑏 ∈ Fin )
110 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝑈 )
111 108 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → 𝑦 ∈ 𝑁 )
112 rspcsbela ⊢ ( ( 𝑦 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝑈 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝑈 )
113 112 expcom ⊢ ( ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝑈 → ( 𝑦 ∈ 𝑁 → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝑈 ) )
114 113 imp ⊢ ( ( ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝑈 ∧ 𝑦 ∈ 𝑁 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝑈 )
115 110 111 114 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝑈 )
116 3 5 mgpbas ⊢ 𝑈 = ( Base ‘ 𝑄 )
117 116 eqcomi ⊢ ( Base ‘ 𝑄 ) = 𝑈
118 117 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑄 ) = 𝑈 )
119 118 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( Base ‘ 𝑄 ) = 𝑈 )
120 119 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( Base ‘ 𝑄 ) = 𝑈 )
121 120 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ( Base ‘ 𝑄 ) = 𝑈 )
122 121 eleq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ ( Base ‘ 𝑄 ) ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝑈 ) )
123 115 122 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ ( Base ‘ 𝑄 ) )
124 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) )
125 124 eldifbd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ¬ 𝑐 ∈ 𝑏 )
126 124 eldifad ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → 𝑐 ∈ 𝑁 )
127 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝑈 )
128 rspcsbela ⊢ ( ( 𝑐 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝑈 ) → ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ∈ 𝑈 )
129 126 127 128 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ∈ 𝑈 )
130 120 eleq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ∈ ( Base ‘ 𝑄 ) ↔ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ∈ 𝑈 ) )
131 129 130 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ∈ ( Base ‘ 𝑄 ) )
132 csbeq1 ⊢ ( 𝑦 = 𝑐 → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 = ⦋ 𝑐 / 𝑥 ⦌ 𝑀 )
133 98 100 106 109 123 124 125 131 132 gsumunsn ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑄 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) = ( ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ( .r ‘ 𝑃 ) ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) )
134 133 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑂 ‘ ( 𝑄 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ) = ( 𝑂 ‘ ( ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ( .r ‘ 𝑃 ) ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ) )
135 134 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ( .r ‘ 𝑃 ) ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ) ‘ 𝑌 ) )
136 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → 𝑅 ∈ CRing )
137 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → 𝑌 ∈ 𝐵 )
138 115 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ∀ 𝑦 ∈ 𝑏 ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝑈 )
139 116 106 109 138 gsummptcl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ∈ 𝑈 )
140 92 equcoms ⊢ ( 𝑦 = 𝑥 → 𝑀 = ⦋ 𝑦 / 𝑥 ⦌ 𝑀 )
141 140 eqcomd ⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 = 𝑀 )
142 91 90 141 cbvmpt ⊢ ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) = ( 𝑥 ∈ 𝑏 ↦ 𝑀 )
143 142 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) = ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) )
144 143 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) = ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) )
145 144 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑂 ‘ ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) )
146 145 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) )
147 139 146 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) ) )
148 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) )
149 129 148 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ∈ 𝑈 ∧ ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ) )
150 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
151 1 2 4 5 136 137 147 149 99 150 evl1muld ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ( .r ‘ 𝑃 ) ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ( .r ‘ 𝑃 ) ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ) ) )
152 151 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( ( 𝑄 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ( .r ‘ 𝑃 ) ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ) )
153 135 152 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ) )
154 97 153 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ) )
155 6 150 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑆 )
156 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
157 156 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
158 7 157 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
159 6 158 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ CMnd )
160 159 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → 𝑆 ∈ CMnd )
161 160 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → 𝑆 ∈ CMnd )
162 csbfv12 ⊢ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝑂 ‘ 𝑀 ) ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑌 )
163 csbfv2g ⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑥 ⦌ ( 𝑂 ‘ 𝑀 ) = ( 𝑂 ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) )
164 163 elv ⊢ ⦋ 𝑦 / 𝑥 ⦌ ( 𝑂 ‘ 𝑀 ) = ( 𝑂 ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 )
165 vex ⊢ 𝑦 ∈ V
166 nfcv ⊢ Ⅎ 𝑥 𝑌
167 165 166 csbgfi ⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝑌 = 𝑌
168 164 167 fveq12i ⊢ ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝑂 ‘ 𝑀 ) ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑌 ) = ( ( 𝑂 ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 )
169 162 168 eqtri ⊢ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 )
170 62 eqcomi ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑅 )
171 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → 𝑅 ∈ CRing )
172 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → 𝑌 ∈ 𝐵 )
173 63 eqcomi ⊢ ( Base ‘ 𝑆 ) = 𝐵
174 173 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ( Base ‘ 𝑆 ) = 𝐵 )
175 174 eleq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ( 𝑌 ∈ ( Base ‘ 𝑆 ) ↔ 𝑌 ∈ 𝐵 ) )
176 172 175 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → 𝑌 ∈ ( Base ‘ 𝑆 ) )
177 1 2 170 5 171 176 115 fveval1fvcl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ( ( 𝑂 ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
178 169 177 eqeltrid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
179 1 2 4 5 136 137 129 fveval1fvcl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )
180 179 63 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
181 nfcv ⊢ Ⅎ 𝑥 𝑐
182 nfcv ⊢ Ⅎ 𝑥 𝑂
183 181 nfcsb1 ⊢ Ⅎ 𝑥 ⦋ 𝑐 / 𝑥 ⦌ 𝑀
184 182 183 nffv ⊢ Ⅎ 𝑥 ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 )
185 184 166 nffv ⊢ Ⅎ 𝑥 ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 )
186 csbeq1a ⊢ ( 𝑥 = 𝑐 → 𝑀 = ⦋ 𝑐 / 𝑥 ⦌ 𝑀 )
187 186 fveq2d ⊢ ( 𝑥 = 𝑐 → ( 𝑂 ‘ 𝑀 ) = ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) )
188 187 fveq1d ⊢ ( 𝑥 = 𝑐 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) )
189 181 185 188 csbhypf ⊢ ( 𝑦 = 𝑐 → ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) )
190 58 155 161 109 178 124 125 180 189 gsumunsn ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑆 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) = ( ( 𝑆 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ) )
191 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
192 nfcv ⊢ Ⅎ 𝑦 ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 )
193 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 )
194 csbeq1a ⊢ ( 𝑥 = 𝑦 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) )
195 192 193 194 cbvmpt ⊢ ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) )
196 195 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) )
197 196 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑆 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
198 191 197 eqtr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑆 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) = ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) )
199 198 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑆 Σg ( 𝑦 ∈ 𝑏 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ) = ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ) )
200 190 199 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑆 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) = ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ) )
201 200 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝑀 ) ‘ 𝑌 ) ) = ( 𝑆 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
202 154 201 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
203 192 193 194 cbvmpt ⊢ ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) )
204 203 eqcomi ⊢ ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) )
205 204 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) = ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) )
206 205 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( 𝑆 Σg ( 𝑦 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑆 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
207 202 206 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) ∧ ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )
208 207 ex ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝑁 ∧ 𝑐 ∈ ( 𝑁 ∖ 𝑏 ) ) ) → ( ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑏 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑏 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ ( 𝑏 ∪ { 𝑐 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) )
209 17 24 31 38 89 208 10 findcard2d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑄 Σg ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑆 Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )