Metamath Proof Explorer

Theorem srngadd

Description: The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses srngcl.i 
|- .* = ( *r ` R )
srngcl.b 
|- B = ( Base ` R )
srngadd.p 
|- .+ = ( +g ` R )
Assertion srngadd 
|- ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( .* ` ( X .+ Y ) ) = ( ( .* ` X ) .+ ( .* ` Y ) ) )

Proof

Step Hyp Ref Expression
1 srngcl.i 
 |-  .* = ( *r ` R )
2 srngcl.b 
 |-  B = ( Base ` R )
3 srngadd.p 
 |-  .+ = ( +g ` R )
4 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
5 eqid 
 |-  ( *rf ` R ) = ( *rf ` R )
6 4 5 srngrhm 
 |-  ( R e. *Ring -> ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) )
7 rhmghm 
 |-  ( ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) -> ( *rf ` R ) e. ( R GrpHom ( oppR ` R ) ) )
8 6 7 syl 
 |-  ( R e. *Ring -> ( *rf ` R ) e. ( R GrpHom ( oppR ` R ) ) )
9 4 3 oppradd 
 |-  .+ = ( +g ` ( oppR ` R ) )
10 2 3 9 ghmlin 
 |-  ( ( ( *rf ` R ) e. ( R GrpHom ( oppR ` R ) ) /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` ( X .+ Y ) ) = ( ( ( *rf ` R ) ` X ) .+ ( ( *rf ` R ) ` Y ) ) )
11 8 10 syl3an1 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` ( X .+ Y ) ) = ( ( ( *rf ` R ) ` X ) .+ ( ( *rf ` R ) ` Y ) ) )
12 srngring 
 |-  ( R e. *Ring -> R e. Ring )
13 2 3 ringacl 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
14 12 13 syl3an1 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
15 2 1 5 stafval 
 |-  ( ( X .+ Y ) e. B -> ( ( *rf ` R ) ` ( X .+ Y ) ) = ( .* ` ( X .+ Y ) ) )
16 14 15 syl 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` ( X .+ Y ) ) = ( .* ` ( X .+ Y ) ) )
17 2 1 5 stafval 
 |-  ( X e. B -> ( ( *rf ` R ) ` X ) = ( .* ` X ) )
18 17 3ad2ant2 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` X ) = ( .* ` X ) )
19 2 1 5 stafval 
 |-  ( Y e. B -> ( ( *rf ` R ) ` Y ) = ( .* ` Y ) )
20 19 3ad2ant3 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` Y ) = ( .* ` Y ) )
21 18 20 oveq12d 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( ( *rf ` R ) ` X ) .+ ( ( *rf ` R ) ` Y ) ) = ( ( .* ` X ) .+ ( .* ` Y ) ) )
22 11 16 21 3eqtr3d 
 |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( .* ` ( X .+ Y ) ) = ( ( .* ` X ) .+ ( .* ` Y ) ) )