Step | Hyp | Ref
| Expression |
1 | | evlseu.p |
. . . 4
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
2 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝑃) |
3 | | evlseu.c |
. . . 4
⊢ 𝐶 = (Base‘𝑆) |
4 | | eqid 2610 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
5 | | eqid 2610 |
. . . 4
⊢ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} = {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈
Fin} |
6 | | eqid 2610 |
. . . 4
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
7 | | eqid 2610 |
. . . 4
⊢
(.g‘(mulGrp‘𝑆)) =
(.g‘(mulGrp‘𝑆)) |
8 | | eqid 2610 |
. . . 4
⊢
(.r‘𝑆) = (.r‘𝑆) |
9 | | evlseu.v |
. . . 4
⊢ 𝑉 = (𝐼 mVar 𝑅) |
10 | | eqid 2610 |
. . . 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 19336 |
. . 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 5201 |
. . . . . . 7
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) → (𝑚 ∘ 𝐴) = ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴)) |
19 | 18 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) → ((𝑚 ∘ 𝐴) = 𝐹 ↔ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹)) |
20 | | coeq1 5201 |
. . . . . . 7
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) → (𝑚 ∘ 𝑉) = ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉)) |
21 | 20 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) → ((𝑚 ∘ 𝑉) = 𝐺 ↔ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘𝑓
(.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺)) |
22 | 19, 21 | anbi12d 743 |
. . . . 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 3282 |
. . . 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 1252 |
. . 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 18381 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
27 | 12, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
28 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
29 | 1 | mplring 19273 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) |
30 | 1 | mpllmod 19272 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod) |
31 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
32 | 16, 28, 29, 30, 31, 2 | asclf 19158 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝐴:(Base‘(Scalar‘𝑃))⟶(Base‘𝑃)) |
33 | 11, 27, 32 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:(Base‘(Scalar‘𝑃))⟶(Base‘𝑃)) |
34 | | ffun 5961 |
. . . . . . . . 9
⊢ (𝐴:(Base‘(Scalar‘𝑃))⟶(Base‘𝑃) → Fun 𝐴) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐴) |
36 | | funcoeqres 6080 |
. . . . . . . 8
⊢ ((Fun
𝐴 ∧ (𝑚 ∘ 𝐴) = 𝐹) → (𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴)) |
37 | 35, 36 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∘ 𝐴) = 𝐹) → (𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴)) |
38 | 1, 9, 2, 11, 27 | mvrf2 19313 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑃)) |
39 | | ffun 5961 |
. . . . . . . . 9
⊢ (𝑉:𝐼⟶(Base‘𝑃) → Fun 𝑉) |
40 | 38, 39 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝑉) |
41 | | funcoeqres 6080 |
. . . . . . . 8
⊢ ((Fun
𝑉 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) |
42 | 40, 41 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) |
43 | 37, 42 | anim12dan 878 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) → ((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉))) |
44 | 43 | ex 449 |
. . . . 5
⊢ (𝜑 → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → ((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)))) |
45 | | resundi 5330 |
. . . . . 6
⊢ (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝑚 ↾ ran 𝐴) ∪ (𝑚 ↾ ran 𝑉)) |
46 | | uneq12 3724 |
. . . . . 6
⊢ (((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) → ((𝑚 ↾ ran 𝐴) ∪ (𝑚 ↾ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) |
47 | 45, 46 | syl5eq 2656 |
. . . . 5
⊢ (((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) |
48 | 44, 47 | syl6 34 |
. . . 4
⊢ (𝜑 → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))) |
49 | 48 | ralrimivw 2950 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ (𝑃 RingHom 𝑆)(((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))) |
50 | | eqtr3 2631 |
. . . . . 6
⊢ (((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉))) |
51 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
52 | 51, 11, 12 | psrassa 19235 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ AssAlg) |
53 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
54 | 51, 9, 53, 11, 27 | mvrf 19245 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘(𝐼 mPwSer 𝑅))) |
55 | | frn 5966 |
. . . . . . . . . . . . 13
⊢ (𝑉:𝐼⟶(Base‘(𝐼 mPwSer 𝑅)) → ran 𝑉 ⊆ (Base‘(𝐼 mPwSer 𝑅))) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘(𝐼 mPwSer 𝑅))) |
57 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(AlgSpan‘(𝐼
mPwSer 𝑅)) =
(AlgSpan‘(𝐼 mPwSer
𝑅)) |
58 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(algSc‘(𝐼
mPwSer 𝑅)) =
(algSc‘(𝐼 mPwSer
𝑅)) |
59 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(mrCls‘(SubRing‘(𝐼 mPwSer 𝑅))) = (mrCls‘(SubRing‘(𝐼 mPwSer 𝑅))) |
60 | 57, 58, 59, 53 | aspval2 19168 |
. . . . . . . . . . . 12
⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘(𝐼 mPwSer 𝑅))) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))) |
61 | 52, 56, 60 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))) |
62 | 1, 51, 9, 57, 11, 12 | mplbas2 19291 |
. . . . . . . . . . 11
⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = (Base‘𝑃)) |
63 | 51, 1, 2, 11, 27 | mplsubrg 19261 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (Base‘𝑃) ∈ (SubRing‘(𝐼 mPwSer 𝑅))) |
64 | 1, 51, 2 | mplval2 19252 |
. . . . . . . . . . . . . . . 16
⊢ 𝑃 = ((𝐼 mPwSer 𝑅) ↾s (Base‘𝑃)) |
65 | 64 | subsubrg2 18630 |
. . . . . . . . . . . . . . 15
⊢
((Base‘𝑃)
∈ (SubRing‘(𝐼
mPwSer 𝑅)) →
(SubRing‘𝑃) =
((SubRing‘(𝐼 mPwSer
𝑅)) ∩ 𝒫
(Base‘𝑃))) |
66 | 63, 65 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (SubRing‘𝑃) = ((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))) |
67 | 66 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(mrCls‘(SubRing‘𝑃)) = (mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))) |
68 | 58, 64 | ressascl 19165 |
. . . . . . . . . . . . . . . . 17
⊢
((Base‘𝑃)
∈ (SubRing‘(𝐼
mPwSer 𝑅)) →
(algSc‘(𝐼 mPwSer
𝑅)) = (algSc‘𝑃)) |
69 | 63, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (algSc‘(𝐼 mPwSer 𝑅)) = (algSc‘𝑃)) |
70 | 69, 16 | syl6reqr 2663 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 = (algSc‘(𝐼 mPwSer 𝑅))) |
71 | 70 | rneqd 5274 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝐴 = ran (algSc‘(𝐼 mPwSer 𝑅))) |
72 | 71 | uneq1d 3728 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran 𝐴 ∪ ran 𝑉) = (ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)) |
73 | 67, 72 | fveq12d 6109 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) = ((mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))‘(ran
(algSc‘(𝐼 mPwSer
𝑅)) ∪ ran 𝑉))) |
74 | | assaring 19141 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 mPwSer 𝑅) ∈ AssAlg → (𝐼 mPwSer 𝑅) ∈ Ring) |
75 | 53 | subrgmre 18627 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 mPwSer 𝑅) ∈ Ring → (SubRing‘(𝐼 mPwSer 𝑅)) ∈ (Moore‘(Base‘(𝐼 mPwSer 𝑅)))) |
76 | 52, 74, 75 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (SubRing‘(𝐼 mPwSer 𝑅)) ∈ (Moore‘(Base‘(𝐼 mPwSer 𝑅)))) |
77 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴:(Base‘(Scalar‘𝑃))⟶(Base‘𝑃) → ran 𝐴 ⊆ (Base‘𝑃)) |
78 | 33, 77 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐴 ⊆ (Base‘𝑃)) |
79 | 71, 78 | eqsstr3d 3603 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran (algSc‘(𝐼 mPwSer 𝑅)) ⊆ (Base‘𝑃)) |
80 | | frn 5966 |
. . . . . . . . . . . . . . 15
⊢ (𝑉:𝐼⟶(Base‘𝑃) → ran 𝑉 ⊆ (Base‘𝑃)) |
81 | 38, 80 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑃)) |
82 | 79, 81 | unssd 3751 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉) ⊆ (Base‘𝑃)) |
83 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))) =
(mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))) |
84 | 59, 83 | submrc 16111 |
. . . . . . . . . . . . 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 𝑉))) |
85 | 76, 63, 82, 84 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))‘(ran
(algSc‘(𝐼 mPwSer
𝑅)) ∪ ran 𝑉)) =
((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))) |
86 | 73, 85 | eqtr2d 2645 |
. . . . . . . . . . 11
⊢ (𝜑 →
((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)) = ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉))) |
87 | 61, 62, 86 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑃) =
((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉))) |
88 | 87 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (Base‘𝑃) = ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉))) |
89 | 11, 27, 29 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ Ring) |
90 | 2 | subrgmre 18627 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring →
(SubRing‘𝑃) ∈
(Moore‘(Base‘𝑃))) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (SubRing‘𝑃) ∈
(Moore‘(Base‘𝑃))) |
92 | 91 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (SubRing‘𝑃) ∈ (Moore‘(Base‘𝑃))) |
93 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) |
94 | | rhmeql 18633 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆)) → dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃)) |
95 | 94 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃)) |
96 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(mrCls‘(SubRing‘𝑃)) = (mrCls‘(SubRing‘𝑃)) |
97 | 96 | mrcsscl 16103 |
. . . . . . . . . 10
⊢
(((SubRing‘𝑃)
∈ (Moore‘(Base‘𝑃)) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛) ∧ dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃)) → ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) ⊆ dom (𝑚 ∩ 𝑛)) |
98 | 92, 93, 95, 97 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) ⊆ dom (𝑚 ∩ 𝑛)) |
99 | 88, 98 | eqsstrd 3602 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛)) |
100 | 99 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛) → (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛))) |
101 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑚 ∈ (𝑃 RingHom 𝑆)) |
102 | 2, 3 | rhmf 18549 |
. . . . . . . . 9
⊢ (𝑚 ∈ (𝑃 RingHom 𝑆) → 𝑚:(Base‘𝑃)⟶𝐶) |
103 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑚:(Base‘𝑃)⟶𝐶 → 𝑚 Fn (Base‘𝑃)) |
104 | 101, 102,
103 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑚 Fn (Base‘𝑃)) |
105 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑛 ∈ (𝑃 RingHom 𝑆)) |
106 | 2, 3 | rhmf 18549 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑃 RingHom 𝑆) → 𝑛:(Base‘𝑃)⟶𝐶) |
107 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑛:(Base‘𝑃)⟶𝐶 → 𝑛 Fn (Base‘𝑃)) |
108 | 105, 106,
107 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑛 Fn (Base‘𝑃)) |
109 | 78 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ran 𝐴 ⊆ (Base‘𝑃)) |
110 | 81 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ran 𝑉 ⊆ (Base‘𝑃)) |
111 | 109, 110 | unssd 3751 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (ran 𝐴 ∪ ran 𝑉) ⊆ (Base‘𝑃)) |
112 | | fnreseql 6235 |
. . . . . . . 8
⊢ ((𝑚 Fn (Base‘𝑃) ∧ 𝑛 Fn (Base‘𝑃) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ (Base‘𝑃)) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) ↔ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛))) |
113 | 104, 108,
111, 112 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) ↔ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛))) |
114 | | fneqeql2 6234 |
. . . . . . . 8
⊢ ((𝑚 Fn (Base‘𝑃) ∧ 𝑛 Fn (Base‘𝑃)) → (𝑚 = 𝑛 ↔ (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛))) |
115 | 104, 108,
114 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (𝑚 = 𝑛 ↔ (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛))) |
116 | 100, 113,
115 | 3imtr4d 282 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) → 𝑚 = 𝑛)) |
117 | 50, 116 | syl5 33 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛)) |
118 | 117 | ralrimivva 2954 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ (𝑃 RingHom 𝑆)∀𝑛 ∈ (𝑃 RingHom 𝑆)(((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛)) |
119 | | reseq1 5311 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉))) |
120 | 119 | eqeq1d 2612 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ↔ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))) |
121 | 120 | rmo4 3366 |
. . . 4
⊢
(∃*𝑚 ∈
(𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ↔ ∀𝑚 ∈ (𝑃 RingHom 𝑆)∀𝑛 ∈ (𝑃 RingHom 𝑆)(((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛)) |
122 | 118, 121 | sylibr 223 |
. . 3
⊢ (𝜑 → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) |
123 | | rmoim 3374 |
. . 3
⊢
(∀𝑚 ∈
(𝑃 RingHom 𝑆)(((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → (∃*𝑚 ∈ (𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))) |
124 | 49, 122, 123 | sylc 63 |
. 2
⊢ (𝜑 → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |
125 | | reu5 3136 |
. 2
⊢
(∃!𝑚 ∈
(𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ↔ (∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ∧ ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))) |
126 | 25, 124, 125 | sylanbrc 695 |
1
⊢ (𝜑 → ∃!𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) |