This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 
|- .|| = ( ||r ` R )
dvdsrspss.x 
|- ( ph -> X e. B )
dvdsrspss.y 
|- ( ph -> Y e. B )
dvdsruassoi.1 
|- U = ( Unit ` R )
dvdsruassoi.2 
|- .x. = ( .r ` R )
dvdsruasso.r 
|- ( ph -> R e. IDomn )
dvdsruasso2.1 
|- .1. = ( 1r ` R )
Assertion dvdsruasso2 
|- ( ph -> ( ( X .|| Y /\ Y .|| X ) <-> E. u e. U E. v e. U ( ( u .x. X ) = Y /\ ( v .x. Y ) = X /\ ( u .x. v ) = .1. ) ) )

Proof

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