MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  asclpropd Unicode version

Theorem asclpropd 17592
Description: If two structures have the same components (properties), one is an associative algebra iff the other one is. The last hypotheses on can be discharged either by letting (if strong equality is known on ) or assuming is a ring. (Contributed by Mario Carneiro, 5-Jul-2015.)
Hypotheses
Ref Expression
asclpropd.f
asclpropd.g
asclpropd.1
asclpropd.2
asclpropd.3
asclpropd.4
asclpropd.5
Assertion
Ref Expression
asclpropd
Distinct variable groups:   , ,   , ,   ,P,   , ,   , ,

Proof of Theorem asclpropd
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 asclpropd.5 . . . . . . 7
21adantr 465 . . . . . 6
3 asclpropd.3 . . . . . . . 8
43proplem 14787 . . . . . . 7
54anassrs 648 . . . . . 6
62, 5mpdan 668 . . . . 5
7 asclpropd.4 . . . . . . 7
87oveq2d 6238 . . . . . 6
98adantr 465 . . . . 5
106, 9eqtrd 2495 . . . 4
1110mpteq2dva 4495 . . 3
12 asclpropd.1 . . . 4
1312mpteq1d 4490 . . 3
14 asclpropd.2 . . . 4
1514mpteq1d 4490 . . 3
1611, 13, 153eqtr3d 2503 . 2
17 eqid 2454 . . 3
18 asclpropd.f . . 3
19 eqid 2454 . . 3
20 eqid 2454 . . 3
21 eqid 2454 . . 3
2217, 18, 19, 20, 21asclfval 17581 . 2
23 eqid 2454 . . 3
24 asclpropd.g . . 3
25 eqid 2454 . . 3
26 eqid 2454 . . 3
27 eqid 2454 . . 3
2823, 24, 25, 26, 27asclfval 17581 . 2
2916, 22, 283eqtr4g 2520 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1370  e.wcel 1758  e.cmpt 4467  `cfv 5537  (class class class)co 6222   cbs 14332   csca 14400   cvsca 14401   cur 16778   cascl 17559
This theorem is referenced by:  ply1ascl  17893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4520  ax-sep 4530  ax-nul 4538  ax-pow 4587  ax-pr 4648
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2805  df-rex 2806  df-reu 2807  df-rab 2809  df-v 3083  df-sbc 3298  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-iun 4290  df-br 4410  df-opab 4468  df-mpt 4469  df-id 4753  df-xp 4963  df-rel 4964  df-cnv 4965  df-co 4966  df-dm 4967  df-rn 4968  df-res 4969  df-ima 4970  df-iota 5500  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-ov 6225  df-slot 14336  df-base 14337  df-ascl 17562
  Copyright terms: Public domain W3C validator