Metamath Proof Explorer


Theorem mulgaddcomlem

Description: Lemma for mulgaddcom . (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 31-Aug-2021)

Ref Expression
Hypotheses mulgaddcom.b โŠข ๐ต = ( Base โ€˜ ๐บ )
mulgaddcom.t โŠข ยท = ( .g โ€˜ ๐บ )
mulgaddcom.p โŠข + = ( +g โ€˜ ๐บ )
Assertion mulgaddcomlem ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( - ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) )

Proof

Step Hyp Ref Expression
1 mulgaddcom.b โŠข ๐ต = ( Base โ€˜ ๐บ )
2 mulgaddcom.t โŠข ยท = ( .g โ€˜ ๐บ )
3 mulgaddcom.p โŠข + = ( +g โ€˜ ๐บ )
4 simp1 โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ๐บ โˆˆ Grp )
5 4 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ๐บ โˆˆ Grp )
6 simp3 โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ๐‘‹ โˆˆ ๐ต )
7 6 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ๐‘‹ โˆˆ ๐ต )
8 znegcl โŠข ( ๐‘ฆ โˆˆ โ„ค โ†’ - ๐‘ฆ โˆˆ โ„ค )
9 1 2 mulgcl โŠข ( ( ๐บ โˆˆ Grp โˆง - ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( - ๐‘ฆ ยท ๐‘‹ ) โˆˆ ๐ต )
10 8 9 syl3an2 โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( - ๐‘ฆ ยท ๐‘‹ ) โˆˆ ๐ต )
11 10 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( - ๐‘ฆ ยท ๐‘‹ ) โˆˆ ๐ต )
12 eqid โŠข ( invg โ€˜ ๐บ ) = ( invg โ€˜ ๐บ )
13 1 12 grpinvcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) โˆˆ ๐ต )
14 13 3adant2 โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) โˆˆ ๐ต )
15 14 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) โˆˆ ๐ต )
16 1 3 grpass โŠข ( ( ๐บ โˆˆ Grp โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ( - ๐‘ฆ ยท ๐‘‹ ) โˆˆ ๐ต โˆง ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) โˆˆ ๐ต ) ) โ†’ ( ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) = ( ๐‘‹ + ( ( - ๐‘ฆ ยท ๐‘‹ ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) ) )
17 5 7 11 15 16 syl13anc โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) = ( ๐‘‹ + ( ( - ๐‘ฆ ยท ๐‘‹ ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) ) )
18 1 2 12 mulgneg โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( - ๐‘ฆ ยท ๐‘‹ ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘ฆ ยท ๐‘‹ ) ) )
19 18 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( - ๐‘ฆ ยท ๐‘‹ ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘ฆ ยท ๐‘‹ ) ) )
20 19 oveq1d โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( - ๐‘ฆ ยท ๐‘‹ ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘ฆ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) )
21 1 2 mulgcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ๐‘ฆ ยท ๐‘‹ ) โˆˆ ๐ต )
22 21 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ๐‘ฆ ยท ๐‘‹ ) โˆˆ ๐ต )
23 1 3 12 grpinvadd โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ( ๐‘ฆ ยท ๐‘‹ ) โˆˆ ๐ต ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘ฆ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) )
24 5 7 22 23 syl3anc โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘ฆ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) )
25 19 oveq2d โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) + ( - ๐‘ฆ ยท ๐‘‹ ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) + ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘ฆ ยท ๐‘‹ ) ) ) )
26 1 3 12 grpinvadd โŠข ( ( ๐บ โˆˆ Grp โˆง ( ๐‘ฆ ยท ๐‘‹ ) โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) + ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘ฆ ยท ๐‘‹ ) ) ) )
27 5 22 7 26 syl3anc โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) + ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘ฆ ยท ๐‘‹ ) ) ) )
28 fveq2 โŠข ( ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) )
29 28 adantl โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) ) = ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) )
30 25 27 29 3eqtr2rd โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( invg โ€˜ ๐บ ) โ€˜ ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) + ( - ๐‘ฆ ยท ๐‘‹ ) ) )
31 20 24 30 3eqtr2d โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( - ๐‘ฆ ยท ๐‘‹ ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) = ( ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) + ( - ๐‘ฆ ยท ๐‘‹ ) ) )
32 31 oveq2d โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ๐‘‹ + ( ( - ๐‘ฆ ยท ๐‘‹ ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) ) = ( ๐‘‹ + ( ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) + ( - ๐‘ฆ ยท ๐‘‹ ) ) ) )
33 1 3 12 grpasscan1 โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ( - ๐‘ฆ ยท ๐‘‹ ) โˆˆ ๐ต ) โ†’ ( ๐‘‹ + ( ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) + ( - ๐‘ฆ ยท ๐‘‹ ) ) ) = ( - ๐‘ฆ ยท ๐‘‹ ) )
34 5 7 11 33 syl3anc โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ๐‘‹ + ( ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) + ( - ๐‘ฆ ยท ๐‘‹ ) ) ) = ( - ๐‘ฆ ยท ๐‘‹ ) )
35 17 32 34 3eqtrd โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) = ( - ๐‘ฆ ยท ๐‘‹ ) )
36 35 oveq1d โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) + ๐‘‹ ) = ( ( - ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) )
37 1 3 grpcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ( - ๐‘ฆ ยท ๐‘‹ ) โˆˆ ๐ต ) โ†’ ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) โˆˆ ๐ต )
38 4 6 10 37 syl3anc โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) โˆˆ ๐ต )
39 38 adantr โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) โˆˆ ๐ต )
40 1 3 12 grpasscan2 โŠข ( ( ๐บ โˆˆ Grp โˆง ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ( ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) + ๐‘‹ ) = ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) )
41 5 39 7 40 syl3anc โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) + ( ( invg โ€˜ ๐บ ) โ€˜ ๐‘‹ ) ) + ๐‘‹ ) = ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) )
42 36 41 eqtr3d โŠข ( ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต ) โˆง ( ( ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( ๐‘ฆ ยท ๐‘‹ ) ) ) โ†’ ( ( - ๐‘ฆ ยท ๐‘‹ ) + ๐‘‹ ) = ( ๐‘‹ + ( - ๐‘ฆ ยท ๐‘‹ ) ) )