Metamath Proof Explorer


Theorem pwsmulg

Description: Value of a group multiple in a structure power. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses pwsmulg.y โŠข ๐‘Œ = ( ๐‘… โ†‘s ๐ผ )
pwsmulg.b โŠข ๐ต = ( Base โ€˜ ๐‘Œ )
pwsmulg.s โŠข โˆ™ = ( .g โ€˜ ๐‘Œ )
pwsmulg.t โŠข ยท = ( .g โ€˜ ๐‘… )
Assertion pwsmulg ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ( ( ๐‘ โˆ™ ๐‘‹ ) โ€˜ ๐ด ) = ( ๐‘ ยท ( ๐‘‹ โ€˜ ๐ด ) ) )

Proof

Step Hyp Ref Expression
1 pwsmulg.y โŠข ๐‘Œ = ( ๐‘… โ†‘s ๐ผ )
2 pwsmulg.b โŠข ๐ต = ( Base โ€˜ ๐‘Œ )
3 pwsmulg.s โŠข โˆ™ = ( .g โ€˜ ๐‘Œ )
4 pwsmulg.t โŠข ยท = ( .g โ€˜ ๐‘… )
5 simpll โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ๐‘… โˆˆ Mnd )
6 simplr โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ๐ผ โˆˆ ๐‘‰ )
7 simpr3 โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ๐ด โˆˆ ๐ผ )
8 1 2 pwspjmhm โŠข ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ โˆง ๐ด โˆˆ ๐ผ ) โ†’ ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โˆˆ ( ๐‘Œ MndHom ๐‘… ) )
9 5 6 7 8 syl3anc โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โˆˆ ( ๐‘Œ MndHom ๐‘… ) )
10 simpr1 โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ๐‘ โˆˆ โ„•0 )
11 simpr2 โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ๐‘‹ โˆˆ ๐ต )
12 2 3 4 mhmmulg โŠข ( ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โˆˆ ( ๐‘Œ MndHom ๐‘… ) โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โ€˜ ( ๐‘ โˆ™ ๐‘‹ ) ) = ( ๐‘ ยท ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โ€˜ ๐‘‹ ) ) )
13 9 10 11 12 syl3anc โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โ€˜ ( ๐‘ โˆ™ ๐‘‹ ) ) = ( ๐‘ ยท ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โ€˜ ๐‘‹ ) ) )
14 1 pwsmnd โŠข ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ๐‘Œ โˆˆ Mnd )
15 14 adantr โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ๐‘Œ โˆˆ Mnd )
16 2 3 mulgnn0cl โŠข ( ( ๐‘Œ โˆˆ Mnd โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ๐‘ โˆ™ ๐‘‹ ) โˆˆ ๐ต )
17 15 10 11 16 syl3anc โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ( ๐‘ โˆ™ ๐‘‹ ) โˆˆ ๐ต )
18 fveq1 โŠข ( ๐‘ฅ = ( ๐‘ โˆ™ ๐‘‹ ) โ†’ ( ๐‘ฅ โ€˜ ๐ด ) = ( ( ๐‘ โˆ™ ๐‘‹ ) โ€˜ ๐ด ) )
19 eqid โŠข ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) = ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) )
20 fvex โŠข ( ( ๐‘ โˆ™ ๐‘‹ ) โ€˜ ๐ด ) โˆˆ V
21 18 19 20 fvmpt โŠข ( ( ๐‘ โˆ™ ๐‘‹ ) โˆˆ ๐ต โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โ€˜ ( ๐‘ โˆ™ ๐‘‹ ) ) = ( ( ๐‘ โˆ™ ๐‘‹ ) โ€˜ ๐ด ) )
22 17 21 syl โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โ€˜ ( ๐‘ โˆ™ ๐‘‹ ) ) = ( ( ๐‘ โˆ™ ๐‘‹ ) โ€˜ ๐ด ) )
23 fveq1 โŠข ( ๐‘ฅ = ๐‘‹ โ†’ ( ๐‘ฅ โ€˜ ๐ด ) = ( ๐‘‹ โ€˜ ๐ด ) )
24 fvex โŠข ( ๐‘‹ โ€˜ ๐ด ) โˆˆ V
25 23 19 24 fvmpt โŠข ( ๐‘‹ โˆˆ ๐ต โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โ€˜ ๐‘‹ ) = ( ๐‘‹ โ€˜ ๐ด ) )
26 11 25 syl โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โ€˜ ๐‘‹ ) = ( ๐‘‹ โ€˜ ๐ด ) )
27 26 oveq2d โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ( ๐‘ ยท ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘ฅ โ€˜ ๐ด ) ) โ€˜ ๐‘‹ ) ) = ( ๐‘ ยท ( ๐‘‹ โ€˜ ๐ด ) ) )
28 13 22 27 3eqtr3d โŠข ( ( ( ๐‘… โˆˆ Mnd โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐ด โˆˆ ๐ผ ) ) โ†’ ( ( ๐‘ โˆ™ ๐‘‹ ) โ€˜ ๐ด ) = ( ๐‘ ยท ( ๐‘‹ โ€˜ ๐ด ) ) )