Step | Hyp | Ref
| Expression |
1 | | elin 3927 |
. . . . . . . . 9
β’ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β (π₯ β (SubRingβπ) β§ π₯ β (LSubSpβπ))) |
2 | 1 | anbi1i 625 |
. . . . . . . 8
β’ ((π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯) β ((π₯ β (SubRingβπ) β§ π₯ β (LSubSpβπ)) β§ π β π₯)) |
3 | | anass 470 |
. . . . . . . 8
β’ (((π₯ β (SubRingβπ) β§ π₯ β (LSubSpβπ)) β§ π β π₯) β (π₯ β (SubRingβπ) β§ (π₯ β (LSubSpβπ) β§ π β π₯))) |
4 | 2, 3 | bitri 275 |
. . . . . . 7
β’ ((π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯) β (π₯ β (SubRingβπ) β§ (π₯ β (LSubSpβπ) β§ π β π₯))) |
5 | | aspval2.c |
. . . . . . . . . . 11
β’ πΆ = (algScβπ) |
6 | | eqid 2733 |
. . . . . . . . . . 11
β’
(LSubSpβπ) =
(LSubSpβπ) |
7 | 5, 6 | issubassa2 21311 |
. . . . . . . . . 10
β’ ((π β AssAlg β§ π₯ β (SubRingβπ)) β (π₯ β (LSubSpβπ) β ran πΆ β π₯)) |
8 | 7 | anbi1d 631 |
. . . . . . . . 9
β’ ((π β AssAlg β§ π₯ β (SubRingβπ)) β ((π₯ β (LSubSpβπ) β§ π β π₯) β (ran πΆ β π₯ β§ π β π₯))) |
9 | | unss 4145 |
. . . . . . . . 9
β’ ((ran
πΆ β π₯ β§ π β π₯) β (ran πΆ βͺ π) β π₯) |
10 | 8, 9 | bitrdi 287 |
. . . . . . . 8
β’ ((π β AssAlg β§ π₯ β (SubRingβπ)) β ((π₯ β (LSubSpβπ) β§ π β π₯) β (ran πΆ βͺ π) β π₯)) |
11 | 10 | pm5.32da 580 |
. . . . . . 7
β’ (π β AssAlg β ((π₯ β (SubRingβπ) β§ (π₯ β (LSubSpβπ) β§ π β π₯)) β (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯))) |
12 | 4, 11 | bitrid 283 |
. . . . . 6
β’ (π β AssAlg β ((π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯) β (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯))) |
13 | 12 | abbidv 2802 |
. . . . 5
β’ (π β AssAlg β {π₯ β£ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯)} = {π₯ β£ (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯)}) |
14 | 13 | adantr 482 |
. . . 4
β’ ((π β AssAlg β§ π β π) β {π₯ β£ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯)} = {π₯ β£ (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯)}) |
15 | | df-rab 3407 |
. . . 4
β’ {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯} = {π₯ β£ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯)} |
16 | | df-rab 3407 |
. . . 4
β’ {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯} = {π₯ β£ (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯)} |
17 | 14, 15, 16 | 3eqtr4g 2798 |
. . 3
β’ ((π β AssAlg β§ π β π) β {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯} = {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
18 | 17 | inteqd 4913 |
. 2
β’ ((π β AssAlg β§ π β π) β β© {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯} = β© {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
19 | | aspval2.a |
. . 3
β’ π΄ = (AlgSpanβπ) |
20 | | aspval2.v |
. . 3
β’ π = (Baseβπ) |
21 | 19, 20, 6 | aspval 21292 |
. 2
β’ ((π β AssAlg β§ π β π) β (π΄βπ) = β© {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯}) |
22 | | assaring 21283 |
. . . 4
β’ (π β AssAlg β π β Ring) |
23 | 20 | subrgmre 20260 |
. . . 4
β’ (π β Ring β
(SubRingβπ) β
(Mooreβπ)) |
24 | 22, 23 | syl 17 |
. . 3
β’ (π β AssAlg β
(SubRingβπ) β
(Mooreβπ)) |
25 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
26 | | assalmod 21282 |
. . . . . . 7
β’ (π β AssAlg β π β LMod) |
27 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
28 | 5, 25, 22, 26, 27, 20 | asclf 21301 |
. . . . . 6
β’ (π β AssAlg β πΆ:(Baseβ(Scalarβπ))βΆπ) |
29 | 28 | frnd 6677 |
. . . . 5
β’ (π β AssAlg β ran πΆ β π) |
30 | 29 | adantr 482 |
. . . 4
β’ ((π β AssAlg β§ π β π) β ran πΆ β π) |
31 | | simpr 486 |
. . . 4
β’ ((π β AssAlg β§ π β π) β π β π) |
32 | 30, 31 | unssd 4147 |
. . 3
β’ ((π β AssAlg β§ π β π) β (ran πΆ βͺ π) β π) |
33 | | aspval2.r |
. . . 4
β’ π
=
(mrClsβ(SubRingβπ)) |
34 | 33 | mrcval 17495 |
. . 3
β’
(((SubRingβπ)
β (Mooreβπ)
β§ (ran πΆ βͺ π) β π) β (π
β(ran πΆ βͺ π)) = β© {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
35 | 24, 32, 34 | syl2an2r 684 |
. 2
β’ ((π β AssAlg β§ π β π) β (π
β(ran πΆ βͺ π)) = β© {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
36 | 18, 21, 35 | 3eqtr4d 2783 |
1
β’ ((π β AssAlg β§ π β π) β (π΄βπ) = (π
β(ran πΆ βͺ π))) |