Step | Hyp | Ref
| Expression |
1 | | evlseu.p |
. . . 4
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
2 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝑃) |
3 | | evlseu.c |
. . . 4
⊢ 𝐶 = (Base‘𝑆) |
4 | | eqid 2737 |
. . . 4
⊢ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} = {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈
Fin} |
5 | | eqid 2737 |
. . . 4
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
6 | | eqid 2737 |
. . . 4
⊢
(.g‘(mulGrp‘𝑆)) =
(.g‘(mulGrp‘𝑆)) |
7 | | eqid 2737 |
. . . 4
⊢
(.r‘𝑆) = (.r‘𝑆) |
8 | | evlseu.v |
. . . 4
⊢ 𝑉 = (𝐼 mVar 𝑅) |
9 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) |
10 | | evlseu.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
11 | | evlseu.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ CRing) |
12 | | evlseu.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ CRing) |
13 | | evlseu.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
14 | | evlseu.g |
. . . 4
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) |
15 | | evlseu.a |
. . . 4
⊢ 𝐴 = (algSc‘𝑃) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | evlslem1 21042 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∈ (𝑃 RingHom 𝑆) ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺)) |
17 | | coeq1 5726 |
. . . . . . 7
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) → (𝑚 ∘ 𝐴) = ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴)) |
18 | 17 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) → ((𝑚 ∘ 𝐴) = 𝐹 ↔ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹)) |
19 | | coeq1 5726 |
. . . . . . 7
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) → (𝑚 ∘ 𝑉) = ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉)) |
20 | 19 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) → ((𝑚 ∘ 𝑉) = 𝐺 ↔ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺)) |
21 | 18, 20 | anbi12d 634 |
. . . . 5
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ↔ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺))) |
22 | 21 | rspcev 3537 |
. . . 4
⊢ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∈ (𝑃 RingHom 𝑆) ∧ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺)) → ∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |
23 | 22 | 3impb 1117 |
. . 3
⊢ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∈ (𝑃 RingHom 𝑆) ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺) → ∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |
24 | 16, 23 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |
25 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
26 | | crngring 19574 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
27 | 11, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
28 | 1, 2, 25, 15, 10, 27 | mplasclf 21023 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:(Base‘𝑅)⟶(Base‘𝑃)) |
29 | 28 | ffund 6549 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐴) |
30 | | funcoeqres 6691 |
. . . . . . . 8
⊢ ((Fun
𝐴 ∧ (𝑚 ∘ 𝐴) = 𝐹) → (𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴)) |
31 | 29, 30 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∘ 𝐴) = 𝐹) → (𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴)) |
32 | 1, 8, 2, 10, 27 | mvrf2 21018 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑃)) |
33 | 32 | ffund 6549 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝑉) |
34 | | funcoeqres 6691 |
. . . . . . . 8
⊢ ((Fun
𝑉 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) |
35 | 33, 34 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) |
36 | 31, 35 | anim12dan 622 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) → ((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉))) |
37 | 36 | ex 416 |
. . . . 5
⊢ (𝜑 → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → ((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)))) |
38 | | resundi 5865 |
. . . . . 6
⊢ (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝑚 ↾ ran 𝐴) ∪ (𝑚 ↾ ran 𝑉)) |
39 | | uneq12 4072 |
. . . . . 6
⊢ (((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) → ((𝑚 ↾ ran 𝐴) ∪ (𝑚 ↾ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) |
40 | 38, 39 | syl5eq 2790 |
. . . . 5
⊢ (((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) |
41 | 37, 40 | syl6 35 |
. . . 4
⊢ (𝜑 → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))) |
42 | 41 | ralrimivw 3106 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ (𝑃 RingHom 𝑆)(((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))) |
43 | | eqtr3 2763 |
. . . . . 6
⊢ (((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉))) |
44 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
45 | 44, 10, 11 | psrassa 20939 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ AssAlg) |
46 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
47 | 44, 8, 46, 10, 27 | mvrf 20949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘(𝐼 mPwSer 𝑅))) |
48 | 47 | frnd 6553 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘(𝐼 mPwSer 𝑅))) |
49 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(AlgSpan‘(𝐼
mPwSer 𝑅)) =
(AlgSpan‘(𝐼 mPwSer
𝑅)) |
50 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(algSc‘(𝐼
mPwSer 𝑅)) =
(algSc‘(𝐼 mPwSer
𝑅)) |
51 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(mrCls‘(SubRing‘(𝐼 mPwSer 𝑅))) = (mrCls‘(SubRing‘(𝐼 mPwSer 𝑅))) |
52 | 49, 50, 51, 46 | aspval2 20858 |
. . . . . . . . . . . 12
⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘(𝐼 mPwSer 𝑅))) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))) |
53 | 45, 48, 52 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))) |
54 | 1, 44, 8, 49, 10, 11 | mplbas2 20999 |
. . . . . . . . . . 11
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = (Base‘𝑃)) |
55 | 44, 1, 2, 10, 27 | mplsubrg 20967 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (Base‘𝑃) ∈ (SubRing‘(𝐼 mPwSer 𝑅))) |
56 | 1, 44, 2 | mplval2 20958 |
. . . . . . . . . . . . . . . 16
⊢ 𝑃 = ((𝐼 mPwSer 𝑅) ↾s (Base‘𝑃)) |
57 | 56 | subsubrg2 19827 |
. . . . . . . . . . . . . . 15
⊢
((Base‘𝑃)
∈ (SubRing‘(𝐼
mPwSer 𝑅)) →
(SubRing‘𝑃) =
((SubRing‘(𝐼 mPwSer
𝑅)) ∩ 𝒫
(Base‘𝑃))) |
58 | 55, 57 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (SubRing‘𝑃) = ((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))) |
59 | 58 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(mrCls‘(SubRing‘𝑃)) = (mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))) |
60 | 50, 56 | ressascl 20856 |
. . . . . . . . . . . . . . . . 17
⊢
((Base‘𝑃)
∈ (SubRing‘(𝐼
mPwSer 𝑅)) →
(algSc‘(𝐼 mPwSer
𝑅)) = (algSc‘𝑃)) |
61 | 55, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (algSc‘(𝐼 mPwSer 𝑅)) = (algSc‘𝑃)) |
62 | 15, 61 | eqtr4id 2797 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 = (algSc‘(𝐼 mPwSer 𝑅))) |
63 | 62 | rneqd 5807 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐴 = ran (algSc‘(𝐼 mPwSer 𝑅))) |
64 | 63 | uneq1d 4076 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran 𝐴 ∪ ran 𝑉) = (ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)) |
65 | 59, 64 | fveq12d 6724 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) = ((mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))‘(ran
(algSc‘(𝐼 mPwSer
𝑅)) ∪ ran 𝑉))) |
66 | | assaring 20823 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 mPwSer 𝑅) ∈ AssAlg → (𝐼 mPwSer 𝑅) ∈ Ring) |
67 | 46 | subrgmre 19824 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 mPwSer 𝑅) ∈ Ring → (SubRing‘(𝐼 mPwSer 𝑅)) ∈ (Moore‘(Base‘(𝐼 mPwSer 𝑅)))) |
68 | 45, 66, 67 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (SubRing‘(𝐼 mPwSer 𝑅)) ∈ (Moore‘(Base‘(𝐼 mPwSer 𝑅)))) |
69 | 28 | frnd 6553 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐴 ⊆ (Base‘𝑃)) |
70 | 63, 69 | eqsstrrd 3940 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran (algSc‘(𝐼 mPwSer 𝑅)) ⊆ (Base‘𝑃)) |
71 | 32 | frnd 6553 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑃)) |
72 | 70, 71 | unssd 4100 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉) ⊆ (Base‘𝑃)) |
73 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))) =
(mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))) |
74 | 51, 73 | submrc 17131 |
. . . . . . . . . . . . 13
⊢
(((SubRing‘(𝐼
mPwSer 𝑅)) ∈
(Moore‘(Base‘(𝐼
mPwSer 𝑅))) ∧
(Base‘𝑃) ∈
(SubRing‘(𝐼 mPwSer
𝑅)) ∧ (ran
(algSc‘(𝐼 mPwSer
𝑅)) ∪ ran 𝑉) ⊆ (Base‘𝑃)) →
((mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))‘(ran
(algSc‘(𝐼 mPwSer
𝑅)) ∪ ran 𝑉)) =
((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))) |
75 | 68, 55, 72, 74 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))‘(ran
(algSc‘(𝐼 mPwSer
𝑅)) ∪ ran 𝑉)) =
((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))) |
76 | 65, 75 | eqtr2d 2778 |
. . . . . . . . . . 11
⊢ (𝜑 →
((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)) = ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉))) |
77 | 53, 54, 76 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑃) =
((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉))) |
78 | 77 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (Base‘𝑃) = ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉))) |
79 | 1 | mplring 20980 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) |
80 | 10, 27, 79 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ Ring) |
81 | 2 | subrgmre 19824 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring →
(SubRing‘𝑃) ∈
(Moore‘(Base‘𝑃))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (SubRing‘𝑃) ∈
(Moore‘(Base‘𝑃))) |
83 | 82 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (SubRing‘𝑃) ∈ (Moore‘(Base‘𝑃))) |
84 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) |
85 | | rhmeql 19830 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆)) → dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃)) |
86 | 85 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃)) |
87 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(mrCls‘(SubRing‘𝑃)) = (mrCls‘(SubRing‘𝑃)) |
88 | 87 | mrcsscl 17123 |
. . . . . . . . . 10
⊢
(((SubRing‘𝑃)
∈ (Moore‘(Base‘𝑃)) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛) ∧ dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃)) → ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) ⊆ dom (𝑚 ∩ 𝑛)) |
89 | 83, 84, 86, 88 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) ⊆ dom (𝑚 ∩ 𝑛)) |
90 | 78, 89 | eqsstrd 3939 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛)) |
91 | 90 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛) → (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛))) |
92 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑚 ∈ (𝑃 RingHom 𝑆)) |
93 | 2, 3 | rhmf 19746 |
. . . . . . . . 9
⊢ (𝑚 ∈ (𝑃 RingHom 𝑆) → 𝑚:(Base‘𝑃)⟶𝐶) |
94 | | ffn 6545 |
. . . . . . . . 9
⊢ (𝑚:(Base‘𝑃)⟶𝐶 → 𝑚 Fn (Base‘𝑃)) |
95 | 92, 93, 94 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑚 Fn (Base‘𝑃)) |
96 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑛 ∈ (𝑃 RingHom 𝑆)) |
97 | 2, 3 | rhmf 19746 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑃 RingHom 𝑆) → 𝑛:(Base‘𝑃)⟶𝐶) |
98 | | ffn 6545 |
. . . . . . . . 9
⊢ (𝑛:(Base‘𝑃)⟶𝐶 → 𝑛 Fn (Base‘𝑃)) |
99 | 96, 97, 98 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑛 Fn (Base‘𝑃)) |
100 | 69 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ran 𝐴 ⊆ (Base‘𝑃)) |
101 | 71 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ran 𝑉 ⊆ (Base‘𝑃)) |
102 | 100, 101 | unssd 4100 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (ran 𝐴 ∪ ran 𝑉) ⊆ (Base‘𝑃)) |
103 | | fnreseql 6868 |
. . . . . . . 8
⊢ ((𝑚 Fn (Base‘𝑃) ∧ 𝑛 Fn (Base‘𝑃) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ (Base‘𝑃)) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) ↔ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛))) |
104 | 95, 99, 102, 103 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) ↔ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛))) |
105 | | fneqeql2 6867 |
. . . . . . . 8
⊢ ((𝑚 Fn (Base‘𝑃) ∧ 𝑛 Fn (Base‘𝑃)) → (𝑚 = 𝑛 ↔ (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛))) |
106 | 95, 99, 105 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (𝑚 = 𝑛 ↔ (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛))) |
107 | 91, 104, 106 | 3imtr4d 297 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) → 𝑚 = 𝑛)) |
108 | 43, 107 | syl5 34 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛)) |
109 | 108 | ralrimivva 3112 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ (𝑃 RingHom 𝑆)∀𝑛 ∈ (𝑃 RingHom 𝑆)(((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛)) |
110 | | reseq1 5845 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉))) |
111 | 110 | eqeq1d 2739 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ↔ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))) |
112 | 111 | rmo4 3643 |
. . . 4
⊢
(∃*𝑚 ∈
(𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ↔ ∀𝑚 ∈ (𝑃 RingHom 𝑆)∀𝑛 ∈ (𝑃 RingHom 𝑆)(((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛)) |
113 | 109, 112 | sylibr 237 |
. . 3
⊢ (𝜑 → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) |
114 | | rmoim 3653 |
. . 3
⊢
(∀𝑚 ∈
(𝑃 RingHom 𝑆)(((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → (∃*𝑚 ∈ (𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))) |
115 | 42, 113, 114 | sylc 65 |
. 2
⊢ (𝜑 → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |
116 | | reu5 3337 |
. 2
⊢
(∃!𝑚 ∈
(𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ↔ (∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ∧ ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))) |
117 | 24, 115, 116 | sylanbrc 586 |
1
⊢ (𝜑 → ∃!𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |