lbspropd

Description: If two structures have the same components (properties), they have the same set of bases. (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 14-Jun-2015) (Revised by AV, 24-Apr-2024)

	Ref	Expression
Hypotheses	lbspropd.b1	$⊢ φ \to B = {Base}_{K}$
	lbspropd.b2	$⊢ φ \to B = {Base}_{L}$
	lbspropd.w	$⊢ φ \to B \subseteq W$
	lbspropd.p	$⊢ (φ \land (x \in W \land y \in W)) \to x +_{K} y = x +_{L} y$
	lbspropd.s1	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y \in W$
	lbspropd.s2	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
	lbspropd.f	$⊢ F = Scalar (K)$
	lbspropd.g	$⊢ G = Scalar (L)$
	lbspropd.p1	$⊢ φ \to P = {Base}_{F}$
	lbspropd.p2	$⊢ φ \to P = {Base}_{G}$
	lbspropd.a	$⊢ (φ \land (x \in P \land y \in P)) \to x +_{F} y = x +_{G} y$
	lbspropd.v1	$⊢ φ \to K \in X$
	lbspropd.v2	$⊢ φ \to L \in Y$
Assertion	lbspropd	$⊢ φ \to LBasis (K) = LBasis (L)$

Proof

Step	Hyp	Ref	Expression
1		lbspropd.b1	$⊢ φ \to B = {Base}_{K}$
2		lbspropd.b2	$⊢ φ \to B = {Base}_{L}$
3		lbspropd.w	$⊢ φ \to B \subseteq W$
4		lbspropd.p	$⊢ (φ \land (x \in W \land y \in W)) \to x +_{K} y = x +_{L} y$
5		lbspropd.s1	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y \in W$
6		lbspropd.s2	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
7		lbspropd.f	$⊢ F = Scalar (K)$
8		lbspropd.g	$⊢ G = Scalar (L)$
9		lbspropd.p1	$⊢ φ \to P = {Base}_{F}$
10		lbspropd.p2	$⊢ φ \to P = {Base}_{G}$
11		lbspropd.a	$⊢ (φ \land (x \in P \land y \in P)) \to x +_{F} y = x +_{G} y$
12		lbspropd.v1	$⊢ φ \to K \in X$
13		lbspropd.v2	$⊢ φ \to L \in Y$
14		simplll	$⊢ (((φ \land z \subseteq B) \land u \in z) \land v \in (P ∖ \{0_{F}\})) \to φ$
15		eldifi	$⊢ v \in (P ∖ \{0_{F}\}) \to v \in P$
16	15	adantl	$⊢ (((φ \land z \subseteq B) \land u \in z) \land v \in (P ∖ \{0_{F}\})) \to v \in P$
17		simpr	$⊢ (φ \land z \subseteq B) \to z \subseteq B$
18	17	sselda	$⊢ ((φ \land z \subseteq B) \land u \in z) \to u \in B$
19	18	adantr	$⊢ (((φ \land z \subseteq B) \land u \in z) \land v \in (P ∖ \{0_{F}\})) \to u \in B$
20	6	oveqrspc2v	$⊢ (φ \land (v \in P \land u \in B)) \to v \cdot_{K} u = v \cdot_{L} u$
21	14 16 19 20	syl12anc	$⊢ (((φ \land z \subseteq B) \land u \in z) \land v \in (P ∖ \{0_{F}\})) \to v \cdot_{K} u = v \cdot_{L} u$
22	7	fveq2i	$⊢ {Base}_{F} = {Base}_{Scalar (K)}$
23	9 22	syl6eq	$⊢ φ \to P = {Base}_{Scalar (K)}$
24	8	fveq2i	$⊢ {Base}_{G} = {Base}_{Scalar (L)}$
25	10 24	syl6eq	$⊢ φ \to P = {Base}_{Scalar (L)}$
26	1 2 3 4 5 6 23 25 12 13	lsppropd	$⊢ φ \to LSpan (K) = LSpan (L)$
27	14 26	syl	$⊢ (((φ \land z \subseteq B) \land u \in z) \land v \in (P ∖ \{0_{F}\})) \to LSpan (K) = LSpan (L)$
28	27	fveq1d	$⊢ (((φ \land z \subseteq B) \land u \in z) \land v \in (P ∖ \{0_{F}\})) \to LSpan (K) (z ∖ \{u\}) = LSpan (L) (z ∖ \{u\})$
29	21 28	eleq12d	$⊢ (((φ \land z \subseteq B) \land u \in z) \land v \in (P ∖ \{0_{F}\})) \to (v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}) \leftrightarrow v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}))$
30	29	notbid	$⊢ (((φ \land z \subseteq B) \land u \in z) \land v \in (P ∖ \{0_{F}\})) \to (\neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}) \leftrightarrow \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}))$
31	30	ralbidva	$⊢ ((φ \land z \subseteq B) \land u \in z) \to (\forall v \in (P ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}) \leftrightarrow \forall v \in (P ∖ \{0_{F}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}))$
32	9	ad2antrr	$⊢ ((φ \land z \subseteq B) \land u \in z) \to P = {Base}_{F}$
33	32	difeq1d	$⊢ ((φ \land z \subseteq B) \land u \in z) \to P ∖ \{0_{F}\} = {Base}_{F} ∖ \{0_{F}\}$
34	33	raleqdv	$⊢ ((φ \land z \subseteq B) \land u \in z) \to (\forall v \in (P ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}) \leftrightarrow \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}))$
35	10	ad2antrr	$⊢ ((φ \land z \subseteq B) \land u \in z) \to P = {Base}_{G}$
36	9 10 11	grpidpropd	$⊢ φ \to 0_{F} = 0_{G}$
37	36	ad2antrr	$⊢ ((φ \land z \subseteq B) \land u \in z) \to 0_{F} = 0_{G}$
38	37	sneqd	$⊢ ((φ \land z \subseteq B) \land u \in z) \to \{0_{F}\} = \{0_{G}\}$
39	35 38	difeq12d	$⊢ ((φ \land z \subseteq B) \land u \in z) \to P ∖ \{0_{F}\} = {Base}_{G} ∖ \{0_{G}\}$
40	39	raleqdv	$⊢ ((φ \land z \subseteq B) \land u \in z) \to (\forall v \in (P ∖ \{0_{F}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}) \leftrightarrow \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}))$
41	31 34 40	3bitr3d	$⊢ ((φ \land z \subseteq B) \land u \in z) \to (\forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}) \leftrightarrow \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}))$
42	41	ralbidva	$⊢ (φ \land z \subseteq B) \to (\forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}) \leftrightarrow \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}))$
43	42	anbi2d	$⊢ (φ \land z \subseteq B) \to ((LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\})) \leftrightarrow (LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\})))$
44	43	pm5.32da	$⊢ φ \to ((z \subseteq B \land (LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}))) \leftrightarrow (z \subseteq B \land (LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}))))$
45	1	sseq2d	$⊢ φ \to (z \subseteq B \leftrightarrow z \subseteq {Base}_{K})$
46	45	anbi1d	$⊢ φ \to ((z \subseteq B \land (LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}))) \leftrightarrow (z \subseteq {Base}_{K} \land (LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}))))$
47	2	sseq2d	$⊢ φ \to (z \subseteq B \leftrightarrow z \subseteq {Base}_{L})$
48	26	fveq1d	$⊢ φ \to LSpan (K) (z) = LSpan (L) (z)$
49	1 2	eqtr3d	$⊢ φ \to {Base}_{K} = {Base}_{L}$
50	48 49	eqeq12d	$⊢ φ \to (LSpan (K) (z) = {Base}_{K} \leftrightarrow LSpan (L) (z) = {Base}_{L})$
51	50	anbi1d	$⊢ φ \to ((LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\})) \leftrightarrow (LSpan (L) (z) = {Base}_{L} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\})))$
52	47 51	anbi12d	$⊢ φ \to ((z \subseteq B \land (LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}))) \leftrightarrow (z \subseteq {Base}_{L} \land (LSpan (L) (z) = {Base}_{L} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}))))$
53	44 46 52	3bitr3d	$⊢ φ \to ((z \subseteq {Base}_{K} \land (LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\}))) \leftrightarrow (z \subseteq {Base}_{L} \land (LSpan (L) (z) = {Base}_{L} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\}))))$
54		3anass	$⊢ (z \subseteq {Base}_{K} \land LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\})) \leftrightarrow (z \subseteq {Base}_{K} \land (LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\})))$
55		3anass	$⊢ (z \subseteq {Base}_{L} \land LSpan (L) (z) = {Base}_{L} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\})) \leftrightarrow (z \subseteq {Base}_{L} \land (LSpan (L) (z) = {Base}_{L} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\})))$
56	53 54 55	3bitr4g	$⊢ φ \to ((z \subseteq {Base}_{K} \land LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\})) \leftrightarrow (z \subseteq {Base}_{L} \land LSpan (L) (z) = {Base}_{L} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\})))$
57		eqid	$⊢ {Base}_{K} = {Base}_{K}$
58		eqid	$⊢ \cdot_{K} = \cdot_{K}$
59		eqid	$⊢ {Base}_{F} = {Base}_{F}$
60		eqid	$⊢ LBasis (K) = LBasis (K)$
61		eqid	$⊢ LSpan (K) = LSpan (K)$
62		eqid	$⊢ 0_{F} = 0_{F}$
63	57 7 58 59 60 61 62	islbs	$⊢ K \in X \to (z \in LBasis (K) \leftrightarrow (z \subseteq {Base}_{K} \land LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\})))$
64	12 63	syl	$⊢ φ \to (z \in LBasis (K) \leftrightarrow (z \subseteq {Base}_{K} \land LSpan (K) (z) = {Base}_{K} \land \forall u \in z \forall v \in ({Base}_{F} ∖ \{0_{F}\}) \neg v \cdot_{K} u \in LSpan (K) (z ∖ \{u\})))$
65		eqid	$⊢ {Base}_{L} = {Base}_{L}$
66		eqid	$⊢ \cdot_{L} = \cdot_{L}$
67		eqid	$⊢ {Base}_{G} = {Base}_{G}$
68		eqid	$⊢ LBasis (L) = LBasis (L)$
69		eqid	$⊢ LSpan (L) = LSpan (L)$
70		eqid	$⊢ 0_{G} = 0_{G}$
71	65 8 66 67 68 69 70	islbs	$⊢ L \in Y \to (z \in LBasis (L) \leftrightarrow (z \subseteq {Base}_{L} \land LSpan (L) (z) = {Base}_{L} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\})))$
72	13 71	syl	$⊢ φ \to (z \in LBasis (L) \leftrightarrow (z \subseteq {Base}_{L} \land LSpan (L) (z) = {Base}_{L} \land \forall u \in z \forall v \in ({Base}_{G} ∖ \{0_{G}\}) \neg v \cdot_{L} u \in LSpan (L) (z ∖ \{u\})))$
73	56 64 72	3bitr4d	$⊢ φ \to (z \in LBasis (K) \leftrightarrow z \in LBasis (L))$
74	73	eqrdv	$⊢ φ \to LBasis (K) = LBasis (L)$

Metamath Proof Explorer

Theorem lbspropd

Proof