Metamath Proof Explorer


Theorem asclpropd

Description: If two structures have the same components (properties), one is an associative algebra iff the other one is. The last hypotheses on 1r can be discharged either by letting W = _V (if strong equality is known on .s ) or assuming K is a ring. (Contributed by Mario Carneiro, 5-Jul-2015)

Ref Expression
Hypotheses asclpropd.f โŠข ๐น = ( Scalar โ€˜ ๐พ )
asclpropd.g โŠข ๐บ = ( Scalar โ€˜ ๐ฟ )
asclpropd.1 โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( Base โ€˜ ๐น ) )
asclpropd.2 โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( Base โ€˜ ๐บ ) )
asclpropd.3 โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘Š ) ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ฆ ) = ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ฆ ) )
asclpropd.4 โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐พ ) = ( 1r โ€˜ ๐ฟ ) )
asclpropd.5 โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐พ ) โˆˆ ๐‘Š )
Assertion asclpropd ( ๐œ‘ โ†’ ( algSc โ€˜ ๐พ ) = ( algSc โ€˜ ๐ฟ ) )

Proof

Step Hyp Ref Expression
1 asclpropd.f โŠข ๐น = ( Scalar โ€˜ ๐พ )
2 asclpropd.g โŠข ๐บ = ( Scalar โ€˜ ๐ฟ )
3 asclpropd.1 โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( Base โ€˜ ๐น ) )
4 asclpropd.2 โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( Base โ€˜ ๐บ ) )
5 asclpropd.3 โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘ƒ โˆง ๐‘ฆ โˆˆ ๐‘Š ) ) โ†’ ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐พ ) ๐‘ฆ ) = ( ๐‘ฅ ( ยท๐‘  โ€˜ ๐ฟ ) ๐‘ฆ ) )
6 asclpropd.4 โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐พ ) = ( 1r โ€˜ ๐ฟ ) )
7 asclpropd.5 โŠข ( ๐œ‘ โ†’ ( 1r โ€˜ ๐พ ) โˆˆ ๐‘Š )
8 5 oveqrspc2v โŠข ( ( ๐œ‘ โˆง ( ๐‘ง โˆˆ ๐‘ƒ โˆง ( 1r โ€˜ ๐พ ) โˆˆ ๐‘Š ) ) โ†’ ( ๐‘ง ( ยท๐‘  โ€˜ ๐พ ) ( 1r โ€˜ ๐พ ) ) = ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐พ ) ) )
9 8 anassrs โŠข ( ( ( ๐œ‘ โˆง ๐‘ง โˆˆ ๐‘ƒ ) โˆง ( 1r โ€˜ ๐พ ) โˆˆ ๐‘Š ) โ†’ ( ๐‘ง ( ยท๐‘  โ€˜ ๐พ ) ( 1r โ€˜ ๐พ ) ) = ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐พ ) ) )
10 7 9 mpidan โŠข ( ( ๐œ‘ โˆง ๐‘ง โˆˆ ๐‘ƒ ) โ†’ ( ๐‘ง ( ยท๐‘  โ€˜ ๐พ ) ( 1r โ€˜ ๐พ ) ) = ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐พ ) ) )
11 6 oveq2d โŠข ( ๐œ‘ โ†’ ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐พ ) ) = ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐ฟ ) ) )
12 11 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ง โˆˆ ๐‘ƒ ) โ†’ ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐พ ) ) = ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐ฟ ) ) )
13 10 12 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘ง โˆˆ ๐‘ƒ ) โ†’ ( ๐‘ง ( ยท๐‘  โ€˜ ๐พ ) ( 1r โ€˜ ๐พ ) ) = ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐ฟ ) ) )
14 13 mpteq2dva โŠข ( ๐œ‘ โ†’ ( ๐‘ง โˆˆ ๐‘ƒ โ†ฆ ( ๐‘ง ( ยท๐‘  โ€˜ ๐พ ) ( 1r โ€˜ ๐พ ) ) ) = ( ๐‘ง โˆˆ ๐‘ƒ โ†ฆ ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐ฟ ) ) ) )
15 3 mpteq1d โŠข ( ๐œ‘ โ†’ ( ๐‘ง โˆˆ ๐‘ƒ โ†ฆ ( ๐‘ง ( ยท๐‘  โ€˜ ๐พ ) ( 1r โ€˜ ๐พ ) ) ) = ( ๐‘ง โˆˆ ( Base โ€˜ ๐น ) โ†ฆ ( ๐‘ง ( ยท๐‘  โ€˜ ๐พ ) ( 1r โ€˜ ๐พ ) ) ) )
16 4 mpteq1d โŠข ( ๐œ‘ โ†’ ( ๐‘ง โˆˆ ๐‘ƒ โ†ฆ ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐ฟ ) ) ) = ( ๐‘ง โˆˆ ( Base โ€˜ ๐บ ) โ†ฆ ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐ฟ ) ) ) )
17 14 15 16 3eqtr3d โŠข ( ๐œ‘ โ†’ ( ๐‘ง โˆˆ ( Base โ€˜ ๐น ) โ†ฆ ( ๐‘ง ( ยท๐‘  โ€˜ ๐พ ) ( 1r โ€˜ ๐พ ) ) ) = ( ๐‘ง โˆˆ ( Base โ€˜ ๐บ ) โ†ฆ ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐ฟ ) ) ) )
18 eqid โŠข ( algSc โ€˜ ๐พ ) = ( algSc โ€˜ ๐พ )
19 eqid โŠข ( Base โ€˜ ๐น ) = ( Base โ€˜ ๐น )
20 eqid โŠข ( ยท๐‘  โ€˜ ๐พ ) = ( ยท๐‘  โ€˜ ๐พ )
21 eqid โŠข ( 1r โ€˜ ๐พ ) = ( 1r โ€˜ ๐พ )
22 18 1 19 20 21 asclfval โŠข ( algSc โ€˜ ๐พ ) = ( ๐‘ง โˆˆ ( Base โ€˜ ๐น ) โ†ฆ ( ๐‘ง ( ยท๐‘  โ€˜ ๐พ ) ( 1r โ€˜ ๐พ ) ) )
23 eqid โŠข ( algSc โ€˜ ๐ฟ ) = ( algSc โ€˜ ๐ฟ )
24 eqid โŠข ( Base โ€˜ ๐บ ) = ( Base โ€˜ ๐บ )
25 eqid โŠข ( ยท๐‘  โ€˜ ๐ฟ ) = ( ยท๐‘  โ€˜ ๐ฟ )
26 eqid โŠข ( 1r โ€˜ ๐ฟ ) = ( 1r โ€˜ ๐ฟ )
27 23 2 24 25 26 asclfval โŠข ( algSc โ€˜ ๐ฟ ) = ( ๐‘ง โˆˆ ( Base โ€˜ ๐บ ) โ†ฆ ( ๐‘ง ( ยท๐‘  โ€˜ ๐ฟ ) ( 1r โ€˜ ๐ฟ ) ) )
28 17 22 27 3eqtr4g โŠข ( ๐œ‘ โ†’ ( algSc โ€˜ ๐พ ) = ( algSc โ€˜ ๐ฟ ) )