Metamath Proof Explorer

Theorem sn-mulid2

Description: mulid2 without ax-mulcom . (Contributed by SN, 27-May-2024)

Ref Expression
Assertion sn-mulid2 
|- ( A e. CC -> ( 1 x. A ) = A )

Proof

Step Hyp Ref Expression
1 cnre 
 |-  ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
2 1cnd 
 |-  ( ( x e. RR /\ y e. RR ) -> 1 e. CC )
3 recn 
 |-  ( x e. RR -> x e. CC )
4 3 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> x e. CC )
5 ax-icn 
 |-  _i e. CC
6 5 a1i 
 |-  ( ( x e. RR /\ y e. RR ) -> _i e. CC )
7 recn 
 |-  ( y e. RR -> y e. CC )
8 7 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> y e. CC )
9 6 8 mulcld 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. y ) e. CC )
10 2 4 9 adddid 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 1 x. ( x + ( _i x. y ) ) ) = ( ( 1 x. x ) + ( 1 x. ( _i x. y ) ) ) )
11 remulid2 
 |-  ( x e. RR -> ( 1 x. x ) = x )
12 11 adantr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 1 x. x ) = x )
13 2 6 8 mulassd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( 1 x. _i ) x. y ) = ( 1 x. ( _i x. y ) ) )
14 sn-1ticom 
 |-  ( 1 x. _i ) = ( _i x. 1 )
15 14 oveq1i 
 |-  ( ( 1 x. _i ) x. y ) = ( ( _i x. 1 ) x. y )
16 15 a1i 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( 1 x. _i ) x. y ) = ( ( _i x. 1 ) x. y ) )
17 6 2 8 mulassd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( _i x. 1 ) x. y ) = ( _i x. ( 1 x. y ) ) )
18 remulid2 
 |-  ( y e. RR -> ( 1 x. y ) = y )
19 18 adantl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 1 x. y ) = y )
20 19 oveq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( _i x. ( 1 x. y ) ) = ( _i x. y ) )
21 16 17 20 3eqtrd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( 1 x. _i ) x. y ) = ( _i x. y ) )
22 13 21 eqtr3d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 1 x. ( _i x. y ) ) = ( _i x. y ) )
23 12 22 oveq12d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( 1 x. x ) + ( 1 x. ( _i x. y ) ) ) = ( x + ( _i x. y ) ) )
24 10 23 eqtrd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( 1 x. ( x + ( _i x. y ) ) ) = ( x + ( _i x. y ) ) )
25 oveq2 
 |-  ( A = ( x + ( _i x. y ) ) -> ( 1 x. A ) = ( 1 x. ( x + ( _i x. y ) ) ) )
26 id 
 |-  ( A = ( x + ( _i x. y ) ) -> A = ( x + ( _i x. y ) ) )
27 25 26 eqeq12d 
 |-  ( A = ( x + ( _i x. y ) ) -> ( ( 1 x. A ) = A <-> ( 1 x. ( x + ( _i x. y ) ) ) = ( x + ( _i x. y ) ) ) )
28 24 27 syl5ibrcom 
 |-  ( ( x e. RR /\ y e. RR ) -> ( A = ( x + ( _i x. y ) ) -> ( 1 x. A ) = A ) )
29 28 rexlimivv 
 |-  ( E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) -> ( 1 x. A ) = A )
30 1 29 syl 
 |-  ( A e. CC -> ( 1 x. A ) = A )