Metamath Proof Explorer


Theorem mulgass3

Description: An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses mulgass3.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
mulgass3.m โŠข ยท = ( .g โ€˜ ๐‘… )
mulgass3.t โŠข ร— = ( .r โ€˜ ๐‘… )
Assertion mulgass3 ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘‹ ร— ( ๐‘ ยท ๐‘Œ ) ) = ( ๐‘ ยท ( ๐‘‹ ร— ๐‘Œ ) ) )

Proof

Step Hyp Ref Expression
1 mulgass3.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
2 mulgass3.m โŠข ยท = ( .g โ€˜ ๐‘… )
3 mulgass3.t โŠข ร— = ( .r โ€˜ ๐‘… )
4 eqid โŠข ( oppr โ€˜ ๐‘… ) = ( oppr โ€˜ ๐‘… )
5 4 opprring โŠข ( ๐‘… โˆˆ Ring โ†’ ( oppr โ€˜ ๐‘… ) โˆˆ Ring )
6 5 adantr โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( oppr โ€˜ ๐‘… ) โˆˆ Ring )
7 simpr1 โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐‘ โˆˆ โ„ค )
8 simpr3 โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐‘Œ โˆˆ ๐ต )
9 simpr2 โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐‘‹ โˆˆ ๐ต )
10 4 1 opprbas โŠข ๐ต = ( Base โ€˜ ( oppr โ€˜ ๐‘… ) )
11 eqid โŠข ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) = ( .g โ€˜ ( oppr โ€˜ ๐‘… ) )
12 eqid โŠข ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) = ( .r โ€˜ ( oppr โ€˜ ๐‘… ) )
13 10 11 12 mulgass2 โŠข ( ( ( oppr โ€˜ ๐‘… ) โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) = ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ( ๐‘Œ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) ) )
14 6 7 8 9 13 syl13anc โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) = ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ( ๐‘Œ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) ) )
15 1 3 4 12 opprmul โŠข ( ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) = ( ๐‘‹ ร— ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) )
16 1 3 4 12 opprmul โŠข ( ๐‘Œ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) = ( ๐‘‹ ร— ๐‘Œ )
17 16 oveq2i โŠข ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ( ๐‘Œ ( .r โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘‹ ) ) = ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ( ๐‘‹ ร— ๐‘Œ ) )
18 14 15 17 3eqtr3g โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘‹ ร— ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) ) = ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ( ๐‘‹ ร— ๐‘Œ ) ) )
19 1 a1i โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐ต = ( Base โ€˜ ๐‘… ) )
20 10 a1i โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐ต = ( Base โ€˜ ( oppr โ€˜ ๐‘… ) ) )
21 ssv โŠข ๐ต โŠ† V
22 21 a1i โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ๐ต โŠ† V )
23 ovexd โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง ( ๐‘ฅ โˆˆ V โˆง ๐‘ฆ โˆˆ V ) ) โ†’ ( ๐‘ฅ ( +g โ€˜ ๐‘… ) ๐‘ฆ ) โˆˆ V )
24 eqid โŠข ( +g โ€˜ ๐‘… ) = ( +g โ€˜ ๐‘… )
25 4 24 oppradd โŠข ( +g โ€˜ ๐‘… ) = ( +g โ€˜ ( oppr โ€˜ ๐‘… ) )
26 25 oveqi โŠข ( ๐‘ฅ ( +g โ€˜ ๐‘… ) ๐‘ฆ ) = ( ๐‘ฅ ( +g โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘ฆ )
27 26 a1i โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โˆง ( ๐‘ฅ โˆˆ V โˆง ๐‘ฆ โˆˆ V ) ) โ†’ ( ๐‘ฅ ( +g โ€˜ ๐‘… ) ๐‘ฆ ) = ( ๐‘ฅ ( +g โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘ฆ ) )
28 2 11 19 20 22 23 27 mulgpropd โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ยท = ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) )
29 28 oveqd โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘ ยท ๐‘Œ ) = ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) )
30 29 oveq2d โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘‹ ร— ( ๐‘ ยท ๐‘Œ ) ) = ( ๐‘‹ ร— ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ๐‘Œ ) ) )
31 28 oveqd โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘ ยท ( ๐‘‹ ร— ๐‘Œ ) ) = ( ๐‘ ( .g โ€˜ ( oppr โ€˜ ๐‘… ) ) ( ๐‘‹ ร— ๐‘Œ ) ) )
32 18 30 31 3eqtr4d โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ๐‘‹ ร— ( ๐‘ ยท ๐‘Œ ) ) = ( ๐‘ ยท ( ๐‘‹ ร— ๐‘Œ ) ) )