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