lsmpropd

Description: If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 29-Jun-2015) (Revised by AV, 25-Apr-2024)

	Ref	Expression
Hypotheses	lsmpropd.b1	$⊢ φ \to B = {Base}_{K}$
	lsmpropd.b2	$⊢ φ \to B = {Base}_{L}$
	lsmpropd.p	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
	lsmpropd.v1	$⊢ φ \to K \in V$
	lsmpropd.v2	$⊢ φ \to L \in W$
Assertion	lsmpropd	$⊢ φ \to LSSum (K) = LSSum (L)$

Proof

Step	Hyp	Ref	Expression
1		lsmpropd.b1	$⊢ φ \to B = {Base}_{K}$
2		lsmpropd.b2	$⊢ φ \to B = {Base}_{L}$
3		lsmpropd.p	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		lsmpropd.v1	$⊢ φ \to K \in V$
5		lsmpropd.v2	$⊢ φ \to L \in W$
6		simp11	$⊢ ((φ \land t \in 𝒫 B \land u \in 𝒫 B) \land x \in t \land y \in u) \to φ$
7		simp12	$⊢ ((φ \land t \in 𝒫 B \land u \in 𝒫 B) \land x \in t \land y \in u) \to t \in 𝒫 B$
8	7	elpwid	$⊢ ((φ \land t \in 𝒫 B \land u \in 𝒫 B) \land x \in t \land y \in u) \to t \subseteq B$
9		simp2	$⊢ ((φ \land t \in 𝒫 B \land u \in 𝒫 B) \land x \in t \land y \in u) \to x \in t$
10	8 9	sseldd	$⊢ ((φ \land t \in 𝒫 B \land u \in 𝒫 B) \land x \in t \land y \in u) \to x \in B$
11		simp13	$⊢ ((φ \land t \in 𝒫 B \land u \in 𝒫 B) \land x \in t \land y \in u) \to u \in 𝒫 B$
12	11	elpwid	$⊢ ((φ \land t \in 𝒫 B \land u \in 𝒫 B) \land x \in t \land y \in u) \to u \subseteq B$
13		simp3	$⊢ ((φ \land t \in 𝒫 B \land u \in 𝒫 B) \land x \in t \land y \in u) \to y \in u$
14	12 13	sseldd	$⊢ ((φ \land t \in 𝒫 B \land u \in 𝒫 B) \land x \in t \land y \in u) \to y \in B$
15	6 10 14 3	syl12anc	$⊢ ((φ \land t \in 𝒫 B \land u \in 𝒫 B) \land x \in t \land y \in u) \to x +_{K} y = x +_{L} y$
16	15	mpoeq3dva	$⊢ (φ \land t \in 𝒫 B \land u \in 𝒫 B) \to (x \in t, y \in u ⟼ x +_{K} y) = (x \in t, y \in u ⟼ x +_{L} y)$
17	16	rneqd	$⊢ (φ \land t \in 𝒫 B \land u \in 𝒫 B) \to ran (x \in t, y \in u ⟼ x +_{K} y) = ran (x \in t, y \in u ⟼ x +_{L} y)$
18	17	mpoeq3dva	$⊢ φ \to (t \in 𝒫 B, u \in 𝒫 B ⟼ ran (x \in t, y \in u ⟼ x +_{K} y)) = (t \in 𝒫 B, u \in 𝒫 B ⟼ ran (x \in t, y \in u ⟼ x +_{L} y))$
19	1	pweqd	$⊢ φ \to 𝒫 B = 𝒫 {Base}_{K}$
20		mpoeq12	$⊢ (𝒫 B = 𝒫 {Base}_{K} \land 𝒫 B = 𝒫 {Base}_{K}) \to (t \in 𝒫 B, u \in 𝒫 B ⟼ ran (x \in t, y \in u ⟼ x +_{K} y)) = (t \in 𝒫 {Base}_{K}, u \in 𝒫 {Base}_{K} ⟼ ran (x \in t, y \in u ⟼ x +_{K} y))$
21	19 19 20	syl2anc	$⊢ φ \to (t \in 𝒫 B, u \in 𝒫 B ⟼ ran (x \in t, y \in u ⟼ x +_{K} y)) = (t \in 𝒫 {Base}_{K}, u \in 𝒫 {Base}_{K} ⟼ ran (x \in t, y \in u ⟼ x +_{K} y))$
22	2	pweqd	$⊢ φ \to 𝒫 B = 𝒫 {Base}_{L}$
23		mpoeq12	$⊢ (𝒫 B = 𝒫 {Base}_{L} \land 𝒫 B = 𝒫 {Base}_{L}) \to (t \in 𝒫 B, u \in 𝒫 B ⟼ ran (x \in t, y \in u ⟼ x +_{L} y)) = (t \in 𝒫 {Base}_{L}, u \in 𝒫 {Base}_{L} ⟼ ran (x \in t, y \in u ⟼ x +_{L} y))$
24	22 22 23	syl2anc	$⊢ φ \to (t \in 𝒫 B, u \in 𝒫 B ⟼ ran (x \in t, y \in u ⟼ x +_{L} y)) = (t \in 𝒫 {Base}_{L}, u \in 𝒫 {Base}_{L} ⟼ ran (x \in t, y \in u ⟼ x +_{L} y))$
25	18 21 24	3eqtr3d	$⊢ φ \to (t \in 𝒫 {Base}_{K}, u \in 𝒫 {Base}_{K} ⟼ ran (x \in t, y \in u ⟼ x +_{K} y)) = (t \in 𝒫 {Base}_{L}, u \in 𝒫 {Base}_{L} ⟼ ran (x \in t, y \in u ⟼ x +_{L} y))$
26		eqid	$⊢ {Base}_{K} = {Base}_{K}$
27		eqid	$⊢ +_{K} = +_{K}$
28		eqid	$⊢ LSSum (K) = LSSum (K)$
29	26 27 28	lsmfval	$⊢ K \in V \to LSSum (K) = (t \in 𝒫 {Base}_{K}, u \in 𝒫 {Base}_{K} ⟼ ran (x \in t, y \in u ⟼ x +_{K} y))$
30	4 29	syl	$⊢ φ \to LSSum (K) = (t \in 𝒫 {Base}_{K}, u \in 𝒫 {Base}_{K} ⟼ ran (x \in t, y \in u ⟼ x +_{K} y))$
31		eqid	$⊢ {Base}_{L} = {Base}_{L}$
32		eqid	$⊢ +_{L} = +_{L}$
33		eqid	$⊢ LSSum (L) = LSSum (L)$
34	31 32 33	lsmfval	$⊢ L \in W \to LSSum (L) = (t \in 𝒫 {Base}_{L}, u \in 𝒫 {Base}_{L} ⟼ ran (x \in t, y \in u ⟼ x +_{L} y))$
35	5 34	syl	$⊢ φ \to LSSum (L) = (t \in 𝒫 {Base}_{L}, u \in 𝒫 {Base}_{L} ⟼ ran (x \in t, y \in u ⟼ x +_{L} y))$
36	25 30 35	3eqtr4d	$⊢ φ \to LSSum (K) = LSSum (L)$

Metamath Proof Explorer

Theorem lsmpropd

Proof