lsspropd

Description: If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	lsspropd.b1	$⊢ φ \to B = {Base}_{K}$
	lsspropd.b2	$⊢ φ \to B = {Base}_{L}$
	lsspropd.w	$⊢ φ \to B \subseteq W$
	lsspropd.p	$⊢ (φ \land (x \in W \land y \in W)) \to x +_{K} y = x +_{L} y$
	lsspropd.s1	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y \in W$
	lsspropd.s2	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
	lsspropd.p1	$⊢ φ \to P = {Base}_{Scalar (K)}$
	lsspropd.p2	$⊢ φ \to P = {Base}_{Scalar (L)}$
Assertion	lsspropd	$⊢ φ \to LSubSp (K) = LSubSp (L)$

Proof

Step	Hyp	Ref	Expression
1		lsspropd.b1	$⊢ φ \to B = {Base}_{K}$
2		lsspropd.b2	$⊢ φ \to B = {Base}_{L}$
3		lsspropd.w	$⊢ φ \to B \subseteq W$
4		lsspropd.p	$⊢ (φ \land (x \in W \land y \in W)) \to x +_{K} y = x +_{L} y$
5		lsspropd.s1	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y \in W$
6		lsspropd.s2	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
7		lsspropd.p1	$⊢ φ \to P = {Base}_{Scalar (K)}$
8		lsspropd.p2	$⊢ φ \to P = {Base}_{Scalar (L)}$
9		simpll	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to φ$
10		simprl	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to z \in P$
11		simplr	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to s \subseteq B$
12		simprrl	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to a \in s$
13	11 12	sseldd	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to a \in B$
14	5	ralrimivva	$⊢ φ \to \forall x \in P \forall y \in B x \cdot_{K} y \in W$
15	14	ad2antrr	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to \forall x \in P \forall y \in B x \cdot_{K} y \in W$
16		ovrspc2v	$⊢ ((z \in P \land a \in B) \land \forall x \in P \forall y \in B x \cdot_{K} y \in W) \to z \cdot_{K} a \in W$
17	10 13 15 16	syl21anc	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to z \cdot_{K} a \in W$
18	3	ad2antrr	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to B \subseteq W$
19		simprrr	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to b \in s$
20	11 19	sseldd	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to b \in B$
21	18 20	sseldd	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to b \in W$
22	4	oveqrspc2v	$⊢ (φ \land (z \cdot_{K} a \in W \land b \in W)) \to (z \cdot_{K} a) +_{K} b = (z \cdot_{K} a) +_{L} b$
23	9 17 21 22	syl12anc	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to (z \cdot_{K} a) +_{K} b = (z \cdot_{K} a) +_{L} b$
24	6	oveqrspc2v	$⊢ (φ \land (z \in P \land a \in B)) \to z \cdot_{K} a = z \cdot_{L} a$
25	9 10 13 24	syl12anc	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to z \cdot_{K} a = z \cdot_{L} a$
26	25	oveq1d	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to (z \cdot_{K} a) +_{L} b = (z \cdot_{L} a) +_{L} b$
27	23 26	eqtrd	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to (z \cdot_{K} a) +_{K} b = (z \cdot_{L} a) +_{L} b$
28	27	eleq1d	$⊢ ((φ \land s \subseteq B) \land (z \in P \land (a \in s \land b \in s))) \to ((z \cdot_{K} a) +_{K} b \in s \leftrightarrow (z \cdot_{L} a) +_{L} b \in s)$
29	28	anassrs	$⊢ (((φ \land s \subseteq B) \land z \in P) \land (a \in s \land b \in s)) \to ((z \cdot_{K} a) +_{K} b \in s \leftrightarrow (z \cdot_{L} a) +_{L} b \in s)$
30	29	2ralbidva	$⊢ ((φ \land s \subseteq B) \land z \in P) \to (\forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s \leftrightarrow \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s)$
31	30	ralbidva	$⊢ (φ \land s \subseteq B) \to (\forall z \in P \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s \leftrightarrow \forall z \in P \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s)$
32	31	anbi2d	$⊢ (φ \land s \subseteq B) \to ((s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s) \leftrightarrow (s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s))$
33	32	pm5.32da	$⊢ φ \to ((s \subseteq B \land (s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s)) \leftrightarrow (s \subseteq B \land (s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s)))$
34		3anass	$⊢ (s \subseteq B \land s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s) \leftrightarrow (s \subseteq B \land (s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s))$
35		3anass	$⊢ (s \subseteq B \land s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s) \leftrightarrow (s \subseteq B \land (s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s))$
36	33 34 35	3bitr4g	$⊢ φ \to ((s \subseteq B \land s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s) \leftrightarrow (s \subseteq B \land s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s))$
37	1	sseq2d	$⊢ φ \to (s \subseteq B \leftrightarrow s \subseteq {Base}_{K})$
38	7	raleqdv	$⊢ φ \to (\forall z \in P \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s \leftrightarrow \forall z \in {Base}_{Scalar (K)} \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s)$
39	37 38	3anbi13d	$⊢ φ \to ((s \subseteq B \land s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s) \leftrightarrow (s \subseteq {Base}_{K} \land s \neq \emptyset \land \forall z \in {Base}_{Scalar (K)} \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s))$
40	2	sseq2d	$⊢ φ \to (s \subseteq B \leftrightarrow s \subseteq {Base}_{L})$
41	8	raleqdv	$⊢ φ \to (\forall z \in P \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s \leftrightarrow \forall z \in {Base}_{Scalar (L)} \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s)$
42	40 41	3anbi13d	$⊢ φ \to ((s \subseteq B \land s \neq \emptyset \land \forall z \in P \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s) \leftrightarrow (s \subseteq {Base}_{L} \land s \neq \emptyset \land \forall z \in {Base}_{Scalar (L)} \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s))$
43	36 39 42	3bitr3d	$⊢ φ \to ((s \subseteq {Base}_{K} \land s \neq \emptyset \land \forall z \in {Base}_{Scalar (K)} \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s) \leftrightarrow (s \subseteq {Base}_{L} \land s \neq \emptyset \land \forall z \in {Base}_{Scalar (L)} \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s))$
44		eqid	$⊢ Scalar (K) = Scalar (K)$
45		eqid	$⊢ {Base}_{Scalar (K)} = {Base}_{Scalar (K)}$
46		eqid	$⊢ {Base}_{K} = {Base}_{K}$
47		eqid	$⊢ +_{K} = +_{K}$
48		eqid	$⊢ \cdot_{K} = \cdot_{K}$
49		eqid	$⊢ LSubSp (K) = LSubSp (K)$
50	44 45 46 47 48 49	islss	$⊢ s \in LSubSp (K) \leftrightarrow (s \subseteq {Base}_{K} \land s \neq \emptyset \land \forall z \in {Base}_{Scalar (K)} \forall a \in s \forall b \in s (z \cdot_{K} a) +_{K} b \in s)$
51		eqid	$⊢ Scalar (L) = Scalar (L)$
52		eqid	$⊢ {Base}_{Scalar (L)} = {Base}_{Scalar (L)}$
53		eqid	$⊢ {Base}_{L} = {Base}_{L}$
54		eqid	$⊢ +_{L} = +_{L}$
55		eqid	$⊢ \cdot_{L} = \cdot_{L}$
56		eqid	$⊢ LSubSp (L) = LSubSp (L)$
57	51 52 53 54 55 56	islss	$⊢ s \in LSubSp (L) \leftrightarrow (s \subseteq {Base}_{L} \land s \neq \emptyset \land \forall z \in {Base}_{Scalar (L)} \forall a \in s \forall b \in s (z \cdot_{L} a) +_{L} b \in s)$
58	43 50 57	3bitr4g	$⊢ φ \to (s \in LSubSp (K) \leftrightarrow s \in LSubSp (L))$
59	58	eqrdv	$⊢ φ \to LSubSp (K) = LSubSp (L)$

Metamath Proof Explorer

Theorem lsspropd

Proof