Metamath Proof Explorer

Theorem sradrng

Description: Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Hypotheses sraring.1 ⊢ 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑉 )
sraring.2 ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion sradrng ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → 𝐴 ∈ DivRing )

Proof

Step Hyp Ref Expression
1 sraring.1 ⊢ 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑉 )
2 sraring.2 ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
4 1 2 sraring ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵 ) → 𝐴 ∈ Ring )
5 3 4 sylan ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → 𝐴 ∈ Ring )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 6 7 8 isdrng ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) )
10 9 simprbi ⊢ ( 𝑅 ∈ DivRing → ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
11 10 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
12 eqidd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
13 1 a1i ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑉 ) )
14 simpr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ⊆ 𝐵 )
15 14 2 sseqtrdi ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → 𝑉 ⊆ ( Base ‘ 𝑅 ) )
16 13 15 srabase ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝐴 ) )
17 13 15 sramulr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐴 ) )
18 17 oveqdr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) )
19 12 16 18 unitpropd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝐴 ) )
20 eqidd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
21 13 20 15 sralmod0 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐴 ) )
22 21 sneqd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → { ( 0g ‘ 𝑅 ) } = { ( 0g ‘ 𝐴 ) } )
23 16 22 difeq12d ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) = ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) )
24 11 19 23 3eqtr3d ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → ( Unit ‘ 𝐴 ) = ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) )
25 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
26 eqid ⊢ ( Unit ‘ 𝐴 ) = ( Unit ‘ 𝐴 )
27 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
28 25 26 27 isdrng ⊢ ( 𝐴 ∈ DivRing ↔ ( 𝐴 ∈ Ring ∧ ( Unit ‘ 𝐴 ) = ( ( Base ‘ 𝐴 ) ∖ { ( 0g ‘ 𝐴 ) } ) ) )
29 5 24 28 sylanbrc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵 ) → 𝐴 ∈ DivRing )