Step | Hyp | Ref
| Expression |
1 | | eqidd 2739 |
. 2
⊢ (𝜑 → (Scalar‘𝐵) = (Scalar‘𝐵)) |
2 | | eqidd 2739 |
. 2
⊢ (𝜑 →
(Base‘(Scalar‘𝐵)) = (Base‘(Scalar‘𝐵))) |
3 | | eqidd 2739 |
. 2
⊢ (𝜑 → (Base‘𝐵) = (Base‘𝐵)) |
4 | | eqidd 2739 |
. 2
⊢ (𝜑 → (+g‘𝐵) = (+g‘𝐵)) |
5 | | eqidd 2739 |
. 2
⊢ (𝜑 → (
·𝑠 ‘𝐵) = ( ·𝑠
‘𝐵)) |
6 | | eqidd 2739 |
. 2
⊢ (𝜑 → (LSubSp‘𝐵) = (LSubSp‘𝐵)) |
7 | | drgext.2 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) |
8 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝐸) =
(Base‘𝐸) |
9 | 8 | subrgss 20025 |
. . . 4
⊢ (𝑈 ∈ (SubRing‘𝐸) → 𝑈 ⊆ (Base‘𝐸)) |
10 | 7, 9 | syl 17 |
. . 3
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐸)) |
11 | | drgext.b |
. . . . 5
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) |
12 | 11 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐵 = ((subringAlg ‘𝐸)‘𝑈)) |
13 | 12, 10 | srabase 20441 |
. . 3
⊢ (𝜑 → (Base‘𝐸) = (Base‘𝐵)) |
14 | 10, 13 | sseqtrd 3961 |
. 2
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝐵)) |
15 | | eqid 2738 |
. . . 4
⊢
(1r‘𝐸) = (1r‘𝐸) |
16 | 15 | subrg1cl 20032 |
. . 3
⊢ (𝑈 ∈ (SubRing‘𝐸) →
(1r‘𝐸)
∈ 𝑈) |
17 | | ne0i 4268 |
. . 3
⊢
((1r‘𝐸) ∈ 𝑈 → 𝑈 ≠ ∅) |
18 | 7, 16, 17 | 3syl 18 |
. 2
⊢ (𝜑 → 𝑈 ≠ ∅) |
19 | | drgext.3 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ DivRing) |
20 | | drnggrp 19999 |
. . . . . 6
⊢ (𝐹 ∈ DivRing → 𝐹 ∈ Grp) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ Grp) |
22 | 21 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝐹 ∈ Grp) |
23 | 12, 10 | sravsca 20449 |
. . . . . . 7
⊢ (𝜑 → (.r‘𝐸) = (
·𝑠 ‘𝐵)) |
24 | | drgext.f |
. . . . . . . . 9
⊢ 𝐹 = (𝐸 ↾s 𝑈) |
25 | | eqid 2738 |
. . . . . . . . 9
⊢
(.r‘𝐸) = (.r‘𝐸) |
26 | 24, 25 | ressmulr 17017 |
. . . . . . . 8
⊢ (𝑈 ∈ (SubRing‘𝐸) →
(.r‘𝐸) =
(.r‘𝐹)) |
27 | 7, 26 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (.r‘𝐸) = (.r‘𝐹)) |
28 | 23, 27 | eqtr3d 2780 |
. . . . . 6
⊢ (𝜑 → (
·𝑠 ‘𝐵) = (.r‘𝐹)) |
29 | 28 | oveqdr 7303 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑥( ·𝑠
‘𝐵)𝑎) = (𝑥(.r‘𝐹)𝑎)) |
30 | | drngring 19998 |
. . . . . . . 8
⊢ (𝐹 ∈ DivRing → 𝐹 ∈ Ring) |
31 | 19, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ Ring) |
32 | 31 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝐹 ∈ Ring) |
33 | | simpr1 1193 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝐵))) |
34 | 12, 10 | srasca 20447 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 ↾s 𝑈) = (Scalar‘𝐵)) |
35 | 24, 34 | eqtrid 2790 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (Scalar‘𝐵)) |
36 | 35 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐹) =
(Base‘(Scalar‘𝐵))) |
37 | 36 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (Base‘𝐹) = (Base‘(Scalar‘𝐵))) |
38 | 33, 37 | eleqtrrd 2842 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑥 ∈ (Base‘𝐹)) |
39 | | simpr2 1194 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑎 ∈ 𝑈) |
40 | 24, 8 | ressbas2 16949 |
. . . . . . . . 9
⊢ (𝑈 ⊆ (Base‘𝐸) → 𝑈 = (Base‘𝐹)) |
41 | 10, 40 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 = (Base‘𝐹)) |
42 | 41 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑈 = (Base‘𝐹)) |
43 | 39, 42 | eleqtrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑎 ∈ (Base‘𝐹)) |
44 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐹) =
(Base‘𝐹) |
45 | | eqid 2738 |
. . . . . . 7
⊢
(.r‘𝐹) = (.r‘𝐹) |
46 | 44, 45 | ringcl 19800 |
. . . . . 6
⊢ ((𝐹 ∈ Ring ∧ 𝑥 ∈ (Base‘𝐹) ∧ 𝑎 ∈ (Base‘𝐹)) → (𝑥(.r‘𝐹)𝑎) ∈ (Base‘𝐹)) |
47 | 32, 38, 43, 46 | syl3anc 1370 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑥(.r‘𝐹)𝑎) ∈ (Base‘𝐹)) |
48 | 29, 47 | eqeltrd 2839 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑥( ·𝑠
‘𝐵)𝑎) ∈ (Base‘𝐹)) |
49 | | simpr3 1195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑏 ∈ 𝑈) |
50 | 49, 42 | eleqtrd 2841 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑏 ∈ (Base‘𝐹)) |
51 | | eqid 2738 |
. . . . 5
⊢
(+g‘𝐹) = (+g‘𝐹) |
52 | 44, 51 | grpcl 18585 |
. . . 4
⊢ ((𝐹 ∈ Grp ∧ (𝑥(
·𝑠 ‘𝐵)𝑎) ∈ (Base‘𝐹) ∧ 𝑏 ∈ (Base‘𝐹)) → ((𝑥( ·𝑠
‘𝐵)𝑎)(+g‘𝐹)𝑏) ∈ (Base‘𝐹)) |
53 | 22, 48, 50, 52 | syl3anc 1370 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → ((𝑥( ·𝑠
‘𝐵)𝑎)(+g‘𝐹)𝑏) ∈ (Base‘𝐹)) |
54 | 12, 10 | sraaddg 20443 |
. . . . . 6
⊢ (𝜑 → (+g‘𝐸) = (+g‘𝐵)) |
55 | | eqid 2738 |
. . . . . . . 8
⊢
(+g‘𝐸) = (+g‘𝐸) |
56 | 24, 55 | ressplusg 17000 |
. . . . . . 7
⊢ (𝑈 ∈ (SubRing‘𝐸) →
(+g‘𝐸) =
(+g‘𝐹)) |
57 | 7, 56 | syl 17 |
. . . . . 6
⊢ (𝜑 → (+g‘𝐸) = (+g‘𝐹)) |
58 | 54, 57 | eqtr3d 2780 |
. . . . 5
⊢ (𝜑 → (+g‘𝐵) = (+g‘𝐹)) |
59 | 58 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (+g‘𝐵) = (+g‘𝐹)) |
60 | 59 | oveqd 7292 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → ((𝑥( ·𝑠
‘𝐵)𝑎)(+g‘𝐵)𝑏) = ((𝑥( ·𝑠
‘𝐵)𝑎)(+g‘𝐹)𝑏)) |
61 | 53, 60, 42 | 3eltr4d 2854 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐵)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → ((𝑥( ·𝑠
‘𝐵)𝑎)(+g‘𝐵)𝑏) ∈ 𝑈) |
62 | 1, 2, 3, 4, 5, 6, 14, 18, 61 | islssd 20197 |
1
⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐵)) |