sradrng

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

	Ref	Expression
Hypotheses	sradrng.1	$⊢ A = subringAlg (R) (V)$
	sradrng.2	$⊢ B = {Base}_{R}$
Assertion	sradrng	$⊢ (R \in DivRing \land V \subseteq B) \to A \in DivRing$

Proof

Step	Hyp	Ref	Expression
1		sradrng.1	$⊢ A = subringAlg (R) (V)$
2		sradrng.2	$⊢ B = {Base}_{R}$
3		drngring	$⊢ R \in DivRing \to R \in Ring$
4	1 2	sraring	$⊢ (R \in Ring \land V \subseteq B) \to A \in Ring$
5	3 4	sylan	$⊢ (R \in DivRing \land V \subseteq B) \to A \in Ring$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ Unit (R) = Unit (R)$
8		eqid	$⊢ 0_{R} = 0_{R}$
9	6 7 8	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = {Base}_{R} ∖ \{0_{R}\})$
10	9	simprbi	$⊢ R \in DivRing \to Unit (R) = {Base}_{R} ∖ \{0_{R}\}$
11	10	adantr	$⊢ (R \in DivRing \land V \subseteq B) \to Unit (R) = {Base}_{R} ∖ \{0_{R}\}$
12		eqidd	$⊢ (R \in DivRing \land V \subseteq B) \to {Base}_{R} = {Base}_{R}$
13	1	a1i	$⊢ (R \in DivRing \land V \subseteq B) \to A = subringAlg (R) (V)$
14		simpr	$⊢ (R \in DivRing \land V \subseteq B) \to V \subseteq B$
15	14 2	sseqtrdi	$⊢ (R \in DivRing \land V \subseteq B) \to V \subseteq {Base}_{R}$
16	13 15	srabase	$⊢ (R \in DivRing \land V \subseteq B) \to {Base}_{R} = {Base}_{A}$
17	13 15	sramulr	$⊢ (R \in DivRing \land V \subseteq B) \to \cdot_{R} = \cdot_{A}$
18	17	oveqdr	$⊢ ((R \in DivRing \land V \subseteq B) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x \cdot_{R} y = x \cdot_{A} y$
19	12 16 18	unitpropd	$⊢ (R \in DivRing \land V \subseteq B) \to Unit (R) = Unit (A)$
20		eqidd	$⊢ (R \in DivRing \land V \subseteq B) \to 0_{R} = 0_{R}$
21	13 20 15	sralmod0	$⊢ (R \in DivRing \land V \subseteq B) \to 0_{R} = 0_{A}$
22	21	sneqd	$⊢ (R \in DivRing \land V \subseteq B) \to \{0_{R}\} = \{0_{A}\}$
23	16 22	difeq12d	$⊢ (R \in DivRing \land V \subseteq B) \to {Base}_{R} ∖ \{0_{R}\} = {Base}_{A} ∖ \{0_{A}\}$
24	11 19 23	3eqtr3d	$⊢ (R \in DivRing \land V \subseteq B) \to Unit (A) = {Base}_{A} ∖ \{0_{A}\}$
25		eqid	$⊢ {Base}_{A} = {Base}_{A}$
26		eqid	$⊢ Unit (A) = Unit (A)$
27		eqid	$⊢ 0_{A} = 0_{A}$
28	25 26 27	isdrng	$⊢ A \in DivRing \leftrightarrow (A \in Ring \land Unit (A) = {Base}_{A} ∖ \{0_{A}\})$
29	5 24 28	sylanbrc	$⊢ (R \in DivRing \land V \subseteq B) \to A \in DivRing$

Metamath Proof Explorer

Theorem sradrng

Proof