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 ⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
drgext.1 ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
drgext.2 ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
drgext.f ⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
drgext.3 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
Assertion drgextlsp ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 drgext.b ⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
2 drgext.1 ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
3 drgext.2 ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
4 drgext.f ⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
5 drgext.3 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
6 eqidd ⊢ ( 𝜑 → ( Scalar ‘ 𝐵 ) = ( Scalar ‘ 𝐵 ) )
7 eqidd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐵 ) ) = ( Base ‘ ( Scalar ‘ 𝐵 ) ) )
8 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 ) )
9 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝐵 ) = ( +g ‘ 𝐵 ) )
10 eqidd ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐵 ) = ( ·𝑠 ‘ 𝐵 ) )
11 eqidd ⊢ ( 𝜑 → ( LSubSp ‘ 𝐵 ) = ( LSubSp ‘ 𝐵 ) )
12 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
13 12 subrgss ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
14 3 13 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
15 1 a1i ⊢ ( 𝜑 → 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) )
16 15 14 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( Base ‘ 𝐵 ) )
17 14 16 sseqtrd ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐵 ) )
18 eqid ⊢ ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐸 )
19 18 subrg1cl ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( 1r ‘ 𝐸 ) ∈ 𝑈 )
20 ne0i ⊢ ( ( 1r ‘ 𝐸 ) ∈ 𝑈 → 𝑈 ≠ ∅ )
21 3 19 20 3syl ⊢ ( 𝜑 → 𝑈 ≠ ∅ )
22 drnggrp ⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ Grp )
23 5 22 syl ⊢ ( 𝜑 → 𝐹 ∈ Grp )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝐹 ∈ Grp )
25 15 14 sravsca ⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐵 ) )
26 eqid ⊢ ( .r ‘ 𝐸 ) = ( .r ‘ 𝐸 )
27 4 26 ressmulr ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( .r ‘ 𝐸 ) = ( .r ‘ 𝐹 ) )
28 3 27 syl ⊢ ( 𝜑 → ( .r ‘ 𝐸 ) = ( .r ‘ 𝐹 ) )
29 25 28 eqtr3d ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐵 ) = ( .r ‘ 𝐹 ) )
30 29 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐵 ) 𝑎 ) = ( 𝑥 ( .r ‘ 𝐹 ) 𝑎 ) )
31 drngring ⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ Ring )
32 5 31 syl ⊢ ( 𝜑 → 𝐹 ∈ Ring )
33 32 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝐹 ∈ Ring )
34 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) )
35 15 14 srasca ⊢ ( 𝜑 → ( 𝐸 ↾s 𝑈 ) = ( Scalar ‘ 𝐵 ) )
36 4 35 syl5eq ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐵 ) )
37 36 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐵 ) ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐵 ) ) )
39 34 38 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
40 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑎 ∈ 𝑈 )
41 4 12 ressbas2 ⊢ ( 𝑈 ⊆ ( Base ‘ 𝐸 ) → 𝑈 = ( Base ‘ 𝐹 ) )
42 14 41 syl ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐹 ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑈 = ( Base ‘ 𝐹 ) )
44 40 43 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑎 ∈ ( Base ‘ 𝐹 ) )
45 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
46 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
47 45 46 ringcl ⊢ ( ( 𝐹 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑎 ∈ ( Base ‘ 𝐹 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑎 ) ∈ ( Base ‘ 𝐹 ) )
48 33 39 44 47 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑎 ) ∈ ( Base ‘ 𝐹 ) )
49 30 48 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐵 ) 𝑎 ) ∈ ( Base ‘ 𝐹 ) )
50 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑏 ∈ 𝑈 )
51 50 43 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑏 ∈ ( Base ‘ 𝐹 ) )
52 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
53 45 52 grpcl ⊢ ( ( 𝐹 ∈ Grp ∧ ( 𝑥 ( ·𝑠 ‘ 𝐵 ) 𝑎 ) ∈ ( Base ‘ 𝐹 ) ∧ 𝑏 ∈ ( Base ‘ 𝐹 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝐵 ) 𝑎 ) ( +g ‘ 𝐹 ) 𝑏 ) ∈ ( Base ‘ 𝐹 ) )
54 24 49 51 53 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝐵 ) 𝑎 ) ( +g ‘ 𝐹 ) 𝑏 ) ∈ ( Base ‘ 𝐹 ) )
55 15 14 sraaddg ⊢ ( 𝜑 → ( +g ‘ 𝐸 ) = ( +g ‘ 𝐵 ) )
56 eqid ⊢ ( +g ‘ 𝐸 ) = ( +g ‘ 𝐸 )
57 4 56 ressplusg ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( +g ‘ 𝐸 ) = ( +g ‘ 𝐹 ) )
58 3 57 syl ⊢ ( 𝜑 → ( +g ‘ 𝐸 ) = ( +g ‘ 𝐹 ) )
59 55 58 eqtr3d ⊢ ( 𝜑 → ( +g ‘ 𝐵 ) = ( +g ‘ 𝐹 ) )
60 59 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( +g ‘ 𝐵 ) = ( +g ‘ 𝐹 ) )
61 60 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝐵 ) 𝑎 ) ( +g ‘ 𝐵 ) 𝑏 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝐵 ) 𝑎 ) ( +g ‘ 𝐹 ) 𝑏 ) )
62 54 61 43 3eltr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐵 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝐵 ) 𝑎 ) ( +g ‘ 𝐵 ) 𝑏 ) ∈ 𝑈 )
63 6 7 8 9 10 11 17 21 62 islssd ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝐵 ) )