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 φ E DivRing
drgext.2 φ U SubRing E
drgext.f F = E 𝑠 U
drgext.3 φ F DivRing
Assertion drgextlsp φ U LSubSp B

Proof

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