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	imbitrrid	$⊢ φ \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	imbitrrid	$⊢ φ \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	14 17	anbi12d	$⊢ φ \to ((K \in LMod \land K \in Ring) \leftrightarrow (L \in LMod \land L \in Ring))$
21	20	adantr	$⊢ (φ \land (K \in LMod \land K \in Ring)) \to ((K \in LMod \land K \in Ring) \leftrightarrow (L \in LMod \land L \in Ring))$
22		simpll	$⊢ ((φ \land (K \in LMod \land K \in Ring)) \land (r \in P \land (z \in B \land w \in B))) \to φ$
23		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$
24		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$
25	5	fveq2d	$⊢ φ \to {Base}_{F} = {Base}_{Scalar (K)}$
26	7 25	eqtrid	$⊢ φ \to P = {Base}_{Scalar (K)}$
27	22 26	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)}$
28	24 27	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)}$
29		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$
30	22 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}$
31	29 30	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}$
32		eqid	$⊢ {Base}_{K} = {Base}_{K}$
33		eqid	$⊢ Scalar (K) = Scalar (K)$
34		eqid	$⊢ \cdot_{K} = \cdot_{K}$
35		eqid	$⊢ {Base}_{Scalar (K)} = {Base}_{Scalar (K)}$
36	32 33 34 35	lmodvscl	$⊢ (K \in LMod \land r \in {Base}_{Scalar (K)} \land z \in {Base}_{K}) \to r \cdot_{K} z \in {Base}_{K}$
37	23 28 31 36	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}$
38	37 30	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$
39		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$
40	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$
41	22 38 39 40	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$
42	8	oveqrspc2v	$⊢ (φ \land (r \in P \land z \in B)) \to r \cdot_{K} z = r \cdot_{L} z$
43	22 24 29 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 = r \cdot_{L} z$
44	43	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$
45	41 44	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$
46		eqid	$⊢ \cdot_{K} = \cdot_{K}$
47		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$
48	39 30	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}$
49	32 46 47 31 48	ringcld	$⊢ ((φ \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}$
50	49 30	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$
51	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)$
52	22 24 50 51	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)$
53	4	oveqrspc2v	$⊢ (φ \land (z \in B \land w \in B)) \to z \cdot_{K} w = z \cdot_{L} w$
54	22 29 39 53	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$
55	54	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)$
56	52 55	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)$
57	45 56	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))$
58	32 33 34 35	lmodvscl	$⊢ (K \in LMod \land r \in {Base}_{Scalar (K)} \land w \in {Base}_{K}) \to r \cdot_{K} w \in {Base}_{K}$
59	23 28 48 58	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}$
60	59 30	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$
61	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)$
62	22 29 60 61	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)$
63	8	oveqrspc2v	$⊢ (φ \land (r \in P \land w \in B)) \to r \cdot_{K} w = r \cdot_{L} w$
64	22 24 39 63	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$
65	64	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)$
66	62 65	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)$
67	66 56	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))$
68	57 67	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)))$
69	68	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)))$
70	69	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)))$
71	70	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)))$
72	26	adantr	$⊢ (φ \land (K \in LMod \land K \in Ring)) \to P = {Base}_{Scalar (K)}$
73	1	adantr	$⊢ (φ \land (K \in LMod \land K \in Ring)) \to B = {Base}_{K}$
74	73	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)))$
75	73 74	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)))$
76	72 75	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)))$
77	6	fveq2d	$⊢ φ \to {Base}_{F} = {Base}_{Scalar (L)}$
78	7 77	eqtrid	$⊢ φ \to P = {Base}_{Scalar (L)}$
79	78	adantr	$⊢ (φ \land (K \in LMod \land K \in Ring)) \to P = {Base}_{Scalar (L)}$
80	2	adantr	$⊢ (φ \land (K \in LMod \land K \in Ring)) \to B = {Base}_{L}$
81	80	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)))$
82	80 81	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)))$
83	79 82	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)))$
84	71 76 83	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)))$
85	21 84	anbi12d	$⊢ (φ \land (K \in LMod \land K \in Ring)) \to (((K \in LMod \land K \in Ring) \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 \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))))$
86	32 33 35 34 46	isassa	$⊢ K \in AssAlg \leftrightarrow ((K \in LMod \land K \in Ring) \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)))$
87		eqid	$⊢ {Base}_{L} = {Base}_{L}$
88		eqid	$⊢ Scalar (L) = Scalar (L)$
89		eqid	$⊢ {Base}_{Scalar (L)} = {Base}_{Scalar (L)}$
90		eqid	$⊢ \cdot_{L} = \cdot_{L}$
91		eqid	$⊢ \cdot_{L} = \cdot_{L}$
92	87 88 89 90 91	isassa	$⊢ L \in AssAlg \leftrightarrow ((L \in LMod \land L \in Ring) \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)))$
93	85 86 92	3bitr4g	$⊢ (φ \land (K \in LMod \land K \in Ring)) \to (K \in AssAlg \leftrightarrow L \in AssAlg)$
94	93	ex	$⊢ φ \to ((K \in LMod \land K \in Ring) \to (K \in AssAlg \leftrightarrow L \in AssAlg))$
95	12 19 94	pm5.21ndd	$⊢ φ \to (K \in AssAlg \leftrightarrow L \in AssAlg)$

Metamath Proof Explorer

Theorem assapropd

Proof