Metamath Proof Explorer

Theorem aspval

Description: Value of the algebraic closure operation inside an associative algebra. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses aspval.a ⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
aspval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
aspval.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion aspval ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } )

Proof

Step Hyp Ref Expression
1 aspval.a ⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
2 aspval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 aspval.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
4 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
5 4 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
6 5 pweqd ⊢ ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 𝑉 )
7 fveq2 ⊢ ( 𝑤 = 𝑊 → ( SubRing ‘ 𝑤 ) = ( SubRing ‘ 𝑊 ) )
8 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = ( LSubSp ‘ 𝑊 ) )
9 8 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = 𝐿 )
10 7 9 ineq12d ⊢ ( 𝑤 = 𝑊 → ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) = ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) )
11 10 rabeqdv ⊢ ( 𝑤 = 𝑊 → { 𝑡 ∈ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) ∣ 𝑠 ⊆ 𝑡 } = { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } )
12 11 inteqd ⊢ ( 𝑤 = 𝑊 → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) ∣ 𝑠 ⊆ 𝑡 } = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } )
13 6 12 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) ∣ 𝑠 ⊆ 𝑡 } ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } ) )
14 df-asp ⊢ AlgSpan = ( 𝑤 ∈ AssAlg ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑤 ) ∩ ( LSubSp ‘ 𝑤 ) ) ∣ 𝑠 ⊆ 𝑡 } ) )
15 2 fvexi ⊢ 𝑉 ∈ V
16 15 pwex ⊢ 𝒫 𝑉 ∈ V
17 16 mptex ⊢ ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } ) ∈ V
18 13 14 17 fvmpt ⊢ ( 𝑊 ∈ AssAlg → ( AlgSpan ‘ 𝑊 ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } ) )
19 1 18 eqtrid ⊢ ( 𝑊 ∈ AssAlg → 𝐴 = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } ) )
20 19 fveq1d ⊢ ( 𝑊 ∈ AssAlg → ( 𝐴 ‘ 𝑆 ) = ( ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } ) ‘ 𝑆 ) )
21 20 adantr ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ( ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } ) ‘ 𝑆 ) )
22 eqid ⊢ ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } )
23 sseq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ⊆ 𝑡 ↔ 𝑆 ⊆ 𝑡 ) )
24 23 rabbidv ⊢ ( 𝑠 = 𝑆 → { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } = { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } )
25 24 inteqd ⊢ ( 𝑠 = 𝑆 → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } )
26 simpr ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ 𝑉 )
27 15 elpw2 ⊢ ( 𝑆 ∈ 𝒫 𝑉 ↔ 𝑆 ⊆ 𝑉 )
28 26 27 sylibr ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ∈ 𝒫 𝑉 )
29 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
30 2 subrgid ⊢ ( 𝑊 ∈ Ring → 𝑉 ∈ ( SubRing ‘ 𝑊 ) )
31 29 30 syl ⊢ ( 𝑊 ∈ AssAlg → 𝑉 ∈ ( SubRing ‘ 𝑊 ) )
32 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
33 2 3 lss1 ⊢ ( 𝑊 ∈ LMod → 𝑉 ∈ 𝐿 )
34 32 33 syl ⊢ ( 𝑊 ∈ AssAlg → 𝑉 ∈ 𝐿 )
35 31 34 elind ⊢ ( 𝑊 ∈ AssAlg → 𝑉 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) )
36 sseq2 ⊢ ( 𝑡 = 𝑉 → ( 𝑆 ⊆ 𝑡 ↔ 𝑆 ⊆ 𝑉 ) )
37 36 rspcev ⊢ ( ( 𝑉 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∧ 𝑆 ⊆ 𝑉 ) → ∃ 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) 𝑆 ⊆ 𝑡 )
38 35 37 sylan ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ∃ 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) 𝑆 ⊆ 𝑡 )
39 intexrab ⊢ ( ∃ 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) 𝑆 ⊆ 𝑡 ↔ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ∈ V )
40 38 39 sylib ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } ∈ V )
41 22 25 28 40 fvmptd3 ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( ( 𝑠 ∈ 𝒫 𝑉 ↦ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑠 ⊆ 𝑡 } ) ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } )
42 21 41 eqtrd ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } )