rngosn3

Description: Obsolete as of 25-Jan-2020. Use ring1zr or srg1zr instead. The only unital ring with a base set consisting in one element is the zero ring. (Contributed by FL, 13-Feb-2010) (Proof shortened by Mario Carneiro, 30-Apr-2015) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	on1el3.1	$⊢ G = 1^{st} (R)$
	on1el3.2	$⊢ X = ran G$
Assertion	rngosn3	$⊢ (R \in RingOps \land A \in B) \to (X = \{A\} \leftrightarrow R = ⟨\{⟨⟨A, A⟩, A⟩\}, \{⟨⟨A, A⟩, A⟩\}⟩)$

Proof

Step	Hyp	Ref	Expression
1		on1el3.1	$⊢ G = 1^{st} (R)$
2		on1el3.2	$⊢ X = ran G$
3	1	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$
4	2	grpofo	$⊢ G \in GrpOp \to G : X \times X \underset{onto}{⟶} X$
5		fof	$⊢ G : X \times X \underset{onto}{⟶} X \to G : X \times X ⟶ X$
6	3 4 5	3syl	$⊢ R \in RingOps \to G : X \times X ⟶ X$
7	6	adantr	$⊢ (R \in RingOps \land A \in B) \to G : X \times X ⟶ X$
8		id	$⊢ X = \{A\} \to X = \{A\}$
9	8	sqxpeqd	$⊢ X = \{A\} \to X \times X = \{A\} \times \{A\}$
10	9 8	feq23d	$⊢ X = \{A\} \to (G : X \times X ⟶ X \leftrightarrow G : \{A\} \times \{A\} ⟶ \{A\})$
11	7 10	syl5ibcom	$⊢ (R \in RingOps \land A \in B) \to (X = \{A\} \to G : \{A\} \times \{A\} ⟶ \{A\})$
12	7	fdmd	$⊢ (R \in RingOps \land A \in B) \to dom G = X \times X$
13	12	eqcomd	$⊢ (R \in RingOps \land A \in B) \to X \times X = dom G$
14		fdm	$⊢ G : \{A\} \times \{A\} ⟶ \{A\} \to dom G = \{A\} \times \{A\}$
15	14	eqeq2d	$⊢ G : \{A\} \times \{A\} ⟶ \{A\} \to (X \times X = dom G \leftrightarrow X \times X = \{A\} \times \{A\})$
16	13 15	syl5ibcom	$⊢ (R \in RingOps \land A \in B) \to (G : \{A\} \times \{A\} ⟶ \{A\} \to X \times X = \{A\} \times \{A\})$
17		xpid11	$⊢ X \times X = \{A\} \times \{A\} \leftrightarrow X = \{A\}$
18	16 17	imbitrdi	$⊢ (R \in RingOps \land A \in B) \to (G : \{A\} \times \{A\} ⟶ \{A\} \to X = \{A\})$
19	11 18	impbid	$⊢ (R \in RingOps \land A \in B) \to (X = \{A\} \leftrightarrow G : \{A\} \times \{A\} ⟶ \{A\})$
20		simpr	$⊢ (R \in RingOps \land A \in B) \to A \in B$
21		xpsng	$⊢ (A \in B \land A \in B) \to \{A\} \times \{A\} = \{⟨A, A⟩\}$
22	20 21	sylancom	$⊢ (R \in RingOps \land A \in B) \to \{A\} \times \{A\} = \{⟨A, A⟩\}$
23	22	feq2d	$⊢ (R \in RingOps \land A \in B) \to (G : \{A\} \times \{A\} ⟶ \{A\} \leftrightarrow G : \{⟨A, A⟩\} ⟶ \{A\})$
24		opex	$⊢ ⟨A, A⟩ \in V$
25		fsng	$⊢ (⟨A, A⟩ \in V \land A \in B) \to (G : \{⟨A, A⟩\} ⟶ \{A\} \leftrightarrow G = \{⟨⟨A, A⟩, A⟩\})$
26	24 20 25	sylancr	$⊢ (R \in RingOps \land A \in B) \to (G : \{⟨A, A⟩\} ⟶ \{A\} \leftrightarrow G = \{⟨⟨A, A⟩, A⟩\})$
27	19 23 26	3bitrd	$⊢ (R \in RingOps \land A \in B) \to (X = \{A\} \leftrightarrow G = \{⟨⟨A, A⟩, A⟩\})$
28	1	eqeq1i	$⊢ G = \{⟨⟨A, A⟩, A⟩\} \leftrightarrow 1^{st} (R) = \{⟨⟨A, A⟩, A⟩\}$
29	27 28	bitrdi	$⊢ (R \in RingOps \land A \in B) \to (X = \{A\} \leftrightarrow 1^{st} (R) = \{⟨⟨A, A⟩, A⟩\})$
30	29	anbi1d	$⊢ (R \in RingOps \land A \in B) \to ((X = \{A\} \land 2^{nd} (R) = \{⟨⟨A, A⟩, A⟩\}) \leftrightarrow (1^{st} (R) = \{⟨⟨A, A⟩, A⟩\} \land 2^{nd} (R) = \{⟨⟨A, A⟩, A⟩\}))$
31		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
32	1 31 2	rngosm	$⊢ R \in RingOps \to 2^{nd} (R) : X \times X ⟶ X$
33	32	adantr	$⊢ (R \in RingOps \land A \in B) \to 2^{nd} (R) : X \times X ⟶ X$
34	9 8	feq23d	$⊢ X = \{A\} \to (2^{nd} (R) : X \times X ⟶ X \leftrightarrow 2^{nd} (R) : \{A\} \times \{A\} ⟶ \{A\})$
35	33 34	syl5ibcom	$⊢ (R \in RingOps \land A \in B) \to (X = \{A\} \to 2^{nd} (R) : \{A\} \times \{A\} ⟶ \{A\})$
36	22	feq2d	$⊢ (R \in RingOps \land A \in B) \to (2^{nd} (R) : \{A\} \times \{A\} ⟶ \{A\} \leftrightarrow 2^{nd} (R) : \{⟨A, A⟩\} ⟶ \{A\})$
37		fsng	$⊢ (⟨A, A⟩ \in V \land A \in B) \to (2^{nd} (R) : \{⟨A, A⟩\} ⟶ \{A\} \leftrightarrow 2^{nd} (R) = \{⟨⟨A, A⟩, A⟩\})$
38	24 20 37	sylancr	$⊢ (R \in RingOps \land A \in B) \to (2^{nd} (R) : \{⟨A, A⟩\} ⟶ \{A\} \leftrightarrow 2^{nd} (R) = \{⟨⟨A, A⟩, A⟩\})$
39	36 38	bitrd	$⊢ (R \in RingOps \land A \in B) \to (2^{nd} (R) : \{A\} \times \{A\} ⟶ \{A\} \leftrightarrow 2^{nd} (R) = \{⟨⟨A, A⟩, A⟩\})$
40	35 39	sylibd	$⊢ (R \in RingOps \land A \in B) \to (X = \{A\} \to 2^{nd} (R) = \{⟨⟨A, A⟩, A⟩\})$
41	40	pm4.71d	$⊢ (R \in RingOps \land A \in B) \to (X = \{A\} \leftrightarrow (X = \{A\} \land 2^{nd} (R) = \{⟨⟨A, A⟩, A⟩\}))$
42		relrngo	$⊢ Rel RingOps$
43		df-rel	$⊢ Rel RingOps \leftrightarrow RingOps \subseteq V \times V$
44	42 43	mpbi	$⊢ RingOps \subseteq V \times V$
45	44	sseli	$⊢ R \in RingOps \to R \in (V \times V)$
46	45	adantr	$⊢ (R \in RingOps \land A \in B) \to R \in (V \times V)$
47		eqop	$⊢ R \in (V \times V) \to (R = ⟨\{⟨⟨A, A⟩, A⟩\}, \{⟨⟨A, A⟩, A⟩\}⟩ \leftrightarrow (1^{st} (R) = \{⟨⟨A, A⟩, A⟩\} \land 2^{nd} (R) = \{⟨⟨A, A⟩, A⟩\}))$
48	46 47	syl	$⊢ (R \in RingOps \land A \in B) \to (R = ⟨\{⟨⟨A, A⟩, A⟩\}, \{⟨⟨A, A⟩, A⟩\}⟩ \leftrightarrow (1^{st} (R) = \{⟨⟨A, A⟩, A⟩\} \land 2^{nd} (R) = \{⟨⟨A, A⟩, A⟩\}))$
49	30 41 48	3bitr4d	$⊢ (R \in RingOps \land A \in B) \to (X = \{A\} \leftrightarrow R = ⟨\{⟨⟨A, A⟩, A⟩\}, \{⟨⟨A, A⟩, A⟩\}⟩)$

Metamath Proof Explorer

Theorem rngosn3

Proof