Step | Hyp | Ref
| Expression |
1 | | aspval.a |
. . . . 5
β’ π΄ = (AlgSpanβπ) |
2 | | fveq2 6847 |
. . . . . . . . 9
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
3 | | aspval.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
4 | 2, 3 | eqtr4di 2795 |
. . . . . . . 8
β’ (π€ = π β (Baseβπ€) = π) |
5 | 4 | pweqd 4582 |
. . . . . . 7
β’ (π€ = π β π« (Baseβπ€) = π« π) |
6 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π€ = π β (SubRingβπ€) = (SubRingβπ)) |
7 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π€ = π β (LSubSpβπ€) = (LSubSpβπ)) |
8 | | aspval.l |
. . . . . . . . . . 11
β’ πΏ = (LSubSpβπ) |
9 | 7, 8 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π€ = π β (LSubSpβπ€) = πΏ) |
10 | 6, 9 | ineq12d 4178 |
. . . . . . . . 9
β’ (π€ = π β ((SubRingβπ€) β© (LSubSpβπ€)) = ((SubRingβπ) β© πΏ)) |
11 | 10 | rabeqdv 3425 |
. . . . . . . 8
β’ (π€ = π β {π‘ β ((SubRingβπ€) β© (LSubSpβπ€)) β£ π β π‘} = {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘}) |
12 | 11 | inteqd 4917 |
. . . . . . 7
β’ (π€ = π β β© {π‘ β ((SubRingβπ€) β© (LSubSpβπ€)) β£ π β π‘} = β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘}) |
13 | 5, 12 | mpteq12dv 5201 |
. . . . . 6
β’ (π€ = π β (π β π« (Baseβπ€) β¦ β© {π‘
β ((SubRingβπ€)
β© (LSubSpβπ€))
β£ π β π‘}) = (π β π« π β¦ β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘})) |
14 | | df-asp 21276 |
. . . . . 6
β’ AlgSpan =
(π€ β AssAlg β¦
(π β π«
(Baseβπ€) β¦
β© {π‘ β ((SubRingβπ€) β© (LSubSpβπ€)) β£ π β π‘})) |
15 | 3 | fvexi 6861 |
. . . . . . . 8
β’ π β V |
16 | 15 | pwex 5340 |
. . . . . . 7
β’ π«
π β V |
17 | 16 | mptex 7178 |
. . . . . 6
β’ (π β π« π β¦ β© {π‘
β ((SubRingβπ)
β© πΏ) β£ π β π‘}) β V |
18 | 13, 14, 17 | fvmpt 6953 |
. . . . 5
β’ (π β AssAlg β
(AlgSpanβπ) = (π β π« π β¦ β© {π‘
β ((SubRingβπ)
β© πΏ) β£ π β π‘})) |
19 | 1, 18 | eqtrid 2789 |
. . . 4
β’ (π β AssAlg β π΄ = (π β π« π β¦ β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘})) |
20 | 19 | fveq1d 6849 |
. . 3
β’ (π β AssAlg β (π΄βπ) = ((π β π« π β¦ β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘})βπ)) |
21 | 20 | adantr 482 |
. 2
β’ ((π β AssAlg β§ π β π) β (π΄βπ) = ((π β π« π β¦ β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘})βπ)) |
22 | | eqid 2737 |
. . 3
β’ (π β π« π β¦ β© {π‘
β ((SubRingβπ)
β© πΏ) β£ π β π‘}) = (π β π« π β¦ β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘}) |
23 | | sseq1 3974 |
. . . . 5
β’ (π = π β (π β π‘ β π β π‘)) |
24 | 23 | rabbidv 3418 |
. . . 4
β’ (π = π β {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘} = {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘}) |
25 | 24 | inteqd 4917 |
. . 3
β’ (π = π β β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘} = β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘}) |
26 | | simpr 486 |
. . . 4
β’ ((π β AssAlg β§ π β π) β π β π) |
27 | 15 | elpw2 5307 |
. . . 4
β’ (π β π« π β π β π) |
28 | 26, 27 | sylibr 233 |
. . 3
β’ ((π β AssAlg β§ π β π) β π β π« π) |
29 | | assaring 21283 |
. . . . . . 7
β’ (π β AssAlg β π β Ring) |
30 | 3 | subrgid 20240 |
. . . . . . 7
β’ (π β Ring β π β (SubRingβπ)) |
31 | 29, 30 | syl 17 |
. . . . . 6
β’ (π β AssAlg β π β (SubRingβπ)) |
32 | | assalmod 21282 |
. . . . . . 7
β’ (π β AssAlg β π β LMod) |
33 | 3, 8 | lss1 20415 |
. . . . . . 7
β’ (π β LMod β π β πΏ) |
34 | 32, 33 | syl 17 |
. . . . . 6
β’ (π β AssAlg β π β πΏ) |
35 | 31, 34 | elind 4159 |
. . . . 5
β’ (π β AssAlg β π β ((SubRingβπ) β© πΏ)) |
36 | | sseq2 3975 |
. . . . . 6
β’ (π‘ = π β (π β π‘ β π β π)) |
37 | 36 | rspcev 3584 |
. . . . 5
β’ ((π β ((SubRingβπ) β© πΏ) β§ π β π) β βπ‘ β ((SubRingβπ) β© πΏ)π β π‘) |
38 | 35, 37 | sylan 581 |
. . . 4
β’ ((π β AssAlg β§ π β π) β βπ‘ β ((SubRingβπ) β© πΏ)π β π‘) |
39 | | intexrab 5302 |
. . . 4
β’
(βπ‘ β
((SubRingβπ) β©
πΏ)π β π‘ β β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘} β V) |
40 | 38, 39 | sylib 217 |
. . 3
β’ ((π β AssAlg β§ π β π) β β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘} β V) |
41 | 22, 25, 28, 40 | fvmptd3 6976 |
. 2
β’ ((π β AssAlg β§ π β π) β ((π β π« π β¦ β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘})βπ) = β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘}) |
42 | 21, 41 | eqtrd 2777 |
1
β’ ((π β AssAlg β§ π β π) β (π΄βπ) = β© {π‘ β ((SubRingβπ) β© πΏ) β£ π β π‘}) |