imadrhmcl

Description: The image of a (nontrivial) division ring homomorphism is a division ring. (Contributed by SN, 17-Feb-2025)

	Ref	Expression
Hypotheses	imadrhmcl.r	$⊢ R = N ↾_{𝑠} F [S]$
	imadrhmcl.0	$⊢ \underset{˙}{0} = 0_{N}$
	imadrhmcl.h	$⊢ φ \to F \in (M RingHom N)$
	imadrhmcl.s	$⊢ φ \to S \in SubDRing (M)$
	imadrhmcl.1	$⊢ φ \to ran F \neq \{\underset{˙}{0}\}$
Assertion	imadrhmcl	$⊢ φ \to R \in DivRing$

Proof

Step	Hyp	Ref	Expression
1		imadrhmcl.r	$⊢ R = N ↾_{𝑠} F [S]$
2		imadrhmcl.0	$⊢ \underset{˙}{0} = 0_{N}$
3		imadrhmcl.h	$⊢ φ \to F \in (M RingHom N)$
4		imadrhmcl.s	$⊢ φ \to S \in SubDRing (M)$
5		imadrhmcl.1	$⊢ φ \to ran F \neq \{\underset{˙}{0}\}$
6		sdrgsubrg	$⊢ S \in SubDRing (M) \to S \in SubRing (M)$
7	4 6	syl	$⊢ φ \to S \in SubRing (M)$
8		rhmima	$⊢ (F \in (M RingHom N) \land S \in SubRing (M)) \to F [S] \in SubRing (N)$
9	3 7 8	syl2anc	$⊢ φ \to F [S] \in SubRing (N)$
10	1	subrgring	$⊢ F [S] \in SubRing (N) \to R \in Ring$
11	9 10	syl	$⊢ φ \to R \in Ring$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13		eqid	$⊢ Unit (R) = Unit (R)$
14	12 13	unitss	$⊢ Unit (R) \subseteq {Base}_{R}$
15	14	a1i	$⊢ φ \to Unit (R) \subseteq {Base}_{R}$
16		eqid	$⊢ {Base}_{M} = {Base}_{M}$
17		eqid	$⊢ {Base}_{N} = {Base}_{N}$
18	16 17	rhmf	$⊢ F \in (M RingHom N) \to F : {Base}_{M} ⟶ {Base}_{N}$
19	3 18	syl	$⊢ φ \to F : {Base}_{M} ⟶ {Base}_{N}$
20	19	adantr	$⊢ (φ \land 1_{R} = 0_{R}) \to F : {Base}_{M} ⟶ {Base}_{N}$
21		rhmrcl2	$⊢ F \in (M RingHom N) \to N \in Ring$
22	3 21	syl	$⊢ φ \to N \in Ring$
23		simpr	$⊢ (φ \land 1_{R} = 0_{R}) \to 1_{R} = 0_{R}$
24		eqid	$⊢ 1_{N} = 1_{N}$
25	1 24	subrg1	$⊢ F [S] \in SubRing (N) \to 1_{N} = 1_{R}$
26	9 25	syl	$⊢ φ \to 1_{N} = 1_{R}$
27	26	adantr	$⊢ (φ \land 1_{R} = 0_{R}) \to 1_{N} = 1_{R}$
28	1 2	subrg0	$⊢ F [S] \in SubRing (N) \to \underset{˙}{0} = 0_{R}$
29	9 28	syl	$⊢ φ \to \underset{˙}{0} = 0_{R}$
30	29	adantr	$⊢ (φ \land 1_{R} = 0_{R}) \to \underset{˙}{0} = 0_{R}$
31	23 27 30	3eqtr4rd	$⊢ (φ \land 1_{R} = 0_{R}) \to \underset{˙}{0} = 1_{N}$
32	17 2 24	01eq0ring	$⊢ (N \in Ring \land \underset{˙}{0} = 1_{N}) \to {Base}_{N} = \{\underset{˙}{0}\}$
33	22 31 32	syl2an2r	$⊢ (φ \land 1_{R} = 0_{R}) \to {Base}_{N} = \{\underset{˙}{0}\}$
34	33	feq3d	$⊢ (φ \land 1_{R} = 0_{R}) \to (F : {Base}_{M} ⟶ {Base}_{N} \leftrightarrow F : {Base}_{M} ⟶ \{\underset{˙}{0}\})$
35	20 34	mpbid	$⊢ (φ \land 1_{R} = 0_{R}) \to F : {Base}_{M} ⟶ \{\underset{˙}{0}\}$
36	2	fvexi	$⊢ \underset{˙}{0} \in V$
37	36	fconst2	$⊢ F : {Base}_{M} ⟶ \{\underset{˙}{0}\} \leftrightarrow F = {Base}_{M} \times \{\underset{˙}{0}\}$
38	35 37	sylib	$⊢ (φ \land 1_{R} = 0_{R}) \to F = {Base}_{M} \times \{\underset{˙}{0}\}$
39	19	ffnd	$⊢ φ \to F Fn {Base}_{M}$
40		sdrgrcl	$⊢ S \in SubDRing (M) \to M \in DivRing$
41	4 40	syl	$⊢ φ \to M \in DivRing$
42	41	drngringd	$⊢ φ \to M \in Ring$
43		eqid	$⊢ 0_{M} = 0_{M}$
44	16 43	ring0cl	$⊢ M \in Ring \to 0_{M} \in {Base}_{M}$
45	42 44	syl	$⊢ φ \to 0_{M} \in {Base}_{M}$
46	45	ne0d	$⊢ φ \to {Base}_{M} \neq \emptyset$
47		fconst5	$⊢ (F Fn {Base}_{M} \land {Base}_{M} \neq \emptyset) \to (F = {Base}_{M} \times \{\underset{˙}{0}\} \leftrightarrow ran F = \{\underset{˙}{0}\})$
48	39 46 47	syl2anc	$⊢ φ \to (F = {Base}_{M} \times \{\underset{˙}{0}\} \leftrightarrow ran F = \{\underset{˙}{0}\})$
49	48	adantr	$⊢ (φ \land 1_{R} = 0_{R}) \to (F = {Base}_{M} \times \{\underset{˙}{0}\} \leftrightarrow ran F = \{\underset{˙}{0}\})$
50	38 49	mpbid	$⊢ (φ \land 1_{R} = 0_{R}) \to ran F = \{\underset{˙}{0}\}$
51	5 50	mteqand	$⊢ φ \to 1_{R} \neq 0_{R}$
52		eqid	$⊢ 0_{R} = 0_{R}$
53		eqid	$⊢ 1_{R} = 1_{R}$
54	13 52 53	0unit	$⊢ R \in Ring \to (0_{R} \in Unit (R) \leftrightarrow 1_{R} = 0_{R})$
55	11 54	syl	$⊢ φ \to (0_{R} \in Unit (R) \leftrightarrow 1_{R} = 0_{R})$
56	55	necon3bbid	$⊢ φ \to (\neg 0_{R} \in Unit (R) \leftrightarrow 1_{R} \neq 0_{R})$
57	51 56	mpbird	$⊢ φ \to \neg 0_{R} \in Unit (R)$
58		ssdifsn	$⊢ Unit (R) \subseteq {Base}_{R} ∖ \{0_{R}\} \leftrightarrow (Unit (R) \subseteq {Base}_{R} \land \neg 0_{R} \in Unit (R))$
59	15 57 58	sylanbrc	$⊢ φ \to Unit (R) \subseteq {Base}_{R} ∖ \{0_{R}\}$
60	39	fnfund	$⊢ φ \to Fun F$
61	1	ressbasss2	$⊢ {Base}_{R} \subseteq F [S]$
62		eldifi	$⊢ x \in ({Base}_{R} ∖ \{0_{R}\}) \to x \in {Base}_{R}$
63	61 62	sselid	$⊢ x \in ({Base}_{R} ∖ \{0_{R}\}) \to x \in F [S]$
64		fvelima	$⊢ (Fun F \land x \in F [S]) \to \exists a \in S F (a) = x$
65	60 63 64	syl2an	$⊢ (φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \to \exists a \in S F (a) = x$
66		simprr	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to F (a) = x$
67		simprl	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to a \in S$
68	67	fvresd	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to ({F ↾}_{S}) (a) = F (a)$
69		eqid	$⊢ M ↾_{𝑠} S = M ↾_{𝑠} S$
70	69	resrhm	$⊢ (F \in (M RingHom N) \land S \in SubRing (M)) \to {F ↾}_{S} \in ((M ↾_{𝑠} S) RingHom N)$
71	3 7 70	syl2anc	$⊢ φ \to {F ↾}_{S} \in ((M ↾_{𝑠} S) RingHom N)$
72		df-ima	$⊢ F [S] = ran ({F ↾}_{S})$
73		eqimss2	$⊢ F [S] = ran ({F ↾}_{S}) \to ran ({F ↾}_{S}) \subseteq F [S]$
74	72 73	mp1i	$⊢ φ \to ran ({F ↾}_{S}) \subseteq F [S]$
75	1	resrhm2b	$⊢ (F [S] \in SubRing (N) \land ran ({F ↾}_{S}) \subseteq F [S]) \to ({F ↾}_{S} \in ((M ↾_{𝑠} S) RingHom N) \leftrightarrow {F ↾}_{S} \in ((M ↾_{𝑠} S) RingHom R))$
76	9 74 75	syl2anc	$⊢ φ \to ({F ↾}_{S} \in ((M ↾_{𝑠} S) RingHom N) \leftrightarrow {F ↾}_{S} \in ((M ↾_{𝑠} S) RingHom R))$
77	71 76	mpbid	$⊢ φ \to {F ↾}_{S} \in ((M ↾_{𝑠} S) RingHom R)$
78	77	ad2antrr	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to {F ↾}_{S} \in ((M ↾_{𝑠} S) RingHom R)$
79		eldifsni	$⊢ x \in ({Base}_{R} ∖ \{0_{R}\}) \to x \neq 0_{R}$
80	79	ad2antlr	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to x \neq 0_{R}$
81	68	adantr	$⊢ (((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \land a = 0_{M}) \to ({F ↾}_{S}) (a) = F (a)$
82		simpr	$⊢ (((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \land a = 0_{M}) \to a = 0_{M}$
83	82	fveq2d	$⊢ (((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \land a = 0_{M}) \to ({F ↾}_{S}) (a) = ({F ↾}_{S}) (0_{M})$
84	69 43	subrg0	$⊢ S \in SubRing (M) \to 0_{M} = 0_{(M ↾_{𝑠} S)}$
85	7 84	syl	$⊢ φ \to 0_{M} = 0_{(M ↾_{𝑠} S)}$
86	85	fveq2d	$⊢ φ \to ({F ↾}_{S}) (0_{M}) = ({F ↾}_{S}) (0_{(M ↾_{𝑠} S)})$
87		rhmghm	$⊢ {F ↾}_{S} \in ((M ↾_{𝑠} S) RingHom R) \to {F ↾}_{S} \in ((M ↾_{𝑠} S) GrpHom R)$
88		eqid	$⊢ 0_{(M ↾_{𝑠} S)} = 0_{(M ↾_{𝑠} S)}$
89	88 52	ghmid	$⊢ {F ↾}_{S} \in ((M ↾_{𝑠} S) GrpHom R) \to ({F ↾}_{S}) (0_{(M ↾_{𝑠} S)}) = 0_{R}$
90	77 87 89	3syl	$⊢ φ \to ({F ↾}_{S}) (0_{(M ↾_{𝑠} S)}) = 0_{R}$
91	86 90	eqtrd	$⊢ φ \to ({F ↾}_{S}) (0_{M}) = 0_{R}$
92	91	ad3antrrr	$⊢ (((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \land a = 0_{M}) \to ({F ↾}_{S}) (0_{M}) = 0_{R}$
93	83 92	eqtrd	$⊢ (((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \land a = 0_{M}) \to ({F ↾}_{S}) (a) = 0_{R}$
94		simplrr	$⊢ (((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \land a = 0_{M}) \to F (a) = x$
95	81 93 94	3eqtr3rd	$⊢ (((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \land a = 0_{M}) \to x = 0_{R}$
96	80 95	mteqand	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to a \neq 0_{M}$
97	4	ad2antrr	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to S \in SubDRing (M)$
98		eqid	$⊢ Unit (M ↾_{𝑠} S) = Unit (M ↾_{𝑠} S)$
99	69 43 98	sdrgunit	$⊢ S \in SubDRing (M) \to (a \in Unit (M ↾_{𝑠} S) \leftrightarrow (a \in S \land a \neq 0_{M}))$
100	97 99	syl	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to (a \in Unit (M ↾_{𝑠} S) \leftrightarrow (a \in S \land a \neq 0_{M}))$
101	67 96 100	mpbir2and	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to a \in Unit (M ↾_{𝑠} S)$
102		elrhmunit	$⊢ ({F ↾}_{S} \in ((M ↾_{𝑠} S) RingHom R) \land a \in Unit (M ↾_{𝑠} S)) \to ({F ↾}_{S}) (a) \in Unit (R)$
103	78 101 102	syl2anc	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to ({F ↾}_{S}) (a) \in Unit (R)$
104	68 103	eqeltrrd	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to F (a) \in Unit (R)$
105	66 104	eqeltrrd	$⊢ ((φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \land (a \in S \land F (a) = x)) \to x \in Unit (R)$
106	65 105	rexlimddv	$⊢ (φ \land x \in ({Base}_{R} ∖ \{0_{R}\})) \to x \in Unit (R)$
107	59 106	eqelssd	$⊢ φ \to Unit (R) = {Base}_{R} ∖ \{0_{R}\}$
108	12 13 52	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = {Base}_{R} ∖ \{0_{R}\})$
109	11 107 108	sylanbrc	$⊢ φ \to R \in DivRing$

Metamath Proof Explorer

Theorem imadrhmcl

Proof