fracfld

Description: The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025)

		Ref	Expression
	Hypothesis	fracfld.1	$⊢ φ \to R \in IDomn$
	Assertion	fracfld	$⊢ φ \to Frac (R) \in Field$

Proof

Step	Hyp	Ref	Expression
1		fracfld.1	$⊢ φ \to R \in IDomn$
2		fracval	$⊢ Frac (R) = R RLocal RLReg (R)$
3	1	idomdomd	$⊢ φ \to R \in Domn$
4		domnnzr	$⊢ R \in Domn \to R \in NzRing$
5		eqid	$⊢ 1_{R} = 1_{R}$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	5 6	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
8	3 4 7	3syl	$⊢ φ \to 1_{R} \neq 0_{R}$
9		fvex	$⊢ 1_{R} \in V$
10	9 9	op1st	$⊢ 1^{st} (⟨1_{R}, 1_{R}⟩) = 1_{R}$
11	10	a1i	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 1^{st} (⟨1_{R}, 1_{R}⟩) = 1_{R}$
12		fvex	$⊢ 0_{R} \in V$
13	12 9	op2nd	$⊢ 2^{nd} (⟨0_{R}, 1_{R}⟩) = 1_{R}$
14	13	a1i	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 2^{nd} (⟨0_{R}, 1_{R}⟩) = 1_{R}$
15	11 14	oveq12d	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 1^{st} (⟨1_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨0_{R}, 1_{R}⟩) = 1_{R} \cdot_{R} 1_{R}$
16		eqid	$⊢ {Base}_{R} = {Base}_{R}$
17		eqid	$⊢ \cdot_{R} = \cdot_{R}$
18	1	idomringd	$⊢ φ \to R \in Ring$
19	18	ad2antrr	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to R \in Ring$
20	16 5	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
21	19 20	syl	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 1_{R} \in {Base}_{R}$
22	16 17 5 19 21	ringlidmd	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 1_{R} \cdot_{R} 1_{R} = 1_{R}$
23	15 22	eqtrd	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 1^{st} (⟨1_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨0_{R}, 1_{R}⟩) = 1_{R}$
24	12 9	op1st	$⊢ 1^{st} (⟨0_{R}, 1_{R}⟩) = 0_{R}$
25	24	a1i	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 1^{st} (⟨0_{R}, 1_{R}⟩) = 0_{R}$
26	9 9	op2nd	$⊢ 2^{nd} (⟨1_{R}, 1_{R}⟩) = 1_{R}$
27	26	a1i	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 2^{nd} (⟨1_{R}, 1_{R}⟩) = 1_{R}$
28	25 27	oveq12d	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 1^{st} (⟨0_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨1_{R}, 1_{R}⟩) = 0_{R} \cdot_{R} 1_{R}$
29	18	ringgrpd	$⊢ φ \to R \in Grp$
30	16 6	grpidcl	$⊢ R \in Grp \to 0_{R} \in {Base}_{R}$
31	29 30	syl	$⊢ φ \to 0_{R} \in {Base}_{R}$
32	31	ad2antrr	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 0_{R} \in {Base}_{R}$
33	16 17 5 19 32	ringridmd	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 0_{R} \cdot_{R} 1_{R} = 0_{R}$
34	28 33	eqtrd	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to 1^{st} (⟨0_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨1_{R}, 1_{R}⟩) = 0_{R}$
35	23 34	oveq12d	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to (1^{st} (⟨1_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨0_{R}, 1_{R}⟩)) -_{R} (1^{st} (⟨0_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨1_{R}, 1_{R}⟩)) = 1_{R} -_{R} 0_{R}$
36	35	oveq2d	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to t \cdot_{R} ((1^{st} (⟨1_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨0_{R}, 1_{R}⟩)) -_{R} (1^{st} (⟨0_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨1_{R}, 1_{R}⟩))) = t \cdot_{R} (1_{R} -_{R} 0_{R})$
37		eqid	$⊢ -_{R} = -_{R}$
38		eqid	$⊢ RLReg (R) = RLReg (R)$
39	38 16	rrgss	$⊢ RLReg (R) \subseteq {Base}_{R}$
40	39	a1i	$⊢ (φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \to RLReg (R) \subseteq {Base}_{R}$
41	40	sselda	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to t \in {Base}_{R}$
42	16 17 37 19 41 21 32	ringsubdi	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to t \cdot_{R} (1_{R} -_{R} 0_{R}) = (t \cdot_{R} 1_{R}) -_{R} (t \cdot_{R} 0_{R})$
43	16 17 5 19 41	ringridmd	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to t \cdot_{R} 1_{R} = t$
44	16 17 6 19 41	ringrzd	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to t \cdot_{R} 0_{R} = 0_{R}$
45	43 44	oveq12d	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to (t \cdot_{R} 1_{R}) -_{R} (t \cdot_{R} 0_{R}) = t -_{R} 0_{R}$
46	29	ad2antrr	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to R \in Grp$
47	16 6 37	grpsubid1	$⊢ (R \in Grp \land t \in {Base}_{R}) \to t -_{R} 0_{R} = t$
48	46 41 47	syl2anc	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to t -_{R} 0_{R} = t$
49	45 48	eqtrd	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to (t \cdot_{R} 1_{R}) -_{R} (t \cdot_{R} 0_{R}) = t$
50	36 42 49	3eqtrd	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to t \cdot_{R} ((1^{st} (⟨1_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨0_{R}, 1_{R}⟩)) -_{R} (1^{st} (⟨0_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨1_{R}, 1_{R}⟩))) = t$
51	50	eqeq1d	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to (t \cdot_{R} ((1^{st} (⟨1_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨0_{R}, 1_{R}⟩)) -_{R} (1^{st} (⟨0_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨1_{R}, 1_{R}⟩))) = 0_{R} \leftrightarrow t = 0_{R})$
52	51	biimpa	$⊢ (((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \land t \cdot_{R} ((1^{st} (⟨1_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨0_{R}, 1_{R}⟩)) -_{R} (1^{st} (⟨0_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨1_{R}, 1_{R}⟩))) = 0_{R}) \to t = 0_{R}$
53		simpr	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to t \in RLReg (R)$
54	38 6	rrgnz	$⊢ R \in NzRing \to \neg 0_{R} \in RLReg (R)$
55	3 4 54	3syl	$⊢ φ \to \neg 0_{R} \in RLReg (R)$
56	55	ad2antrr	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to \neg 0_{R} \in RLReg (R)$
57		nelne2	$⊢ (t \in RLReg (R) \land \neg 0_{R} \in RLReg (R)) \to t \neq 0_{R}$
58	53 56 57	syl2anc	$⊢ ((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \to t \neq 0_{R}$
59	58	adantr	$⊢ (((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \land t \cdot_{R} ((1^{st} (⟨1_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨0_{R}, 1_{R}⟩)) -_{R} (1^{st} (⟨0_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨1_{R}, 1_{R}⟩))) = 0_{R}) \to t \neq 0_{R}$
60	52 59	pm2.21ddne	$⊢ (((φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \land t \in RLReg (R)) \land t \cdot_{R} ((1^{st} (⟨1_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨0_{R}, 1_{R}⟩)) -_{R} (1^{st} (⟨0_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨1_{R}, 1_{R}⟩))) = 0_{R}) \to 1_{R} = 0_{R}$
61		eqid	$⊢ R ~_{RL} RLReg (R) = R ~_{RL} RLReg (R)$
62		eqid	$⊢ {Base}_{R} \times RLReg (R) = {Base}_{R} \times RLReg (R)$
63	1	idomcringd	$⊢ φ \to R \in CRing$
64	16 38 6	isdomn6	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land {Base}_{R} ∖ \{0_{R}\} = RLReg (R))$
65	3 64	sylib	$⊢ φ \to (R \in NzRing \land {Base}_{R} ∖ \{0_{R}\} = RLReg (R))$
66	65	simprd	$⊢ φ \to {Base}_{R} ∖ \{0_{R}\} = RLReg (R)$
67		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
68	16 6 67	isdomn3	$⊢ R \in Domn \leftrightarrow (R \in Ring \land {Base}_{R} ∖ \{0_{R}\} \in SubMnd ({mulGrp}_{R}))$
69	3 68	sylib	$⊢ φ \to (R \in Ring \land {Base}_{R} ∖ \{0_{R}\} \in SubMnd ({mulGrp}_{R}))$
70	69	simprd	$⊢ φ \to {Base}_{R} ∖ \{0_{R}\} \in SubMnd ({mulGrp}_{R})$
71	66 70	eqeltrrd	$⊢ φ \to RLReg (R) \in SubMnd ({mulGrp}_{R})$
72	16 6 5 17 37 62 61 63 71	erler	$⊢ φ \to (R ~_{RL} RLReg (R)) Er ({Base}_{R} \times RLReg (R))$
73	18 20	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
74	5 38 18	1rrg	$⊢ φ \to 1_{R} \in RLReg (R)$
75	73 74	opelxpd	$⊢ φ \to ⟨1_{R}, 1_{R}⟩ \in ({Base}_{R} \times RLReg (R))$
76	72 75	erth	$⊢ φ \to (⟨1_{R}, 1_{R}⟩ (R ~_{RL} RLReg (R)) ⟨0_{R}, 1_{R}⟩ \leftrightarrow [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)))$
77	76	biimpar	$⊢ (φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \to ⟨1_{R}, 1_{R}⟩ (R ~_{RL} RLReg (R)) ⟨0_{R}, 1_{R}⟩$
78	16 61 40 6 17 37 77	erldi	$⊢ (φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \to \exists t \in RLReg (R) t \cdot_{R} ((1^{st} (⟨1_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨0_{R}, 1_{R}⟩)) -_{R} (1^{st} (⟨0_{R}, 1_{R}⟩) \cdot_{R} 2^{nd} (⟨1_{R}, 1_{R}⟩))) = 0_{R}$
79	60 78	r19.29a	$⊢ (φ \land [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))) \to 1_{R} = 0_{R}$
80	8 79	mteqand	$⊢ φ \to [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) \neq [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))$
81		eqid	$⊢ R RLocal RLReg (R) = R RLocal RLReg (R)$
82		eqid	$⊢ [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))$
83	6 5 81 61 63 71 82	rloc1r	$⊢ φ \to [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = 1_{(R RLocal RLReg (R))}$
84		eqid	$⊢ [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))$
85	6 5 81 61 63 71 84	rloc0g	$⊢ φ \to [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = 0_{(R RLocal RLReg (R))}$
86	80 83 85	3netr3d	$⊢ φ \to 1_{(R RLocal RLReg (R))} \neq 0_{(R RLocal RLReg (R))}$
87		oveq2	$⊢ y = [⟨b, a⟩] (R ~_{RL} RLReg (R)) \to x \cdot_{(R RLocal RLReg (R))} y = x \cdot_{(R RLocal RLReg (R))} [⟨b, a⟩] (R ~_{RL} RLReg (R))$
88	87	eqeq1d	$⊢ y = [⟨b, a⟩] (R ~_{RL} RLReg (R)) \to (x \cdot_{(R RLocal RLReg (R))} y = 1_{(R RLocal RLReg (R))} \leftrightarrow x \cdot_{(R RLocal RLReg (R))} [⟨b, a⟩] (R ~_{RL} RLReg (R)) = 1_{(R RLocal RLReg (R))})$
89		oveq1	$⊢ y = [⟨b, a⟩] (R ~_{RL} RLReg (R)) \to y \cdot_{(R RLocal RLReg (R))} x = [⟨b, a⟩] (R ~_{RL} RLReg (R)) \cdot_{(R RLocal RLReg (R))} x$
90	89	eqeq1d	$⊢ y = [⟨b, a⟩] (R ~_{RL} RLReg (R)) \to (y \cdot_{(R RLocal RLReg (R))} x = 1_{(R RLocal RLReg (R))} \leftrightarrow [⟨b, a⟩] (R ~_{RL} RLReg (R)) \cdot_{(R RLocal RLReg (R))} x = 1_{(R RLocal RLReg (R))})$
91	88 90	anbi12d	$⊢ y = [⟨b, a⟩] (R ~_{RL} RLReg (R)) \to ((x \cdot_{(R RLocal RLReg (R))} y = 1_{(R RLocal RLReg (R))} \land y \cdot_{(R RLocal RLReg (R))} x = 1_{(R RLocal RLReg (R))}) \leftrightarrow (x \cdot_{(R RLocal RLReg (R))} [⟨b, a⟩] (R ~_{RL} RLReg (R)) = 1_{(R RLocal RLReg (R))} \land [⟨b, a⟩] (R ~_{RL} RLReg (R)) \cdot_{(R RLocal RLReg (R))} x = 1_{(R RLocal RLReg (R))}))$
92		simplr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to b \in RLReg (R)$
93	39 92	sselid	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to b \in {Base}_{R}$
94		simpllr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to a \in {Base}_{R}$
95		simplr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to x = [⟨a, b⟩] (R ~_{RL} RLReg (R))$
96	72	ad5antr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to (R ~_{RL} RLReg (R)) Er ({Base}_{R} \times RLReg (R))$
97	18	ad5antr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to R \in Ring$
98	97 20	syl	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to 1_{R} \in {Base}_{R}$
99	16 17 6 97 98	ringlzd	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to 0_{R} \cdot_{R} 1_{R} = 0_{R}$
100		simpr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to a = 0_{R}$
101	100	oveq1d	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to a \cdot_{R} 1_{R} = 0_{R} \cdot_{R} 1_{R}$
102	93	adantr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to b \in {Base}_{R}$
103	16 17 6 97 102	ringlzd	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to 0_{R} \cdot_{R} b = 0_{R}$
104	99 101 103	3eqtr4d	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to a \cdot_{R} 1_{R} = 0_{R} \cdot_{R} b$
105	63	ad5antr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to R \in CRing$
106	94	adantr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to a \in {Base}_{R}$
107	31	ad5antr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to 0_{R} \in {Base}_{R}$
108	92	adantr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to b \in RLReg (R)$
109	74	ad5antr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to 1_{R} \in RLReg (R)$
110	16 17 61 105 106 107 108 109	fracerl	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to (⟨a, b⟩ (R ~_{RL} RLReg (R)) ⟨0_{R}, 1_{R}⟩ \leftrightarrow a \cdot_{R} 1_{R} = 0_{R} \cdot_{R} b)$
111	104 110	mpbird	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to ⟨a, b⟩ (R ~_{RL} RLReg (R)) ⟨0_{R}, 1_{R}⟩$
112	96 111	erthi	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to [⟨a, b⟩] (R ~_{RL} RLReg (R)) = [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))$
113	85	ad5antr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to [⟨0_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = 0_{(R RLocal RLReg (R))}$
114	95 112 113	3eqtrd	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to x = 0_{(R RLocal RLReg (R))}$
115		eldifsni	$⊢ x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\}) \to x \neq 0_{(R RLocal RLReg (R))}$
116	115	ad5antlr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to x \neq 0_{(R RLocal RLReg (R))}$
117	116	neneqd	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a = 0_{R}) \to \neg x = 0_{(R RLocal RLReg (R))}$
118	114 117	pm2.65da	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to \neg a = 0_{R}$
119	118	neqned	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to a \neq 0_{R}$
120	94 119	eldifsnd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to a \in ({Base}_{R} ∖ \{0_{R}\})$
121	66	ad4antr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to {Base}_{R} ∖ \{0_{R}\} = RLReg (R)$
122	120 121	eleqtrd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to a \in RLReg (R)$
123	93 122	opelxpd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to ⟨b, a⟩ \in ({Base}_{R} \times RLReg (R))$
124		ovex	$⊢ R ~_{RL} RLReg (R) \in V$
125	124	ecelqsi	$⊢ ⟨b, a⟩ \in ({Base}_{R} \times RLReg (R)) \to [⟨b, a⟩] (R ~_{RL} RLReg (R)) \in (({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R)))$
126	123 125	syl	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to [⟨b, a⟩] (R ~_{RL} RLReg (R)) \in (({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R)))$
127	39	a1i	$⊢ φ \to RLReg (R) \subseteq {Base}_{R}$
128	16 6 17 37 62 81 61 1 127	rlocbas	$⊢ φ \to ({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R)) = {Base}_{(R RLocal RLReg (R))}$
129	128	ad4antr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to ({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R)) = {Base}_{(R RLocal RLReg (R))}$
130	126 129	eleqtrd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to [⟨b, a⟩] (R ~_{RL} RLReg (R)) \in {Base}_{(R RLocal RLReg (R))}$
131		eqid	$⊢ {Base}_{(R RLocal RLReg (R))} = {Base}_{(R RLocal RLReg (R))}$
132		eqid	$⊢ \cdot_{(R RLocal RLReg (R))} = \cdot_{(R RLocal RLReg (R))}$
133		eqid	$⊢ +_{R} = +_{R}$
134	16 17 133 81 61 63 71	rloccring	$⊢ φ \to R RLocal RLReg (R) \in CRing$
135	134	ad4antr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to R RLocal RLReg (R) \in CRing$
136		simp-4r	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})$
137	136	eldifad	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to x \in {Base}_{(R RLocal RLReg (R))}$
138	131 132 135 137 130	crngcomd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to x \cdot_{(R RLocal RLReg (R))} [⟨b, a⟩] (R ~_{RL} RLReg (R)) = [⟨b, a⟩] (R ~_{RL} RLReg (R)) \cdot_{(R RLocal RLReg (R))} x$
139		simpr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to x = [⟨a, b⟩] (R ~_{RL} RLReg (R))$
140	139	oveq2d	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to [⟨b, a⟩] (R ~_{RL} RLReg (R)) \cdot_{(R RLocal RLReg (R))} x = [⟨b, a⟩] (R ~_{RL} RLReg (R)) \cdot_{(R RLocal RLReg (R))} [⟨a, b⟩] (R ~_{RL} RLReg (R))$
141	63	ad4antr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to R \in CRing$
142	71	ad4antr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to RLReg (R) \in SubMnd ({mulGrp}_{R})$
143	16 17 133 81 61 141 142 93 94 122 92 132	rlocmulval	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to [⟨b, a⟩] (R ~_{RL} RLReg (R)) \cdot_{(R RLocal RLReg (R))} [⟨a, b⟩] (R ~_{RL} RLReg (R)) = [⟨b \cdot_{R} a, a \cdot_{R} b⟩] (R ~_{RL} RLReg (R))$
144	72	ad4antr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to (R ~_{RL} RLReg (R)) Er ({Base}_{R} \times RLReg (R))$
145	16 17 141 93 94	crngcomd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to b \cdot_{R} a = a \cdot_{R} b$
146	18	ad4antr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to R \in Ring$
147	16 17 146 93 94	ringcld	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to b \cdot_{R} a \in {Base}_{R}$
148	16 17 5 146 147	ringridmd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to (b \cdot_{R} a) \cdot_{R} 1_{R} = b \cdot_{R} a$
149	16 17 146 94 93	ringcld	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to a \cdot_{R} b \in {Base}_{R}$
150	16 17 5 146 149	ringlidmd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to 1_{R} \cdot_{R} (a \cdot_{R} b) = a \cdot_{R} b$
151	145 148 150	3eqtr4d	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to (b \cdot_{R} a) \cdot_{R} 1_{R} = 1_{R} \cdot_{R} (a \cdot_{R} b)$
152	73	ad4antr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to 1_{R} \in {Base}_{R}$
153	94	adantr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to a \in {Base}_{R}$
154	31	ad5antr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to 0_{R} \in {Base}_{R}$
155	92	adantr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to b \in RLReg (R)$
156	66	ad5antr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to {Base}_{R} ∖ \{0_{R}\} = RLReg (R)$
157	155 156	eleqtrrd	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to b \in ({Base}_{R} ∖ \{0_{R}\})$
158	1	adantr	$⊢ (φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \to R \in IDomn$
159	158	ad4antr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to R \in IDomn$
160		simpr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to a \cdot_{R} b = 0_{R}$
161	146	adantr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to R \in Ring$
162	93	adantr	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to b \in {Base}_{R}$
163	16 17 6 161 162	ringlzd	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to 0_{R} \cdot_{R} b = 0_{R}$
164	160 163	eqtr4d	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to a \cdot_{R} b = 0_{R} \cdot_{R} b$
165	16 6 17 153 154 157 159 164	idomrcan	$⊢ (((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \land a \cdot_{R} b = 0_{R}) \to a = 0_{R}$
166	118 165	mtand	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to \neg a \cdot_{R} b = 0_{R}$
167	166	neqned	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to a \cdot_{R} b \neq 0_{R}$
168	149 167	eldifsnd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to a \cdot_{R} b \in ({Base}_{R} ∖ \{0_{R}\})$
169	168 121	eleqtrd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to a \cdot_{R} b \in RLReg (R)$
170	74	ad4antr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to 1_{R} \in RLReg (R)$
171	16 17 61 141 147 152 169 170	fracerl	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to (⟨b \cdot_{R} a, a \cdot_{R} b⟩ (R ~_{RL} RLReg (R)) ⟨1_{R}, 1_{R}⟩ \leftrightarrow (b \cdot_{R} a) \cdot_{R} 1_{R} = 1_{R} \cdot_{R} (a \cdot_{R} b))$
172	151 171	mpbird	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to ⟨b \cdot_{R} a, a \cdot_{R} b⟩ (R ~_{RL} RLReg (R)) ⟨1_{R}, 1_{R}⟩$
173	144 172	erthi	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to [⟨b \cdot_{R} a, a \cdot_{R} b⟩] (R ~_{RL} RLReg (R)) = [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))$
174	143 173	eqtrd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to [⟨b, a⟩] (R ~_{RL} RLReg (R)) \cdot_{(R RLocal RLReg (R))} [⟨a, b⟩] (R ~_{RL} RLReg (R)) = [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R))$
175	83	ad4antr	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to [⟨1_{R}, 1_{R}⟩] (R ~_{RL} RLReg (R)) = 1_{(R RLocal RLReg (R))}$
176	140 174 175	3eqtrd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to [⟨b, a⟩] (R ~_{RL} RLReg (R)) \cdot_{(R RLocal RLReg (R))} x = 1_{(R RLocal RLReg (R))}$
177	138 176	eqtrd	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to x \cdot_{(R RLocal RLReg (R))} [⟨b, a⟩] (R ~_{RL} RLReg (R)) = 1_{(R RLocal RLReg (R))}$
178	177 176	jca	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to (x \cdot_{(R RLocal RLReg (R))} [⟨b, a⟩] (R ~_{RL} RLReg (R)) = 1_{(R RLocal RLReg (R))} \land [⟨b, a⟩] (R ~_{RL} RLReg (R)) \cdot_{(R RLocal RLReg (R))} x = 1_{(R RLocal RLReg (R))})$
179	91 130 178	rspcedvdw	$⊢ ((((φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \land a \in {Base}_{R}) \land b \in RLReg (R)) \land x = [⟨a, b⟩] (R ~_{RL} RLReg (R))) \to \exists y \in {Base}_{(R RLocal RLReg (R))} (x \cdot_{(R RLocal RLReg (R))} y = 1_{(R RLocal RLReg (R))} \land y \cdot_{(R RLocal RLReg (R))} x = 1_{(R RLocal RLReg (R))})$
180	128	difeq1d	$⊢ φ \to (({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R))) ∖ \{0_{(R RLocal RLReg (R))}\} = {Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\}$
181	180	eleq2d	$⊢ φ \to (x \in ((({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R))) ∖ \{0_{(R RLocal RLReg (R))}\}) \leftrightarrow x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\}))$
182	181	biimpar	$⊢ (φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \to x \in ((({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R))) ∖ \{0_{(R RLocal RLReg (R))}\})$
183	182	eldifad	$⊢ (φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \to x \in (({Base}_{R} \times RLReg (R)) / (R ~_{RL} RLReg (R)))$
184	183	elrlocbasi	$⊢ (φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \to \exists a \in {Base}_{R} \exists b \in RLReg (R) x = [⟨a, b⟩] (R ~_{RL} RLReg (R))$
185	179 184	r19.29vva	$⊢ (φ \land x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\})) \to \exists y \in {Base}_{(R RLocal RLReg (R))} (x \cdot_{(R RLocal RLReg (R))} y = 1_{(R RLocal RLReg (R))} \land y \cdot_{(R RLocal RLReg (R))} x = 1_{(R RLocal RLReg (R))})$
186	185	ralrimiva	$⊢ φ \to \forall x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\}) \exists y \in {Base}_{(R RLocal RLReg (R))} (x \cdot_{(R RLocal RLReg (R))} y = 1_{(R RLocal RLReg (R))} \land y \cdot_{(R RLocal RLReg (R))} x = 1_{(R RLocal RLReg (R))})$
187		eqid	$⊢ 0_{(R RLocal RLReg (R))} = 0_{(R RLocal RLReg (R))}$
188		eqid	$⊢ 1_{(R RLocal RLReg (R))} = 1_{(R RLocal RLReg (R))}$
189		eqid	$⊢ Unit (R RLocal RLReg (R)) = Unit (R RLocal RLReg (R))$
190	134	crngringd	$⊢ φ \to R RLocal RLReg (R) \in Ring$
191	131 187 188 132 189 190	isdrng4	$⊢ φ \to (R RLocal RLReg (R) \in DivRing \leftrightarrow (1_{(R RLocal RLReg (R))} \neq 0_{(R RLocal RLReg (R))} \land \forall x \in ({Base}_{(R RLocal RLReg (R))} ∖ \{0_{(R RLocal RLReg (R))}\}) \exists y \in {Base}_{(R RLocal RLReg (R))} (x \cdot_{(R RLocal RLReg (R))} y = 1_{(R RLocal RLReg (R))} \land y \cdot_{(R RLocal RLReg (R))} x = 1_{(R RLocal RLReg (R))})))$
192	86 186 191	mpbir2and	$⊢ φ \to R RLocal RLReg (R) \in DivRing$
193		isfld	$⊢ R RLocal RLReg (R) \in Field \leftrightarrow (R RLocal RLReg (R) \in DivRing \land R RLocal RLReg (R) \in CRing)$
194	192 134 193	sylanbrc	$⊢ φ \to R RLocal RLReg (R) \in Field$
195	2 194	eqeltrid	$⊢ φ \to Frac (R) \in Field$

Metamath Proof Explorer

Theorem fracfld

Proof