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