Step | Hyp | Ref
| Expression |
1 | | elin 3758 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ↔ (𝑥 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (LSubSp‘𝑊))) |
2 | 1 | anbi1i 727 |
. . . . . . . 8
⊢ ((𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ∧ 𝑆 ⊆ 𝑥) ↔ ((𝑥 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (LSubSp‘𝑊)) ∧ 𝑆 ⊆ 𝑥)) |
3 | | anass 679 |
. . . . . . . 8
⊢ (((𝑥 ∈ (SubRing‘𝑊) ∧ 𝑥 ∈ (LSubSp‘𝑊)) ∧ 𝑆 ⊆ 𝑥) ↔ (𝑥 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (LSubSp‘𝑊) ∧ 𝑆 ⊆ 𝑥))) |
4 | 2, 3 | bitri 263 |
. . . . . . 7
⊢ ((𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ∧ 𝑆 ⊆ 𝑥) ↔ (𝑥 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (LSubSp‘𝑊) ∧ 𝑆 ⊆ 𝑥))) |
5 | | aspval2.c |
. . . . . . . . . . 11
⊢ 𝐶 = (algSc‘𝑊) |
6 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
7 | 5, 6 | issubassa2 19166 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ AssAlg ∧ 𝑥 ∈ (SubRing‘𝑊)) → (𝑥 ∈ (LSubSp‘𝑊) ↔ ran 𝐶 ⊆ 𝑥)) |
8 | 7 | anbi1d 737 |
. . . . . . . . 9
⊢ ((𝑊 ∈ AssAlg ∧ 𝑥 ∈ (SubRing‘𝑊)) → ((𝑥 ∈ (LSubSp‘𝑊) ∧ 𝑆 ⊆ 𝑥) ↔ (ran 𝐶 ⊆ 𝑥 ∧ 𝑆 ⊆ 𝑥))) |
9 | | unss 3749 |
. . . . . . . . 9
⊢ ((ran
𝐶 ⊆ 𝑥 ∧ 𝑆 ⊆ 𝑥) ↔ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥) |
10 | 8, 9 | syl6bb 275 |
. . . . . . . 8
⊢ ((𝑊 ∈ AssAlg ∧ 𝑥 ∈ (SubRing‘𝑊)) → ((𝑥 ∈ (LSubSp‘𝑊) ∧ 𝑆 ⊆ 𝑥) ↔ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥)) |
11 | 10 | pm5.32da 671 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → ((𝑥 ∈ (SubRing‘𝑊) ∧ (𝑥 ∈ (LSubSp‘𝑊) ∧ 𝑆 ⊆ 𝑥)) ↔ (𝑥 ∈ (SubRing‘𝑊) ∧ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥))) |
12 | 4, 11 | syl5bb 271 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → ((𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ∧ 𝑆 ⊆ 𝑥) ↔ (𝑥 ∈ (SubRing‘𝑊) ∧ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥))) |
13 | 12 | abbidv 2728 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → {𝑥 ∣ (𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ∧ 𝑆 ⊆ 𝑥)} = {𝑥 ∣ (𝑥 ∈ (SubRing‘𝑊) ∧ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥)}) |
14 | 13 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → {𝑥 ∣ (𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ∧ 𝑆 ⊆ 𝑥)} = {𝑥 ∣ (𝑥 ∈ (SubRing‘𝑊) ∧ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥)}) |
15 | | df-rab 2905 |
. . . 4
⊢ {𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ∣ 𝑆 ⊆ 𝑥} = {𝑥 ∣ (𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ∧ 𝑆 ⊆ 𝑥)} |
16 | | df-rab 2905 |
. . . 4
⊢ {𝑥 ∈ (SubRing‘𝑊) ∣ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥} = {𝑥 ∣ (𝑥 ∈ (SubRing‘𝑊) ∧ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥)} |
17 | 14, 15, 16 | 3eqtr4g 2669 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → {𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ∣ 𝑆 ⊆ 𝑥} = {𝑥 ∈ (SubRing‘𝑊) ∣ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥}) |
18 | 17 | inteqd 4415 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ∩ {𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ∣ 𝑆 ⊆ 𝑥} = ∩ {𝑥 ∈ (SubRing‘𝑊) ∣ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥}) |
19 | | aspval2.a |
. . 3
⊢ 𝐴 = (AlgSpan‘𝑊) |
20 | | aspval2.v |
. . 3
⊢ 𝑉 = (Base‘𝑊) |
21 | 19, 20, 6 | aspval 19149 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ∩ {𝑥 ∈ ((SubRing‘𝑊) ∩ (LSubSp‘𝑊)) ∣ 𝑆 ⊆ 𝑥}) |
22 | | assaring 19141 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
23 | 20 | subrgmre 18627 |
. . . . 5
⊢ (𝑊 ∈ Ring →
(SubRing‘𝑊) ∈
(Moore‘𝑉)) |
24 | 22, 23 | syl 17 |
. . . 4
⊢ (𝑊 ∈ AssAlg →
(SubRing‘𝑊) ∈
(Moore‘𝑉)) |
25 | 24 | adantr 480 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (SubRing‘𝑊) ∈ (Moore‘𝑉)) |
26 | | eqid 2610 |
. . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
27 | | assalmod 19140 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
28 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
29 | 5, 26, 22, 27, 28, 20 | asclf 19158 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → 𝐶:(Base‘(Scalar‘𝑊))⟶𝑉) |
30 | | frn 5966 |
. . . . . 6
⊢ (𝐶:(Base‘(Scalar‘𝑊))⟶𝑉 → ran 𝐶 ⊆ 𝑉) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → ran 𝐶 ⊆ 𝑉) |
32 | 31 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ran 𝐶 ⊆ 𝑉) |
33 | | simpr 476 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉) |
34 | 32, 33 | unssd 3751 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (ran 𝐶 ∪ 𝑆) ⊆ 𝑉) |
35 | | aspval2.r |
. . . 4
⊢ 𝑅 =
(mrCls‘(SubRing‘𝑊)) |
36 | 35 | mrcval 16093 |
. . 3
⊢
(((SubRing‘𝑊)
∈ (Moore‘𝑉)
∧ (ran 𝐶 ∪ 𝑆) ⊆ 𝑉) → (𝑅‘(ran 𝐶 ∪ 𝑆)) = ∩ {𝑥 ∈ (SubRing‘𝑊) ∣ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥}) |
37 | 25, 34, 36 | syl2anc 691 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝑅‘(ran 𝐶 ∪ 𝑆)) = ∩ {𝑥 ∈ (SubRing‘𝑊) ∣ (ran 𝐶 ∪ 𝑆) ⊆ 𝑥}) |
38 | 18, 21, 37 | 3eqtr4d 2654 |
1
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = (𝑅‘(ran 𝐶 ∪ 𝑆))) |