Step | Hyp | Ref
| Expression |
1 | | evlseu.p |
. . . 4
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
2 | | eqid 2794 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝑃) |
3 | | evlseu.c |
. . . 4
⊢ 𝐶 = (Base‘𝑆) |
4 | | eqid 2794 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
5 | | eqid 2794 |
. . . 4
⊢ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} = {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈
Fin} |
6 | | eqid 2794 |
. . . 4
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
7 | | eqid 2794 |
. . . 4
⊢
(.g‘(mulGrp‘𝑆)) =
(.g‘(mulGrp‘𝑆)) |
8 | | eqid 2794 |
. . . 4
⊢
(.r‘𝑆) = (.r‘𝑆) |
9 | | evlseu.v |
. . . 4
⊢ 𝑉 = (𝐼 mVar 𝑅) |
10 | | eqid 2794 |
. . . 4
⊢ (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) |
11 | | evlseu.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ V) |
12 | | evlseu.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ CRing) |
13 | | evlseu.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ CRing) |
14 | | evlseu.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) |
15 | | evlseu.g |
. . . 4
⊢ (𝜑 → 𝐺:𝐼⟶𝐶) |
16 | | evlseu.a |
. . . 4
⊢ 𝐴 = (algSc‘𝑃) |
17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16 | evlslem1 19982 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∈ (𝑃 RingHom 𝑆) ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺)) |
18 | | coeq1 5617 |
. . . . . . 7
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) → (𝑚 ∘ 𝐴) = ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴)) |
19 | 18 | eqeq1d 2796 |
. . . . . 6
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) → ((𝑚 ∘ 𝐴) = 𝐹 ↔ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹)) |
20 | | coeq1 5617 |
. . . . . . 7
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) → (𝑚 ∘ 𝑉) = ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉)) |
21 | 20 | eqeq1d 2796 |
. . . . . 6
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) → ((𝑚 ∘ 𝑉) = 𝐺 ↔ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺)) |
22 | 19, 21 | anbi12d 630 |
. . . . 5
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ↔ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺))) |
23 | 22 | rspcev 3557 |
. . . 4
⊢ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∈ (𝑃 RingHom 𝑆) ∧ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺)) → ∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |
24 | 23 | 3impb 1108 |
. . 3
⊢ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∈ (𝑃 RingHom 𝑆) ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺) → ∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |
25 | 17, 24 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |
26 | | crngring 18998 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
27 | 12, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
28 | | eqid 2794 |
. . . . . . . . . . 11
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
29 | 1 | mplring 19920 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) |
30 | 1 | mpllmod 19919 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod) |
31 | | eqid 2794 |
. . . . . . . . . . 11
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
32 | 16, 28, 29, 30, 31, 2 | asclf 19799 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝐴:(Base‘(Scalar‘𝑃))⟶(Base‘𝑃)) |
33 | 11, 27, 32 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:(Base‘(Scalar‘𝑃))⟶(Base‘𝑃)) |
34 | 33 | ffund 6389 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐴) |
35 | | funcoeqres 6516 |
. . . . . . . 8
⊢ ((Fun
𝐴 ∧ (𝑚 ∘ 𝐴) = 𝐹) → (𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴)) |
36 | 34, 35 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∘ 𝐴) = 𝐹) → (𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴)) |
37 | 1, 9, 2, 11, 27 | mvrf2 19959 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑃)) |
38 | 37 | ffund 6389 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝑉) |
39 | | funcoeqres 6516 |
. . . . . . . 8
⊢ ((Fun
𝑉 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) |
40 | 38, 39 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) |
41 | 36, 40 | anim12dan 618 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) → ((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉))) |
42 | 41 | ex 413 |
. . . . 5
⊢ (𝜑 → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → ((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)))) |
43 | | resundi 5751 |
. . . . . 6
⊢ (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝑚 ↾ ran 𝐴) ∪ (𝑚 ↾ ran 𝑉)) |
44 | | uneq12 4057 |
. . . . . 6
⊢ (((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) → ((𝑚 ↾ ran 𝐴) ∪ (𝑚 ↾ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) |
45 | 43, 44 | syl5eq 2842 |
. . . . 5
⊢ (((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) |
46 | 42, 45 | syl6 35 |
. . . 4
⊢ (𝜑 → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))) |
47 | 46 | ralrimivw 3149 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ (𝑃 RingHom 𝑆)(((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))) |
48 | | eqtr3 2817 |
. . . . . 6
⊢ (((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉))) |
49 | | eqid 2794 |
. . . . . . . . . . . . 13
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
50 | 49, 11, 12 | psrassa 19882 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ AssAlg) |
51 | | eqid 2794 |
. . . . . . . . . . . . . 14
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
52 | 49, 9, 51, 11, 27 | mvrf 19892 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘(𝐼 mPwSer 𝑅))) |
53 | 52 | frnd 6392 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘(𝐼 mPwSer 𝑅))) |
54 | | eqid 2794 |
. . . . . . . . . . . . 13
⊢
(AlgSpan‘(𝐼
mPwSer 𝑅)) =
(AlgSpan‘(𝐼 mPwSer
𝑅)) |
55 | | eqid 2794 |
. . . . . . . . . . . . 13
⊢
(algSc‘(𝐼
mPwSer 𝑅)) =
(algSc‘(𝐼 mPwSer
𝑅)) |
56 | | eqid 2794 |
. . . . . . . . . . . . 13
⊢
(mrCls‘(SubRing‘(𝐼 mPwSer 𝑅))) = (mrCls‘(SubRing‘(𝐼 mPwSer 𝑅))) |
57 | 54, 55, 56, 51 | aspval2 19815 |
. . . . . . . . . . . 12
⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘(𝐼 mPwSer 𝑅))) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))) |
58 | 50, 53, 57 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))) |
59 | 1, 49, 9, 54, 11, 12 | mplbas2 19938 |
. . . . . . . . . . 11
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = (Base‘𝑃)) |
60 | 49, 1, 2, 11, 27 | mplsubrg 19908 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (Base‘𝑃) ∈ (SubRing‘(𝐼 mPwSer 𝑅))) |
61 | 1, 49, 2 | mplval2 19899 |
. . . . . . . . . . . . . . . 16
⊢ 𝑃 = ((𝐼 mPwSer 𝑅) ↾s (Base‘𝑃)) |
62 | 61 | subsubrg2 19252 |
. . . . . . . . . . . . . . 15
⊢
((Base‘𝑃)
∈ (SubRing‘(𝐼
mPwSer 𝑅)) →
(SubRing‘𝑃) =
((SubRing‘(𝐼 mPwSer
𝑅)) ∩ 𝒫
(Base‘𝑃))) |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (SubRing‘𝑃) = ((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))) |
64 | 63 | fveq2d 6545 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(mrCls‘(SubRing‘𝑃)) = (mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))) |
65 | 55, 61 | ressascl 19812 |
. . . . . . . . . . . . . . . . 17
⊢
((Base‘𝑃)
∈ (SubRing‘(𝐼
mPwSer 𝑅)) →
(algSc‘(𝐼 mPwSer
𝑅)) = (algSc‘𝑃)) |
66 | 60, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (algSc‘(𝐼 mPwSer 𝑅)) = (algSc‘𝑃)) |
67 | 66, 16 | syl6reqr 2849 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 = (algSc‘(𝐼 mPwSer 𝑅))) |
68 | 67 | rneqd 5693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐴 = ran (algSc‘(𝐼 mPwSer 𝑅))) |
69 | 68 | uneq1d 4061 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran 𝐴 ∪ ran 𝑉) = (ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)) |
70 | 64, 69 | fveq12d 6548 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) = ((mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))‘(ran
(algSc‘(𝐼 mPwSer
𝑅)) ∪ ran 𝑉))) |
71 | | assaring 19782 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 mPwSer 𝑅) ∈ AssAlg → (𝐼 mPwSer 𝑅) ∈ Ring) |
72 | 51 | subrgmre 19249 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 mPwSer 𝑅) ∈ Ring → (SubRing‘(𝐼 mPwSer 𝑅)) ∈ (Moore‘(Base‘(𝐼 mPwSer 𝑅)))) |
73 | 50, 71, 72 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (SubRing‘(𝐼 mPwSer 𝑅)) ∈ (Moore‘(Base‘(𝐼 mPwSer 𝑅)))) |
74 | 33 | frnd 6392 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐴 ⊆ (Base‘𝑃)) |
75 | 68, 74 | eqsstrrd 3929 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran (algSc‘(𝐼 mPwSer 𝑅)) ⊆ (Base‘𝑃)) |
76 | 37 | frnd 6392 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑃)) |
77 | 75, 76 | unssd 4085 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉) ⊆ (Base‘𝑃)) |
78 | | eqid 2794 |
. . . . . . . . . . . . . 14
⊢
(mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))) =
(mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))) |
79 | 56, 78 | submrc 16728 |
. . . . . . . . . . . . 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 𝑉))) |
80 | 73, 60, 77, 79 | syl3anc 1364 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))‘(ran
(algSc‘(𝐼 mPwSer
𝑅)) ∪ ran 𝑉)) =
((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))) |
81 | 70, 80 | eqtr2d 2831 |
. . . . . . . . . . 11
⊢ (𝜑 →
((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)) = ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉))) |
82 | 58, 59, 81 | 3eqtr3d 2838 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑃) =
((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉))) |
83 | 82 | ad2antrr 722 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (Base‘𝑃) = ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉))) |
84 | 11, 27, 29 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ Ring) |
85 | 2 | subrgmre 19249 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring →
(SubRing‘𝑃) ∈
(Moore‘(Base‘𝑃))) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (SubRing‘𝑃) ∈
(Moore‘(Base‘𝑃))) |
87 | 86 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (SubRing‘𝑃) ∈ (Moore‘(Base‘𝑃))) |
88 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) |
89 | | rhmeql 19255 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆)) → dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃)) |
90 | 89 | ad2antlr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃)) |
91 | | eqid 2794 |
. . . . . . . . . . 11
⊢
(mrCls‘(SubRing‘𝑃)) = (mrCls‘(SubRing‘𝑃)) |
92 | 91 | mrcsscl 16720 |
. . . . . . . . . 10
⊢
(((SubRing‘𝑃)
∈ (Moore‘(Base‘𝑃)) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛) ∧ dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃)) → ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) ⊆ dom (𝑚 ∩ 𝑛)) |
93 | 87, 88, 90, 92 | syl3anc 1364 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) ⊆ dom (𝑚 ∩ 𝑛)) |
94 | 83, 93 | eqsstrd 3928 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛)) |
95 | 94 | ex 413 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛) → (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛))) |
96 | | simprl 767 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑚 ∈ (𝑃 RingHom 𝑆)) |
97 | 2, 3 | rhmf 19168 |
. . . . . . . . 9
⊢ (𝑚 ∈ (𝑃 RingHom 𝑆) → 𝑚:(Base‘𝑃)⟶𝐶) |
98 | | ffn 6385 |
. . . . . . . . 9
⊢ (𝑚:(Base‘𝑃)⟶𝐶 → 𝑚 Fn (Base‘𝑃)) |
99 | 96, 97, 98 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑚 Fn (Base‘𝑃)) |
100 | | simprr 769 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑛 ∈ (𝑃 RingHom 𝑆)) |
101 | 2, 3 | rhmf 19168 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑃 RingHom 𝑆) → 𝑛:(Base‘𝑃)⟶𝐶) |
102 | | ffn 6385 |
. . . . . . . . 9
⊢ (𝑛:(Base‘𝑃)⟶𝐶 → 𝑛 Fn (Base‘𝑃)) |
103 | 100, 101,
102 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑛 Fn (Base‘𝑃)) |
104 | 74 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ran 𝐴 ⊆ (Base‘𝑃)) |
105 | 76 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ran 𝑉 ⊆ (Base‘𝑃)) |
106 | 104, 105 | unssd 4085 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (ran 𝐴 ∪ ran 𝑉) ⊆ (Base‘𝑃)) |
107 | | fnreseql 6686 |
. . . . . . . 8
⊢ ((𝑚 Fn (Base‘𝑃) ∧ 𝑛 Fn (Base‘𝑃) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ (Base‘𝑃)) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) ↔ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛))) |
108 | 99, 103, 106, 107 | syl3anc 1364 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) ↔ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛))) |
109 | | fneqeql2 6685 |
. . . . . . . 8
⊢ ((𝑚 Fn (Base‘𝑃) ∧ 𝑛 Fn (Base‘𝑃)) → (𝑚 = 𝑛 ↔ (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛))) |
110 | 99, 103, 109 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (𝑚 = 𝑛 ↔ (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛))) |
111 | 95, 108, 110 | 3imtr4d 295 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) → 𝑚 = 𝑛)) |
112 | 48, 111 | syl5 34 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛)) |
113 | 112 | ralrimivva 3157 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ (𝑃 RingHom 𝑆)∀𝑛 ∈ (𝑃 RingHom 𝑆)(((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛)) |
114 | | reseq1 5731 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉))) |
115 | 114 | eqeq1d 2796 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ↔ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))) |
116 | 115 | rmo4 3656 |
. . . 4
⊢
(∃*𝑚 ∈
(𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ↔ ∀𝑚 ∈ (𝑃 RingHom 𝑆)∀𝑛 ∈ (𝑃 RingHom 𝑆)(((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛)) |
117 | 113, 116 | sylibr 235 |
. . 3
⊢ (𝜑 → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) |
118 | | rmoim 3666 |
. . 3
⊢
(∀𝑚 ∈
(𝑃 RingHom 𝑆)(((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → (∃*𝑚 ∈ (𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))) |
119 | 47, 117, 118 | sylc 65 |
. 2
⊢ (𝜑 → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |
120 | | reu5 3389 |
. 2
⊢
(∃!𝑚 ∈
(𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ↔ (∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ∧ ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))) |
121 | 25, 119, 120 | sylanbrc 583 |
1
⊢ (𝜑 → ∃!𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |