invrfval

Description: Multiplicative inverse function for a division ring. (Contributed by NM, 21-Sep-2011) (Revised by Mario Carneiro, 25-Dec-2014)

	Ref	Expression
Hypotheses	invrfval.u	$⊢ U = Unit (R)$
	invrfval.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} U$
	invrfval.i	$⊢ I = {inv}_{r} (R)$
Assertion	invrfval	$⊢ I = {inv}_{g} (G)$

Proof

Step	Hyp	Ref	Expression
1		invrfval.u	$⊢ U = Unit (R)$
2		invrfval.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} U$
3		invrfval.i	$⊢ I = {inv}_{r} (R)$
4		fveq2	$⊢ r = R \to {mulGrp}_{r} = {mulGrp}_{R}$
5		fveq2	$⊢ r = R \to Unit (r) = Unit (R)$
6	5 1	syl6eqr	$⊢ r = R \to Unit (r) = U$
7	4 6	oveq12d	$⊢ r = R \to {mulGrp}_{r} ↾_{𝑠} Unit (r) = {mulGrp}_{R} ↾_{𝑠} U$
8	7 2	syl6eqr	$⊢ r = R \to {mulGrp}_{r} ↾_{𝑠} Unit (r) = G$
9	8	fveq2d	$⊢ r = R \to {inv}_{g} ({mulGrp}_{r} ↾_{𝑠} Unit (r)) = {inv}_{g} (G)$
10		df-invr	$⊢ {inv}_{r} = (r \in V ⟼ {inv}_{g} ({mulGrp}_{r} ↾_{𝑠} Unit (r)))$
11		fvex	$⊢ {inv}_{g} (G) \in V$
12	9 10 11	fvmpt	$⊢ R \in V \to {inv}_{r} (R) = {inv}_{g} (G)$
13		fvprc	$⊢ \neg R \in V \to {inv}_{r} (R) = \emptyset$
14		base0	$⊢ \emptyset = {Base}_{\emptyset}$
15		eqid	$⊢ {inv}_{g} (\emptyset) = {inv}_{g} (\emptyset)$
16	14 15	grpinvfn	$⊢ {inv}_{g} (\emptyset) Fn \emptyset$
17		fn0	$⊢ {inv}_{g} (\emptyset) Fn \emptyset \leftrightarrow {inv}_{g} (\emptyset) = \emptyset$
18	16 17	mpbi	$⊢ {inv}_{g} (\emptyset) = \emptyset$
19	13 18	syl6eqr	$⊢ \neg R \in V \to {inv}_{r} (R) = {inv}_{g} (\emptyset)$
20		fvprc	$⊢ \neg R \in V \to {mulGrp}_{R} = \emptyset$
21	20	oveq1d	$⊢ \neg R \in V \to {mulGrp}_{R} ↾_{𝑠} U = \emptyset ↾_{𝑠} U$
22	2 21	syl5eq	$⊢ \neg R \in V \to G = \emptyset ↾_{𝑠} U$
23		ress0	$⊢ \emptyset ↾_{𝑠} U = \emptyset$
24	22 23	syl6eq	$⊢ \neg R \in V \to G = \emptyset$
25	24	fveq2d	$⊢ \neg R \in V \to {inv}_{g} (G) = {inv}_{g} (\emptyset)$
26	19 25	eqtr4d	$⊢ \neg R \in V \to {inv}_{r} (R) = {inv}_{g} (G)$
27	12 26	pm2.61i	$⊢ {inv}_{r} (R) = {inv}_{g} (G)$
28	3 27	eqtri	$⊢ I = {inv}_{g} (G)$

Metamath Proof Explorer

Theorem invrfval

Proof