Metamath Proof Explorer

Theorem o2timesd

Description: An element of a ring-like structure plus itself is two times the element. "Two" in such a structure is the sum of the unity element with itself. This (formerly) part of the proof for ringcom depends on the (right) distributivity and the existence of a (left) multiplicative identity only. (Contributed by Gérard Lang, 4-Dec-2014) (Revised by AV, 1-Feb-2025)

Ref Expression
Hypotheses o2timesd.e 
|- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
o2timesd.u 
|- ( ph -> .1. e. B )
o2timesd.i 
|- ( ph -> A. x e. B ( .1. .x. x ) = x )
o2timesd.x 
|- ( ph -> X e. B )
Assertion o2timesd 
|- ( ph -> ( X .+ X ) = ( ( .1. .+ .1. ) .x. X ) )

Proof

Step Hyp Ref Expression
1 o2timesd.e 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
2 o2timesd.u 
 |-  ( ph -> .1. e. B )
3 o2timesd.i 
 |-  ( ph -> A. x e. B ( .1. .x. x ) = x )
4 o2timesd.x 
 |-  ( ph -> X e. B )
5 oveq2 
 |-  ( x = X -> ( .1. .x. x ) = ( .1. .x. X ) )
6 id 
 |-  ( x = X -> x = X )
7 5 6 eqeq12d 
 |-  ( x = X -> ( ( .1. .x. x ) = x <-> ( .1. .x. X ) = X ) )
8 7 rspcva 
 |-  ( ( X e. B /\ A. x e. B ( .1. .x. x ) = x ) -> ( .1. .x. X ) = X )
9 8 eqcomd 
 |-  ( ( X e. B /\ A. x e. B ( .1. .x. x ) = x ) -> X = ( .1. .x. X ) )
10 4 3 9 syl2anc 
 |-  ( ph -> X = ( .1. .x. X ) )
11 10 10 oveq12d 
 |-  ( ph -> ( X .+ X ) = ( ( .1. .x. X ) .+ ( .1. .x. X ) ) )
12 2 2 4 3jca 
 |-  ( ph -> ( .1. e. B /\ .1. e. B /\ X e. B ) )
13 oveq1 
 |-  ( x = .1. -> ( x .+ y ) = ( .1. .+ y ) )
14 13 oveq1d 
 |-  ( x = .1. -> ( ( x .+ y ) .x. z ) = ( ( .1. .+ y ) .x. z ) )
15 oveq1 
 |-  ( x = .1. -> ( x .x. z ) = ( .1. .x. z ) )
16 15 oveq1d 
 |-  ( x = .1. -> ( ( x .x. z ) .+ ( y .x. z ) ) = ( ( .1. .x. z ) .+ ( y .x. z ) ) )
17 14 16 eqeq12d 
 |-  ( x = .1. -> ( ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) <-> ( ( .1. .+ y ) .x. z ) = ( ( .1. .x. z ) .+ ( y .x. z ) ) ) )
18 oveq2 
 |-  ( y = .1. -> ( .1. .+ y ) = ( .1. .+ .1. ) )
19 18 oveq1d 
 |-  ( y = .1. -> ( ( .1. .+ y ) .x. z ) = ( ( .1. .+ .1. ) .x. z ) )
20 oveq1 
 |-  ( y = .1. -> ( y .x. z ) = ( .1. .x. z ) )
21 20 oveq2d 
 |-  ( y = .1. -> ( ( .1. .x. z ) .+ ( y .x. z ) ) = ( ( .1. .x. z ) .+ ( .1. .x. z ) ) )
22 19 21 eqeq12d 
 |-  ( y = .1. -> ( ( ( .1. .+ y ) .x. z ) = ( ( .1. .x. z ) .+ ( y .x. z ) ) <-> ( ( .1. .+ .1. ) .x. z ) = ( ( .1. .x. z ) .+ ( .1. .x. z ) ) ) )
23 oveq2 
 |-  ( z = X -> ( ( .1. .+ .1. ) .x. z ) = ( ( .1. .+ .1. ) .x. X ) )
24 oveq2 
 |-  ( z = X -> ( .1. .x. z ) = ( .1. .x. X ) )
25 24 24 oveq12d 
 |-  ( z = X -> ( ( .1. .x. z ) .+ ( .1. .x. z ) ) = ( ( .1. .x. X ) .+ ( .1. .x. X ) ) )
26 23 25 eqeq12d 
 |-  ( z = X -> ( ( ( .1. .+ .1. ) .x. z ) = ( ( .1. .x. z ) .+ ( .1. .x. z ) ) <-> ( ( .1. .+ .1. ) .x. X ) = ( ( .1. .x. X ) .+ ( .1. .x. X ) ) ) )
27 17 22 26 rspc3v 
 |-  ( ( .1. e. B /\ .1. e. B /\ X e. B ) -> ( A. x e. B A. y e. B A. z e. B ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) -> ( ( .1. .+ .1. ) .x. X ) = ( ( .1. .x. X ) .+ ( .1. .x. X ) ) ) )
28 12 1 27 sylc 
 |-  ( ph -> ( ( .1. .+ .1. ) .x. X ) = ( ( .1. .x. X ) .+ ( .1. .x. X ) ) )
29 11 28 eqtr4d 
 |-  ( ph -> ( X .+ X ) = ( ( .1. .+ .1. ) .x. X ) )