Metamath Proof Explorer

Theorem divsmulw

Description: Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. Later, when we prove precsex , we can eliminate the existence hypothesis (see divsmul ). (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Assertion divsmulw 
|- ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> ( ( A /su C ) = B <-> ( C x.s B ) = A ) )

Proof

Step Hyp Ref Expression
1 divsval 
 |-  ( ( A e. No /\ C e. No /\ C =/= 0s ) -> ( A /su C ) = ( iota_ y e. No ( C x.s y ) = A ) )
2 1 eqeq1d 
 |-  ( ( A e. No /\ C e. No /\ C =/= 0s ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) )
3 2 3expb 
 |-  ( ( A e. No /\ ( C e. No /\ C =/= 0s ) ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) )
4 3 3adant2 
 |-  ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) )
5 4 adantr 
 |-  ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> ( ( A /su C ) = B <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) )
6 simpl2 
 |-  ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> B e. No )
7 simp3l 
 |-  ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> C e. No )
8 simp3r 
 |-  ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> C =/= 0s )
9 simp1 
 |-  ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> A e. No )
10 7 8 9 3jca 
 |-  ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) -> ( C e. No /\ C =/= 0s /\ A e. No ) )
11 noreceuw 
 |-  ( ( ( C e. No /\ C =/= 0s /\ A e. No ) /\ E. x e. No ( C x.s x ) = 1s ) -> E! y e. No ( C x.s y ) = A )
12 10 11 sylan 
 |-  ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> E! y e. No ( C x.s y ) = A )
13 oveq2 
 |-  ( y = B -> ( C x.s y ) = ( C x.s B ) )
14 13 eqeq1d 
 |-  ( y = B -> ( ( C x.s y ) = A <-> ( C x.s B ) = A ) )
15 14 riota2 
 |-  ( ( B e. No /\ E! y e. No ( C x.s y ) = A ) -> ( ( C x.s B ) = A <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) )
16 6 12 15 syl2anc 
 |-  ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> ( ( C x.s B ) = A <-> ( iota_ y e. No ( C x.s y ) = A ) = B ) )
17 5 16 bitr4d 
 |-  ( ( ( A e. No /\ B e. No /\ ( C e. No /\ C =/= 0s ) ) /\ E. x e. No ( C x.s x ) = 1s ) -> ( ( A /su C ) = B <-> ( C x.s B ) = A ) )