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	$⊢ φ \to B = {Base}_{K}$
	assapropd.2	$⊢ φ \to B = {Base}_{L}$
	assapropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
	assapropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
	assapropd.5	$⊢ φ \to F = Scalar (K)$
	assapropd.6	$⊢ φ \to F = Scalar (L)$
	assapropd.7	$⊢ P = {Base}_{F}$
	assapropd.8	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
Assertion	assapropd	$⊢ φ \to (K \in AssAlg \leftrightarrow L \in AssAlg)$

Proof

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

Metamath Proof Explorer

Theorem assapropd

Proof