| Step | Hyp | Ref
| Expression |
|---|
| 1 | | elin 3963 |
. . . . . . . . 9
β’ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β (π₯ β (SubRingβπ) β§ π₯ β (LSubSpβπ))) |
| 2 | 1 | anbi1i 622 |
. . . . . . . 8
β’ ((π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯) β ((π₯ β (SubRingβπ) β§ π₯ β (LSubSpβπ)) β§ π β π₯)) |
| 3 | | anass 467 |
. . . . . . . 8
β’ (((π₯ β (SubRingβπ) β§ π₯ β (LSubSpβπ)) β§ π β π₯) β (π₯ β (SubRingβπ) β§ (π₯ β (LSubSpβπ) β§ π β π₯))) |
| 4 | 2, 3 | bitri 274 |
. . . . . . 7
β’ ((π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯) β (π₯ β (SubRingβπ) β§ (π₯ β (LSubSpβπ) β§ π β π₯))) |
| 5 | | aspval2.c |
. . . . . . . . . . 11
β’ πΆ = (algScβπ) |
| 6 | | eqid 2730 |
. . . . . . . . . . 11
β’
(LSubSpβπ) =
(LSubSpβπ) |
| 7 | 5, 6 | issubassa2 21665 |
. . . . . . . . . 10
β’ ((π β AssAlg β§ π₯ β (SubRingβπ)) β (π₯ β (LSubSpβπ) β ran πΆ β π₯)) |
| 8 | 7 | anbi1d 628 |
. . . . . . . . 9
β’ ((π β AssAlg β§ π₯ β (SubRingβπ)) β ((π₯ β (LSubSpβπ) β§ π β π₯) β (ran πΆ β π₯ β§ π β π₯))) |
| 9 | | unss 4183 |
. . . . . . . . 9
β’ ((ran
πΆ β π₯ β§ π β π₯) β (ran πΆ βͺ π) β π₯) |
| 10 | 8, 9 | bitrdi 286 |
. . . . . . . 8
β’ ((π β AssAlg β§ π₯ β (SubRingβπ)) β ((π₯ β (LSubSpβπ) β§ π β π₯) β (ran πΆ βͺ π) β π₯)) |
| 11 | 10 | pm5.32da 577 |
. . . . . . 7
β’ (π β AssAlg β ((π₯ β (SubRingβπ) β§ (π₯ β (LSubSpβπ) β§ π β π₯)) β (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯))) |
| 12 | 4, 11 | bitrid 282 |
. . . . . 6
β’ (π β AssAlg β ((π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯) β (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯))) |
| 13 | 12 | abbidv 2799 |
. . . . 5
β’ (π β AssAlg β {π₯ β£ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯)} = {π₯ β£ (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯)}) |
| 14 | 13 | adantr 479 |
. . . 4
β’ ((π β AssAlg β§ π β π) β {π₯ β£ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯)} = {π₯ β£ (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯)}) |
| 15 | | df-rab 3431 |
. . . 4
β’ {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯} = {π₯ β£ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯)} |
| 16 | | df-rab 3431 |
. . . 4
β’ {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯} = {π₯ β£ (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯)} |
| 17 | 14, 15, 16 | 3eqtr4g 2795 |
. . 3
β’ ((π β AssAlg β§ π β π) β {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯} = {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
| 18 | 17 | inteqd 4954 |
. 2
β’ ((π β AssAlg β§ π β π) β β© {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯} = β© {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
| 19 | | aspval2.a |
. . 3
β’ π΄ = (AlgSpanβπ) |
| 20 | | aspval2.v |
. . 3
β’ π = (Baseβπ) |
| 21 | 19, 20, 6 | aspval 21646 |
. 2
β’ ((π β AssAlg β§ π β π) β (π΄βπ) = β© {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯}) |
| 22 | | assaring 21635 |
. . . 4
β’ (π β AssAlg β π β Ring) |
| 23 | 20 | subrgmre 20487 |
. . . 4
β’ (π β Ring β
(SubRingβπ) β
(Mooreβπ)) |
| 24 | 22, 23 | syl 17 |
. . 3
β’ (π β AssAlg β
(SubRingβπ) β
(Mooreβπ)) |
| 25 | | eqid 2730 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
| 26 | | assalmod 21634 |
. . . . . . 7
β’ (π β AssAlg β π β LMod) |
| 27 | | eqid 2730 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
| 28 | 5, 25, 22, 26, 27, 20 | asclf 21655 |
. . . . . 6
β’ (π β AssAlg β πΆ:(Baseβ(Scalarβπ))βΆπ) |
| 29 | 28 | frnd 6724 |
. . . . 5
β’ (π β AssAlg β ran πΆ β π) |
| 30 | 29 | adantr 479 |
. . . 4
β’ ((π β AssAlg β§ π β π) β ran πΆ β π) |
| 31 | | simpr 483 |
. . . 4
β’ ((π β AssAlg β§ π β π) β π β π) |
| 32 | 30, 31 | unssd 4185 |
. . 3
β’ ((π β AssAlg β§ π β π) β (ran πΆ βͺ π) β π) |
| 33 | | aspval2.r |
. . . 4
β’ π
=
(mrClsβ(SubRingβπ)) |
| 34 | 33 | mrcval 17558 |
. . 3
β’
(((SubRingβπ)
β (Mooreβπ)
β§ (ran πΆ βͺ π) β π) β (π
β(ran πΆ βͺ π)) = β© {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
| 35 | 24, 32, 34 | syl2an2r 681 |
. 2
β’ ((π β AssAlg β§ π β π) β (π
β(ran πΆ βͺ π)) = β© {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
| 36 | 18, 21, 35 | 3eqtr4d 2780 |
1
β’ ((π β AssAlg β§ π β π) β (π΄βπ) = (π
β(ran πΆ βͺ π))) |
