sdrginvcl

Description: A sub-division-ring is closed under the ring inverse operation. (Contributed by Thierry Arnoux, 15-Jan-2025)

	Ref	Expression
Hypotheses	sdrginvcl.i	$⊢ I = {inv}_{r} (R)$
	sdrginvcl.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	sdrginvcl	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to I (X) \in A$

Proof

Step	Hyp	Ref	Expression
1		sdrginvcl.i	$⊢ I = {inv}_{r} (R)$
2		sdrginvcl.0	$⊢ \underset{˙}{0} = 0_{R}$
3		issdrg	$⊢ A \in SubDRing (R) \leftrightarrow (R \in DivRing \land A \in SubRing (R) \land R ↾_{𝑠} A \in DivRing)$
4	3	biimpi	$⊢ A \in SubDRing (R) \to (R \in DivRing \land A \in SubRing (R) \land R ↾_{𝑠} A \in DivRing)$
5	4	3ad2ant1	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to (R \in DivRing \land A \in SubRing (R) \land R ↾_{𝑠} A \in DivRing)$
6	5	simp3d	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to R ↾_{𝑠} A \in DivRing$
7		simp2	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to X \in A$
8	5	simp2d	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to A \in SubRing (R)$
9		eqid	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} A$
10	9	subrgbas	$⊢ A \in SubRing (R) \to A = {Base}_{(R ↾_{𝑠} A)}$
11	8 10	syl	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to A = {Base}_{(R ↾_{𝑠} A)}$
12	7 11	eleqtrd	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to X \in {Base}_{(R ↾_{𝑠} A)}$
13		simp3	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to X \neq \underset{˙}{0}$
14	9 2	subrg0	$⊢ A \in SubRing (R) \to \underset{˙}{0} = 0_{(R ↾_{𝑠} A)}$
15	8 14	syl	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to \underset{˙}{0} = 0_{(R ↾_{𝑠} A)}$
16	13 15	neeqtrd	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to X \neq 0_{(R ↾_{𝑠} A)}$
17		eqid	$⊢ {Base}_{(R ↾_{𝑠} A)} = {Base}_{(R ↾_{𝑠} A)}$
18		eqid	$⊢ 0_{(R ↾_{𝑠} A)} = 0_{(R ↾_{𝑠} A)}$
19		eqid	$⊢ {inv}_{r} (R ↾_{𝑠} A) = {inv}_{r} (R ↾_{𝑠} A)$
20	17 18 19	drnginvrcl	$⊢ (R ↾_{𝑠} A \in DivRing \land X \in {Base}_{(R ↾_{𝑠} A)} \land X \neq 0_{(R ↾_{𝑠} A)}) \to {inv}_{r} (R ↾_{𝑠} A) (X) \in {Base}_{(R ↾_{𝑠} A)}$
21	6 12 16 20	syl3anc	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to {inv}_{r} (R ↾_{𝑠} A) (X) \in {Base}_{(R ↾_{𝑠} A)}$
22		eqid	$⊢ Unit (R ↾_{𝑠} A) = Unit (R ↾_{𝑠} A)$
23	17 22 18	drngunit	$⊢ R ↾_{𝑠} A \in DivRing \to (X \in Unit (R ↾_{𝑠} A) \leftrightarrow (X \in {Base}_{(R ↾_{𝑠} A)} \land X \neq 0_{(R ↾_{𝑠} A)}))$
24	23	biimpar	$⊢ (R ↾_{𝑠} A \in DivRing \land (X \in {Base}_{(R ↾_{𝑠} A)} \land X \neq 0_{(R ↾_{𝑠} A)})) \to X \in Unit (R ↾_{𝑠} A)$
25	6 12 16 24	syl12anc	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to X \in Unit (R ↾_{𝑠} A)$
26	9 1 22 19	subrginv	$⊢ (A \in SubRing (R) \land X \in Unit (R ↾_{𝑠} A)) \to I (X) = {inv}_{r} (R ↾_{𝑠} A) (X)$
27	8 25 26	syl2anc	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to I (X) = {inv}_{r} (R ↾_{𝑠} A) (X)$
28	21 27 11	3eltr4d	$⊢ (A \in SubDRing (R) \land X \in A \land X \neq \underset{˙}{0}) \to I (X) \in A$

Metamath Proof Explorer

Theorem sdrginvcl

Proof