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 
|- F = ( Scalar ` K )
asclpropd.g 
|- G = ( Scalar ` L )
asclpropd.1 
|- ( ph -> P = ( Base ` F ) )
asclpropd.2 
|- ( ph -> P = ( Base ` G ) )
asclpropd.3 
|- ( ( ph /\ ( x e. P /\ y e. W ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
asclpropd.4 
|- ( ph -> ( 1r ` K ) = ( 1r ` L ) )
asclpropd.5 
|- ( ph -> ( 1r ` K ) e. W )
Assertion asclpropd 
|- ( ph -> ( algSc ` K ) = ( algSc ` L ) )

Proof

Step Hyp Ref Expression
1 asclpropd.f 
 |-  F = ( Scalar ` K )
2 asclpropd.g 
 |-  G = ( Scalar ` L )
3 asclpropd.1 
 |-  ( ph -> P = ( Base ` F ) )
4 asclpropd.2 
 |-  ( ph -> P = ( Base ` G ) )
5 asclpropd.3 
 |-  ( ( ph /\ ( x e. P /\ y e. W ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
6 asclpropd.4 
 |-  ( ph -> ( 1r ` K ) = ( 1r ` L ) )
7 asclpropd.5 
 |-  ( ph -> ( 1r ` K ) e. W )
8 5 oveqrspc2v 
 |-  ( ( ph /\ ( z e. P /\ ( 1r ` K ) e. W ) ) -> ( z ( .s ` K ) ( 1r ` K ) ) = ( z ( .s ` L ) ( 1r ` K ) ) )
9 8 anassrs 
 |-  ( ( ( ph /\ z e. P ) /\ ( 1r ` K ) e. W ) -> ( z ( .s ` K ) ( 1r ` K ) ) = ( z ( .s ` L ) ( 1r ` K ) ) )
10 7 9 mpidan 
 |-  ( ( ph /\ z e. P ) -> ( z ( .s ` K ) ( 1r ` K ) ) = ( z ( .s ` L ) ( 1r ` K ) ) )
11 6 oveq2d 
 |-  ( ph -> ( z ( .s ` L ) ( 1r ` K ) ) = ( z ( .s ` L ) ( 1r ` L ) ) )
12 11 adantr 
 |-  ( ( ph /\ z e. P ) -> ( z ( .s ` L ) ( 1r ` K ) ) = ( z ( .s ` L ) ( 1r ` L ) ) )
13 10 12 eqtrd 
 |-  ( ( ph /\ z e. P ) -> ( z ( .s ` K ) ( 1r ` K ) ) = ( z ( .s ` L ) ( 1r ` L ) ) )
14 13 mpteq2dva 
 |-  ( ph -> ( z e. P |-> ( z ( .s ` K ) ( 1r ` K ) ) ) = ( z e. P |-> ( z ( .s ` L ) ( 1r ` L ) ) ) )
15 3 mpteq1d 
 |-  ( ph -> ( z e. P |-> ( z ( .s ` K ) ( 1r ` K ) ) ) = ( z e. ( Base ` F ) |-> ( z ( .s ` K ) ( 1r ` K ) ) ) )
16 4 mpteq1d 
 |-  ( ph -> ( z e. P |-> ( z ( .s ` L ) ( 1r ` L ) ) ) = ( z e. ( Base ` G ) |-> ( z ( .s ` L ) ( 1r ` L ) ) ) )
17 14 15 16 3eqtr3d 
 |-  ( ph -> ( z e. ( Base ` F ) |-> ( z ( .s ` K ) ( 1r ` K ) ) ) = ( z e. ( Base ` G ) |-> ( z ( .s ` L ) ( 1r ` L ) ) ) )
18 eqid 
 |-  ( algSc ` K ) = ( algSc ` K )
19 eqid 
 |-  ( Base ` F ) = ( Base ` F )
20 eqid 
 |-  ( .s ` K ) = ( .s ` K )
21 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
22 18 1 19 20 21 asclfval 
 |-  ( algSc ` K ) = ( z e. ( Base ` F ) |-> ( z ( .s ` K ) ( 1r ` K ) ) )
23 eqid 
 |-  ( algSc ` L ) = ( algSc ` L )
24 eqid 
 |-  ( Base ` G ) = ( Base ` G )
25 eqid 
 |-  ( .s ` L ) = ( .s ` L )
26 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
27 23 2 24 25 26 asclfval 
 |-  ( algSc ` L ) = ( z e. ( Base ` G ) |-> ( z ( .s ` L ) ( 1r ` L ) ) )
28 17 22 27 3eqtr4g 
 |-  ( ph -> ( algSc ` K ) = ( algSc ` L ) )