Metamath Proof Explorer

Theorem drgextlsp

Description: The scalar field is a subspace of a subring algebra. (Contributed by Thierry Arnoux, 17-Jul-2023)

Ref Expression
Hypotheses drgext.b 
|- B = ( ( subringAlg ` E ) ` U )
drgext.1 
|- ( ph -> E e. DivRing )
drgext.2 
|- ( ph -> U e. ( SubRing ` E ) )
drgext.f 
|- F = ( E |`s U )
drgext.3 
|- ( ph -> F e. DivRing )
Assertion drgextlsp 
|- ( ph -> U e. ( LSubSp ` B ) )

Proof

Step Hyp Ref Expression
1 drgext.b 
 |-  B = ( ( subringAlg ` E ) ` U )
2 drgext.1 
 |-  ( ph -> E e. DivRing )
3 drgext.2 
 |-  ( ph -> U e. ( SubRing ` E ) )
4 drgext.f 
 |-  F = ( E |`s U )
5 drgext.3 
 |-  ( ph -> F e. DivRing )
6 eqidd 
 |-  ( ph -> ( Scalar ` B ) = ( Scalar ` B ) )
7 eqidd 
 |-  ( ph -> ( Base ` ( Scalar ` B ) ) = ( Base ` ( Scalar ` B ) ) )
8 eqidd 
 |-  ( ph -> ( Base ` B ) = ( Base ` B ) )
9 eqidd 
 |-  ( ph -> ( +g ` B ) = ( +g ` B ) )
10 eqidd 
 |-  ( ph -> ( .s ` B ) = ( .s ` B ) )
11 eqidd 
 |-  ( ph -> ( LSubSp ` B ) = ( LSubSp ` B ) )
12 eqid 
 |-  ( Base ` E ) = ( Base ` E )
13 12 subrgss 
 |-  ( U e. ( SubRing ` E ) -> U C_ ( Base ` E ) )
14 3 13 syl 
 |-  ( ph -> U C_ ( Base ` E ) )
15 1 a1i 
 |-  ( ph -> B = ( ( subringAlg ` E ) ` U ) )
16 15 14 srabase 
 |-  ( ph -> ( Base ` E ) = ( Base ` B ) )
17 14 16 sseqtrd 
 |-  ( ph -> U C_ ( Base ` B ) )
18 eqid 
 |-  ( 1r ` E ) = ( 1r ` E )
19 18 subrg1cl 
 |-  ( U e. ( SubRing ` E ) -> ( 1r ` E ) e. U )
20 ne0i 
 |-  ( ( 1r ` E ) e. U -> U =/= (/) )
21 3 19 20 3syl 
 |-  ( ph -> U =/= (/) )
22 drnggrp 
 |-  ( F e. DivRing -> F e. Grp )
23 5 22 syl 
 |-  ( ph -> F e. Grp )
24 23 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> F e. Grp )
25 15 14 sravsca 
 |-  ( ph -> ( .r ` E ) = ( .s ` B ) )
26 eqid 
 |-  ( .r ` E ) = ( .r ` E )
27 4 26 ressmulr 
 |-  ( U e. ( SubRing ` E ) -> ( .r ` E ) = ( .r ` F ) )
28 3 27 syl 
 |-  ( ph -> ( .r ` E ) = ( .r ` F ) )
29 25 28 eqtr3d 
 |-  ( ph -> ( .s ` B ) = ( .r ` F ) )
30 29 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> ( x ( .s ` B ) a ) = ( x ( .r ` F ) a ) )
31 drngring 
 |-  ( F e. DivRing -> F e. Ring )
32 5 31 syl 
 |-  ( ph -> F e. Ring )
33 32 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> F e. Ring )
34 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> x e. ( Base ` ( Scalar ` B ) ) )
35 15 14 srasca 
 |-  ( ph -> ( E |`s U ) = ( Scalar ` B ) )
36 4 35 syl5eq 
 |-  ( ph -> F = ( Scalar ` B ) )
37 36 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` B ) ) )
38 37 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> ( Base ` F ) = ( Base ` ( Scalar ` B ) ) )
39 34 38 eleqtrrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> x e. ( Base ` F ) )
40 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> a e. U )
41 4 12 ressbas2 
 |-  ( U C_ ( Base ` E ) -> U = ( Base ` F ) )
42 14 41 syl 
 |-  ( ph -> U = ( Base ` F ) )
43 42 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> U = ( Base ` F ) )
44 40 43 eleqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> a e. ( Base ` F ) )
45 eqid 
 |-  ( Base ` F ) = ( Base ` F )
46 eqid 
 |-  ( .r ` F ) = ( .r ` F )
47 45 46 ringcl 
 |-  ( ( F e. Ring /\ x e. ( Base ` F ) /\ a e. ( Base ` F ) ) -> ( x ( .r ` F ) a ) e. ( Base ` F ) )
48 33 39 44 47 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> ( x ( .r ` F ) a ) e. ( Base ` F ) )
49 30 48 eqeltrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> ( x ( .s ` B ) a ) e. ( Base ` F ) )
50 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> b e. U )
51 50 43 eleqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> b e. ( Base ` F ) )
52 eqid 
 |-  ( +g ` F ) = ( +g ` F )
53 45 52 grpcl 
 |-  ( ( F e. Grp /\ ( x ( .s ` B ) a ) e. ( Base ` F ) /\ b e. ( Base ` F ) ) -> ( ( x ( .s ` B ) a ) ( +g ` F ) b ) e. ( Base ` F ) )
54 24 49 51 53 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> ( ( x ( .s ` B ) a ) ( +g ` F ) b ) e. ( Base ` F ) )
55 15 14 sraaddg 
 |-  ( ph -> ( +g ` E ) = ( +g ` B ) )
56 eqid 
 |-  ( +g ` E ) = ( +g ` E )
57 4 56 ressplusg 
 |-  ( U e. ( SubRing ` E ) -> ( +g ` E ) = ( +g ` F ) )
58 3 57 syl 
 |-  ( ph -> ( +g ` E ) = ( +g ` F ) )
59 55 58 eqtr3d 
 |-  ( ph -> ( +g ` B ) = ( +g ` F ) )
60 59 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> ( +g ` B ) = ( +g ` F ) )
61 60 oveqd 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> ( ( x ( .s ` B ) a ) ( +g ` B ) b ) = ( ( x ( .s ` B ) a ) ( +g ` F ) b ) )
62 54 61 43 3eltr4d 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` B ) ) /\ a e. U /\ b e. U ) ) -> ( ( x ( .s ` B ) a ) ( +g ` B ) b ) e. U )
63 6 7 8 9 10 11 17 21 62 islssd 
 |-  ( ph -> U e. ( LSubSp ` B ) )