Metamath Proof Explorer


Theorem assapropd

Description: If two structures have the same components (properties), one is an associative algebra iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses assapropd.1 φ B = Base K
assapropd.2 φ B = Base L
assapropd.3 φ x B y B x + K y = x + L y
assapropd.4 φ x B y B x K y = x L y
assapropd.5 φ F = Scalar K
assapropd.6 φ F = Scalar L
assapropd.7 P = Base F
assapropd.8 φ x P y B x K y = x L y
Assertion assapropd φ K AssAlg L AssAlg

Proof

Step Hyp Ref Expression
1 assapropd.1 φ B = Base K
2 assapropd.2 φ B = Base L
3 assapropd.3 φ x B y B x + K y = x + L y
4 assapropd.4 φ x B y B x K y = x L y
5 assapropd.5 φ F = Scalar K
6 assapropd.6 φ F = Scalar L
7 assapropd.7 P = Base F
8 assapropd.8 φ x P y B x K y = x L y
9 assalmod K AssAlg K LMod
10 assaring K AssAlg K Ring
11 9 10 jca K AssAlg K LMod K Ring
12 11 a1i φ K AssAlg K LMod K Ring
13 assalmod L AssAlg L LMod
14 1 2 3 5 6 7 8 lmodpropd φ K LMod L LMod
15 13 14 imbitrrid φ L AssAlg K LMod
16 assaring L AssAlg L Ring
17 1 2 3 4 ringpropd φ K Ring L Ring
18 16 17 imbitrrid φ L AssAlg K Ring
19 15 18 jcad φ L AssAlg K LMod K Ring
20 14 17 anbi12d φ K LMod K Ring L LMod L Ring
21 20 adantr φ K LMod K Ring K LMod K Ring L LMod L Ring
22 simpll φ K LMod K Ring r P z B w B φ
23 simplrl φ K LMod K Ring r P z B w B K LMod
24 simprl φ K LMod K Ring r P z B w B r P
25 5 fveq2d φ Base F = Base Scalar K
26 7 25 eqtrid φ P = Base Scalar K
27 22 26 syl φ K LMod K Ring r P z B w B P = Base Scalar K
28 24 27 eleqtrd φ K LMod K Ring r P z B w B r Base Scalar K
29 simprrl φ K LMod K Ring r P z B w B z B
30 22 1 syl φ K LMod K Ring r P z B w B B = Base K
31 29 30 eleqtrd φ K LMod K Ring r P z B w B z Base K
32 eqid Base K = Base K
33 eqid Scalar K = Scalar K
34 eqid K = K
35 eqid Base Scalar K = Base Scalar K
36 32 33 34 35 lmodvscl K LMod r Base Scalar K z Base K r K z Base K
37 23 28 31 36 syl3anc φ K LMod K Ring r P z B w B r K z Base K
38 37 30 eleqtrrd φ K LMod K Ring r P z B w B r K z B
39 simprrr φ K LMod K Ring r P z B w B w B
40 4 oveqrspc2v φ r K z B w B r K z K w = r K z L w
41 22 38 39 40 syl12anc φ K LMod K Ring r P z B w B r K z K w = r K z L w
42 8 oveqrspc2v φ r P z B r K z = r L z
43 22 24 29 42 syl12anc φ K LMod K Ring r P z B w B r K z = r L z
44 43 oveq1d φ K LMod K Ring r P z B w B r K z L w = r L z L w
45 41 44 eqtrd φ K LMod K Ring r P z B w B r K z K w = r L z L w
46 eqid K = K
47 simplrr φ K LMod K Ring r P z B w B K Ring
48 39 30 eleqtrd φ K LMod K Ring r P z B w B w Base K
49 32 46 47 31 48 ringcld φ K LMod K Ring r P z B w B z K w Base K
50 49 30 eleqtrrd φ K LMod K Ring r P z B w B z K w B
51 8 oveqrspc2v φ r P z K w B r K z K w = r L z K w
52 22 24 50 51 syl12anc φ K LMod K Ring r P z B w B r K z K w = r L z K w
53 4 oveqrspc2v φ z B w B z K w = z L w
54 22 29 39 53 syl12anc φ K LMod K Ring r P z B w B z K w = z L w
55 54 oveq2d φ K LMod K Ring r P z B w B r L z K w = r L z L w
56 52 55 eqtrd φ K LMod K Ring r P z B w B r K z K w = r L z L w
57 45 56 eqeq12d φ K LMod K Ring r P z B w B r K z K w = r K z K w r L z L w = r L z L w
58 32 33 34 35 lmodvscl K LMod r Base Scalar K w Base K r K w Base K
59 23 28 48 58 syl3anc φ K LMod K Ring r P z B w B r K w Base K
60 59 30 eleqtrrd φ K LMod K Ring r P z B w B r K w B
61 4 oveqrspc2v φ z B r K w B z K r K w = z L r K w
62 22 29 60 61 syl12anc φ K LMod K Ring r P z B w B z K r K w = z L r K w
63 8 oveqrspc2v φ r P w B r K w = r L w
64 22 24 39 63 syl12anc φ K LMod K Ring r P z B w B r K w = r L w
65 64 oveq2d φ K LMod K Ring r P z B w B z L r K w = z L r L w
66 62 65 eqtrd φ K LMod K Ring r P z B w B z K r K w = z L r L w
67 66 56 eqeq12d φ K LMod K Ring r P z B w B z K r K w = r K z K w z L r L w = r L z L w
68 57 67 anbi12d φ K LMod K Ring r P z B w B r K z K w = r K z K w z K r K w = r K z K w r L z L w = r L z L w z L r L w = r L z L w
69 68 anassrs φ K LMod K Ring r P z B w B r K z K w = r K z K w z K r K w = r K z K w r L z L w = r L z L w z L r L w = r L z L w
70 69 2ralbidva φ K LMod K Ring r P z B w B r K z K w = r K z K w z K r K w = r K z K w z B w B r L z L w = r L z L w z L r L w = r L z L w
71 70 ralbidva φ K LMod K Ring r P z B w B r K z K w = r K z K w z K r K w = r K z K w r P z B w B r L z L w = r L z L w z L r L w = r L z L w
72 26 adantr φ K LMod K Ring P = Base Scalar K
73 1 adantr φ K LMod K Ring B = Base K
74 73 raleqdv φ K LMod K Ring w B r K z K w = r K z K w z K r K w = r K z K w w Base K r K z K w = r K z K w z K r K w = r K z K w
75 73 74 raleqbidv φ K LMod K Ring z B w B r K z K w = r K z K w z K r K w = r K z K w z Base K w Base K r K z K w = r K z K w z K r K w = r K z K w
76 72 75 raleqbidv φ K LMod K Ring r P z B w B r K z K w = r K z K w z K r K w = r K z K w r Base Scalar K z Base K w Base K r K z K w = r K z K w z K r K w = r K z K w
77 6 fveq2d φ Base F = Base Scalar L
78 7 77 eqtrid φ P = Base Scalar L
79 78 adantr φ K LMod K Ring P = Base Scalar L
80 2 adantr φ K LMod K Ring B = Base L
81 80 raleqdv φ K LMod K Ring w B r L z L w = r L z L w z L r L w = r L z L w w Base L r L z L w = r L z L w z L r L w = r L z L w
82 80 81 raleqbidv φ K LMod K Ring z B w B r L z L w = r L z L w z L r L w = r L z L w z Base L w Base L r L z L w = r L z L w z L r L w = r L z L w
83 79 82 raleqbidv φ K LMod K Ring r P z B w B r L z L w = r L z L w z L r L w = r L z L w r Base Scalar L z Base L w Base L r L z L w = r L z L w z L r L w = r L z L w
84 71 76 83 3bitr3d φ K LMod K Ring r Base Scalar K z Base K w Base K r K z K w = r K z K w z K r K w = r K z K w r Base Scalar L z Base L w Base L r L z L w = r L z L w z L r L w = r L z L w
85 21 84 anbi12d φ K LMod K Ring K LMod K Ring r Base Scalar K z Base K w Base K r K z K w = r K z K w z K r K w = r K z K w L LMod L Ring r Base Scalar L z Base L w Base L r L z L w = r L z L w z L r L w = r L z L w
86 32 33 35 34 46 isassa K AssAlg K LMod K Ring r Base Scalar K z Base K w Base K r K z K w = r K z K w z K r K w = r K z K w
87 eqid Base L = Base L
88 eqid Scalar L = Scalar L
89 eqid Base Scalar L = Base Scalar L
90 eqid L = L
91 eqid L = L
92 87 88 89 90 91 isassa L AssAlg L LMod L Ring r Base Scalar L z Base L w Base L r L z L w = r L z L w z L r L w = r L z L w
93 85 86 92 3bitr4g φ K LMod K Ring K AssAlg L AssAlg
94 93 ex φ K LMod K Ring K AssAlg L AssAlg
95 12 19 94 pm5.21ndd φ K AssAlg L AssAlg