Metamath Proof Explorer


Theorem ringmneg1

Description: Negation of a product in a ring. ( mulneg1 analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014)

Ref Expression
Hypotheses ringneglmul.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
ringneglmul.t โŠข ยท = ( .r โ€˜ ๐‘… )
ringneglmul.n โŠข ๐‘ = ( invg โ€˜ ๐‘… )
ringneglmul.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
ringneglmul.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
ringneglmul.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
Assertion ringmneg1 ( ๐œ‘ โ†’ ( ( ๐‘ โ€˜ ๐‘‹ ) ยท ๐‘Œ ) = ( ๐‘ โ€˜ ( ๐‘‹ ยท ๐‘Œ ) ) )

Proof

Step Hyp Ref Expression
1 ringneglmul.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
2 ringneglmul.t โŠข ยท = ( .r โ€˜ ๐‘… )
3 ringneglmul.n โŠข ๐‘ = ( invg โ€˜ ๐‘… )
4 ringneglmul.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
5 ringneglmul.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
6 ringneglmul.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
7 ringgrp โŠข ( ๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ Grp )
8 4 7 syl โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Grp )
9 eqid โŠข ( 1r โ€˜ ๐‘… ) = ( 1r โ€˜ ๐‘… )
10 1 9 ringidcl โŠข ( ๐‘… โˆˆ Ring โ†’ ( 1r โ€˜ ๐‘… ) โˆˆ ๐ต )
11 4 10 syl โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐‘… ) โˆˆ ๐ต )
12 1 3 grpinvcl โŠข ( ( ๐‘… โˆˆ Grp โˆง ( 1r โ€˜ ๐‘… ) โˆˆ ๐ต ) โ†’ ( ๐‘ โ€˜ ( 1r โ€˜ ๐‘… ) ) โˆˆ ๐ต )
13 8 11 12 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘ โ€˜ ( 1r โ€˜ ๐‘… ) ) โˆˆ ๐ต )
14 1 2 ringass โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ( ๐‘ โ€˜ ( 1r โ€˜ ๐‘… ) ) โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ( ( ๐‘ โ€˜ ( 1r โ€˜ ๐‘… ) ) ยท ๐‘‹ ) ยท ๐‘Œ ) = ( ( ๐‘ โ€˜ ( 1r โ€˜ ๐‘… ) ) ยท ( ๐‘‹ ยท ๐‘Œ ) ) )
15 4 13 5 6 14 syl13anc โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ โ€˜ ( 1r โ€˜ ๐‘… ) ) ยท ๐‘‹ ) ยท ๐‘Œ ) = ( ( ๐‘ โ€˜ ( 1r โ€˜ ๐‘… ) ) ยท ( ๐‘‹ ยท ๐‘Œ ) ) )
16 1 2 9 3 4 5 ringnegl โŠข ( ๐œ‘ โ†’ ( ( ๐‘ โ€˜ ( 1r โ€˜ ๐‘… ) ) ยท ๐‘‹ ) = ( ๐‘ โ€˜ ๐‘‹ ) )
17 16 oveq1d โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ โ€˜ ( 1r โ€˜ ๐‘… ) ) ยท ๐‘‹ ) ยท ๐‘Œ ) = ( ( ๐‘ โ€˜ ๐‘‹ ) ยท ๐‘Œ ) )
18 1 2 ringcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ต )
19 4 5 6 18 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ๐ต )
20 1 2 9 3 4 19 ringnegl โŠข ( ๐œ‘ โ†’ ( ( ๐‘ โ€˜ ( 1r โ€˜ ๐‘… ) ) ยท ( ๐‘‹ ยท ๐‘Œ ) ) = ( ๐‘ โ€˜ ( ๐‘‹ ยท ๐‘Œ ) ) )
21 15 17 20 3eqtr3d โŠข ( ๐œ‘ โ†’ ( ( ๐‘ โ€˜ ๐‘‹ ) ยท ๐‘Œ ) = ( ๐‘ โ€˜ ( ๐‘‹ ยท ๐‘Œ ) ) )