# Metamath Proof Explorer

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 )`
`|- .+ = ( +g ` R )`
`|- ( ( 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 )`
` |-  .+ = ( +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 ) ) )`
` |-  .+ = ( +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 ) )`
` |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` X ) = ( .* ` X ) )`
` |-  ( Y e. B -> ( ( *rf ` R ) ` Y ) = ( .* ` Y ) )`
` |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( *rf ` R ) ` Y ) = ( .* ` Y ) )`
` |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( ( ( *rf ` R ) ` X ) .+ ( ( *rf ` R ) ` Y ) ) = ( ( .* ` X ) .+ ( .* ` Y ) ) )`
` |-  ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( .* ` ( X .+ Y ) ) = ( ( .* ` X ) .+ ( .* ` Y ) ) )`