Proof of Theorem subsubrg
Step | Hyp | Ref
| Expression |
1 | | subrgrcl 18608 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → 𝑅 ∈ Ring) |
3 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑆) =
(Base‘𝑆) |
4 | 3 | subrgss 18604 |
. . . . . . . . 9
⊢ (𝐵 ∈ (SubRing‘𝑆) → 𝐵 ⊆ (Base‘𝑆)) |
5 | 4 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → 𝐵 ⊆ (Base‘𝑆)) |
6 | | subsubrg.s |
. . . . . . . . . 10
⊢ 𝑆 = (𝑅 ↾s 𝐴) |
7 | 6 | subrgbas 18612 |
. . . . . . . . 9
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) |
8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → 𝐴 = (Base‘𝑆)) |
9 | 5, 8 | sseqtr4d 3605 |
. . . . . . 7
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → 𝐵 ⊆ 𝐴) |
10 | 6 | oveq1i 6559 |
. . . . . . . 8
⊢ (𝑆 ↾s 𝐵) = ((𝑅 ↾s 𝐴) ↾s 𝐵) |
11 | | ressabs 15766 |
. . . . . . . 8
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴) → ((𝑅 ↾s 𝐴) ↾s 𝐵) = (𝑅 ↾s 𝐵)) |
12 | 10, 11 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴) → (𝑆 ↾s 𝐵) = (𝑅 ↾s 𝐵)) |
13 | 9, 12 | syldan 486 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → (𝑆 ↾s 𝐵) = (𝑅 ↾s 𝐵)) |
14 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑆 ↾s 𝐵) = (𝑆 ↾s 𝐵) |
15 | 14 | subrgring 18606 |
. . . . . . 7
⊢ (𝐵 ∈ (SubRing‘𝑆) → (𝑆 ↾s 𝐵) ∈ Ring) |
16 | 15 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → (𝑆 ↾s 𝐵) ∈ Ring) |
17 | 13, 16 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → (𝑅 ↾s 𝐵) ∈ Ring) |
18 | 2, 17 | jca 553 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → (𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐵) ∈ Ring)) |
19 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
20 | 19 | subrgss 18604 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
21 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → 𝐴 ⊆ (Base‘𝑅)) |
22 | 9, 21 | sstrd 3578 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → 𝐵 ⊆ (Base‘𝑅)) |
23 | | eqid 2610 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
24 | 6, 23 | subrg1 18613 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(1r‘𝑅) =
(1r‘𝑆)) |
25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → (1r‘𝑅) = (1r‘𝑆)) |
26 | | eqid 2610 |
. . . . . . . 8
⊢
(1r‘𝑆) = (1r‘𝑆) |
27 | 26 | subrg1cl 18611 |
. . . . . . 7
⊢ (𝐵 ∈ (SubRing‘𝑆) →
(1r‘𝑆)
∈ 𝐵) |
28 | 27 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → (1r‘𝑆) ∈ 𝐵) |
29 | 25, 28 | eqeltrd 2688 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → (1r‘𝑅) ∈ 𝐵) |
30 | 22, 29 | jca 553 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → (𝐵 ⊆ (Base‘𝑅) ∧ (1r‘𝑅) ∈ 𝐵)) |
31 | 19, 23 | issubrg 18603 |
. . . 4
⊢ (𝐵 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐵) ∈ Ring) ∧ (𝐵 ⊆ (Base‘𝑅) ∧ (1r‘𝑅) ∈ 𝐵))) |
32 | 18, 30, 31 | sylanbrc 695 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → 𝐵 ∈ (SubRing‘𝑅)) |
33 | 32, 9 | jca 553 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐵 ∈ (SubRing‘𝑆)) → (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) |
34 | 6 | subrgring 18606 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring) |
35 | 34 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → 𝑆 ∈ Ring) |
36 | 12 | adantrl 748 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → (𝑆 ↾s 𝐵) = (𝑅 ↾s 𝐵)) |
37 | | eqid 2610 |
. . . . . . 7
⊢ (𝑅 ↾s 𝐵) = (𝑅 ↾s 𝐵) |
38 | 37 | subrgring 18606 |
. . . . . 6
⊢ (𝐵 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝐵) ∈ Ring) |
39 | 38 | ad2antrl 760 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → (𝑅 ↾s 𝐵) ∈ Ring) |
40 | 36, 39 | eqeltrd 2688 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → (𝑆 ↾s 𝐵) ∈ Ring) |
41 | 35, 40 | jca 553 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → (𝑆 ∈ Ring ∧ (𝑆 ↾s 𝐵) ∈ Ring)) |
42 | | simprr 792 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ⊆ 𝐴) |
43 | 7 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → 𝐴 = (Base‘𝑆)) |
44 | 42, 43 | sseqtrd 3604 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ⊆ (Base‘𝑆)) |
45 | 24 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → (1r‘𝑅) = (1r‘𝑆)) |
46 | 23 | subrg1cl 18611 |
. . . . . 6
⊢ (𝐵 ∈ (SubRing‘𝑅) →
(1r‘𝑅)
∈ 𝐵) |
47 | 46 | ad2antrl 760 |
. . . . 5
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → (1r‘𝑅) ∈ 𝐵) |
48 | 45, 47 | eqeltrrd 2689 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → (1r‘𝑆) ∈ 𝐵) |
49 | 44, 48 | jca 553 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → (𝐵 ⊆ (Base‘𝑆) ∧ (1r‘𝑆) ∈ 𝐵)) |
50 | 3, 26 | issubrg 18603 |
. . 3
⊢ (𝐵 ∈ (SubRing‘𝑆) ↔ ((𝑆 ∈ Ring ∧ (𝑆 ↾s 𝐵) ∈ Ring) ∧ (𝐵 ⊆ (Base‘𝑆) ∧ (1r‘𝑆) ∈ 𝐵))) |
51 | 41, 49, 50 | sylanbrc 695 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ∈ (SubRing‘𝑆)) |
52 | 33, 51 | impbida 873 |
1
⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐵 ∈ (SubRing‘𝑆) ↔ (𝐵 ∈ (SubRing‘𝑅) ∧ 𝐵 ⊆ 𝐴))) |