Step | Hyp | Ref
| Expression |
1 | | subrgpsr.s |
. . . 4
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | simpl 473 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐼 ∈ 𝑉) |
3 | | subrgrcl 18785 |
. . . . 5
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
4 | 3 | adantl 482 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝑅 ∈ Ring) |
5 | 1, 2, 4 | psrring 19411 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝑆 ∈ Ring) |
6 | | subrgpsr.u |
. . . . 5
⊢ 𝑈 = (𝐼 mPwSer 𝐻) |
7 | | subrgpsr.h |
. . . . . . 7
⊢ 𝐻 = (𝑅 ↾s 𝑇) |
8 | 7 | subrgring 18783 |
. . . . . 6
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝐻 ∈ Ring) |
9 | 8 | adantl 482 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐻 ∈ Ring) |
10 | 6, 2, 9 | psrring 19411 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝑈 ∈ Ring) |
11 | | subrgpsr.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑈) |
12 | 11 | a1i 11 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐵 = (Base‘𝑈)) |
13 | | eqid 2622 |
. . . . . 6
⊢ (𝑆 ↾s 𝐵) = (𝑆 ↾s 𝐵) |
14 | | simpr 477 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝑇 ∈ (SubRing‘𝑅)) |
15 | 1, 7, 6, 11, 13, 14 | resspsrbas 19415 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐵 = (Base‘(𝑆 ↾s 𝐵))) |
16 | 1, 7, 6, 11, 13, 14 | resspsradd 19416 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑈)𝑦) = (𝑥(+g‘(𝑆 ↾s 𝐵))𝑦)) |
17 | 1, 7, 6, 11, 13, 14 | resspsrmul 19417 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝑈)𝑦) = (𝑥(.r‘(𝑆 ↾s 𝐵))𝑦)) |
18 | 12, 15, 16, 17 | ringpropd 18582 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → (𝑈 ∈ Ring ↔ (𝑆 ↾s 𝐵) ∈ Ring)) |
19 | 10, 18 | mpbid 222 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → (𝑆 ↾s 𝐵) ∈ Ring) |
20 | 5, 19 | jca 554 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → (𝑆 ∈ Ring ∧ (𝑆 ↾s 𝐵) ∈ Ring)) |
21 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝑆) =
(Base‘𝑆) |
22 | 13, 21 | ressbasss 15932 |
. . . 4
⊢
(Base‘(𝑆
↾s 𝐵))
⊆ (Base‘𝑆) |
23 | 15, 22 | syl6eqss 3655 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐵 ⊆ (Base‘𝑆)) |
24 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) |
25 | 24 | subrg1cl 18788 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ (SubRing‘𝑅) →
(1r‘𝑅)
∈ 𝑇) |
26 | | subrgsubg 18786 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 ∈ (SubGrp‘𝑅)) |
27 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) = (0g‘𝑅) |
28 | 27 | subg0cl 17602 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (SubGrp‘𝑅) →
(0g‘𝑅)
∈ 𝑇) |
29 | 26, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ (SubRing‘𝑅) →
(0g‘𝑅)
∈ 𝑇) |
30 | 25, 29 | ifcld 4131 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) ∈ 𝑇) |
31 | 30 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) ∈ 𝑇) |
32 | 7 | subrgbas 18789 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (SubRing‘𝑅) → 𝑇 = (Base‘𝐻)) |
33 | 32 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝑇 = (Base‘𝐻)) |
34 | 31, 33 | eleqtrd 2703 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) ∈ (Base‘𝐻)) |
35 | 34 | adantr 481 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) ∈ (Base‘𝐻)) |
36 | | eqid 2622 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) = (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) |
37 | 35, 36 | fmptd 6385 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))):{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
38 | | eqid 2622 |
. . . . . . . 8
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
39 | | eqid 2622 |
. . . . . . . 8
⊢
(1r‘𝑆) = (1r‘𝑆) |
40 | 1, 2, 4, 38, 27, 24, 39 | psr1 19412 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → (1r‘𝑆) = (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)))) |
41 | 40 | feq1d 6030 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → ((1r‘𝑆):{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)
↔ (𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))):{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻))) |
42 | 37, 41 | mpbird 247 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → (1r‘𝑆):{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
43 | | fvex 6201 |
. . . . . 6
⊢
(Base‘𝐻)
∈ V |
44 | | ovex 6678 |
. . . . . . 7
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
45 | 44 | rabex 4813 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V |
46 | 43, 45 | elmap 7886 |
. . . . 5
⊢
((1r‘𝑆) ∈ ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ↔
(1r‘𝑆):{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝐻)) |
47 | 42, 46 | sylibr 224 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → (1r‘𝑆) ∈ ((Base‘𝐻) ↑𝑚
{𝑓 ∈
(ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
48 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝐻) =
(Base‘𝐻) |
49 | 6, 48, 38, 11, 2 | psrbas 19378 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐵 = ((Base‘𝐻) ↑𝑚 {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin})) |
50 | 47, 49 | eleqtrrd 2704 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → (1r‘𝑆) ∈ 𝐵) |
51 | 23, 50 | jca 554 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → (𝐵 ⊆ (Base‘𝑆) ∧ (1r‘𝑆) ∈ 𝐵)) |
52 | 21, 39 | issubrg 18780 |
. 2
⊢ (𝐵 ∈ (SubRing‘𝑆) ↔ ((𝑆 ∈ Ring ∧ (𝑆 ↾s 𝐵) ∈ Ring) ∧ (𝐵 ⊆ (Base‘𝑆) ∧ (1r‘𝑆) ∈ 𝐵))) |
53 | 20, 51, 52 | sylanbrc 698 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑇 ∈ (SubRing‘𝑅)) → 𝐵 ∈ (SubRing‘𝑆)) |