dvdsruasso2

Description: A reformulation of dvdsruasso . (Proposed by Gerard Lang, 28-May-2025.) (Contributed by Thiery Arnoux, 29-May-2025)

	Ref	Expression
Hypotheses	dvdsrspss.b	$⊢ B = {Base}_{R}$
	dvdsrspss.k	$⊢ K = RSpan (R)$
	dvdsrspss.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
	dvdsrspss.x	$⊢ φ \to X \in B$
	dvdsrspss.y	$⊢ φ \to Y \in B$
	dvdsruassoi.1	$⊢ U = Unit (R)$
	dvdsruassoi.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	dvdsruasso.r	$⊢ φ \to R \in IDomn$
	dvdsruasso2.1	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	dvdsruasso2	$⊢ φ \to ((X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X) \leftrightarrow \exists u \in U \exists v \in U (u \underset{˙}{\cdot} X = Y \land v \underset{˙}{\cdot} Y = X \land u \underset{˙}{\cdot} v = \underset{˙}{1}))$

Proof

Step	Hyp	Ref	Expression
1		dvdsrspss.b	$⊢ B = {Base}_{R}$
2		dvdsrspss.k	$⊢ K = RSpan (R)$
3		dvdsrspss.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
4		dvdsrspss.x	$⊢ φ \to X \in B$
5		dvdsrspss.y	$⊢ φ \to Y \in B$
6		dvdsruassoi.1	$⊢ U = Unit (R)$
7		dvdsruassoi.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		dvdsruasso.r	$⊢ φ \to R \in IDomn$
9		dvdsruasso2.1	$⊢ \underset{˙}{1} = 1_{R}$
10	1 2 3 4 5 6 7 8	dvdsruasso	$⊢ φ \to ((X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X) \leftrightarrow \exists u \in U u \underset{˙}{\cdot} X = Y)$
11		oveq1	$⊢ v = {inv}_{r} (R) (u) \to v \underset{˙}{\cdot} Y = {inv}_{r} (R) (u) \underset{˙}{\cdot} Y$
12	11	eqeq1d	$⊢ v = {inv}_{r} (R) (u) \to (v \underset{˙}{\cdot} Y = X \leftrightarrow {inv}_{r} (R) (u) \underset{˙}{\cdot} Y = X)$
13		oveq2	$⊢ v = {inv}_{r} (R) (u) \to u \underset{˙}{\cdot} v = u \underset{˙}{\cdot} {inv}_{r} (R) (u)$
14	13	eqeq1d	$⊢ v = {inv}_{r} (R) (u) \to (u \underset{˙}{\cdot} v = \underset{˙}{1} \leftrightarrow u \underset{˙}{\cdot} {inv}_{r} (R) (u) = \underset{˙}{1})$
15	12 14	3anbi23d	$⊢ v = {inv}_{r} (R) (u) \to ((u \underset{˙}{\cdot} X = Y \land v \underset{˙}{\cdot} Y = X \land u \underset{˙}{\cdot} v = \underset{˙}{1}) \leftrightarrow (u \underset{˙}{\cdot} X = Y \land {inv}_{r} (R) (u) \underset{˙}{\cdot} Y = X \land u \underset{˙}{\cdot} {inv}_{r} (R) (u) = \underset{˙}{1}))$
16	8	idomringd	$⊢ φ \to R \in Ring$
17	16	ad2antrr	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to R \in Ring$
18		simplr	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to u \in U$
19		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
20	6 19	unitinvcl	$⊢ (R \in Ring \land u \in U) \to {inv}_{r} (R) (u) \in U$
21	17 18 20	syl2anc	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to {inv}_{r} (R) (u) \in U$
22		simpr	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to u \underset{˙}{\cdot} X = Y$
23	22	oveq2d	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to {inv}_{r} (R) (u) \underset{˙}{\cdot} (u \underset{˙}{\cdot} X) = {inv}_{r} (R) (u) \underset{˙}{\cdot} Y$
24	8	idomcringd	$⊢ φ \to R \in CRing$
25	24	ad2antrr	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to R \in CRing$
26	1 6	unitcl	$⊢ {inv}_{r} (R) (u) \in U \to {inv}_{r} (R) (u) \in B$
27	21 26	syl	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to {inv}_{r} (R) (u) \in B$
28	1 6	unitcl	$⊢ u \in U \to u \in B$
29	18 28	syl	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to u \in B$
30	1 7 25 27 29	crngcomd	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to {inv}_{r} (R) (u) \underset{˙}{\cdot} u = u \underset{˙}{\cdot} {inv}_{r} (R) (u)$
31	6 19 7 9	unitrinv	$⊢ (R \in Ring \land u \in U) \to u \underset{˙}{\cdot} {inv}_{r} (R) (u) = \underset{˙}{1}$
32	17 18 31	syl2anc	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to u \underset{˙}{\cdot} {inv}_{r} (R) (u) = \underset{˙}{1}$
33	30 32	eqtrd	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to {inv}_{r} (R) (u) \underset{˙}{\cdot} u = \underset{˙}{1}$
34	33	oveq1d	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to ({inv}_{r} (R) (u) \underset{˙}{\cdot} u) \underset{˙}{\cdot} X = \underset{˙}{1} \underset{˙}{\cdot} X$
35	4	ad2antrr	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to X \in B$
36	1 7 17 27 29 35	ringassd	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to ({inv}_{r} (R) (u) \underset{˙}{\cdot} u) \underset{˙}{\cdot} X = {inv}_{r} (R) (u) \underset{˙}{\cdot} (u \underset{˙}{\cdot} X)$
37	1 7 9 17 35	ringlidmd	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to \underset{˙}{1} \underset{˙}{\cdot} X = X$
38	34 36 37	3eqtr3d	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to {inv}_{r} (R) (u) \underset{˙}{\cdot} (u \underset{˙}{\cdot} X) = X$
39	23 38	eqtr3d	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to {inv}_{r} (R) (u) \underset{˙}{\cdot} Y = X$
40	22 39 32	3jca	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to (u \underset{˙}{\cdot} X = Y \land {inv}_{r} (R) (u) \underset{˙}{\cdot} Y = X \land u \underset{˙}{\cdot} {inv}_{r} (R) (u) = \underset{˙}{1})$
41	15 21 40	rspcedvdw	$⊢ ((φ \land u \in U) \land u \underset{˙}{\cdot} X = Y) \to \exists v \in U (u \underset{˙}{\cdot} X = Y \land v \underset{˙}{\cdot} Y = X \land u \underset{˙}{\cdot} v = \underset{˙}{1})$
42		simpr1	$⊢ (((φ \land u \in U) \land v \in U) \land (u \underset{˙}{\cdot} X = Y \land v \underset{˙}{\cdot} Y = X \land u \underset{˙}{\cdot} v = \underset{˙}{1})) \to u \underset{˙}{\cdot} X = Y$
43	42	r19.29an	$⊢ ((φ \land u \in U) \land \exists v \in U (u \underset{˙}{\cdot} X = Y \land v \underset{˙}{\cdot} Y = X \land u \underset{˙}{\cdot} v = \underset{˙}{1})) \to u \underset{˙}{\cdot} X = Y$
44	41 43	impbida	$⊢ (φ \land u \in U) \to (u \underset{˙}{\cdot} X = Y \leftrightarrow \exists v \in U (u \underset{˙}{\cdot} X = Y \land v \underset{˙}{\cdot} Y = X \land u \underset{˙}{\cdot} v = \underset{˙}{1}))$
45	44	rexbidva	$⊢ φ \to (\exists u \in U u \underset{˙}{\cdot} X = Y \leftrightarrow \exists u \in U \exists v \in U (u \underset{˙}{\cdot} X = Y \land v \underset{˙}{\cdot} Y = X \land u \underset{˙}{\cdot} v = \underset{˙}{1}))$
46	10 45	bitrd	$⊢ φ \to ((X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X) \leftrightarrow \exists u \in U \exists v \in U (u \underset{˙}{\cdot} X = Y \land v \underset{˙}{\cdot} Y = X \land u \underset{˙}{\cdot} v = \underset{˙}{1}))$

Metamath Proof Explorer

Theorem dvdsruasso2

Proof