Metamath Proof Explorer


Theorem 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 φ B = Base K
lbspropd.b2 φ B = Base L
lbspropd.w φ B W
lbspropd.p φ x W y W x + K y = x + L y
lbspropd.s1 φ x P y B x K y W
lbspropd.s2 φ x P y B x K y = x L y
lbspropd.f F = Scalar K
lbspropd.g G = Scalar L
lbspropd.p1 φ P = Base F
lbspropd.p2 φ P = Base G
lbspropd.a φ x P y P x + F y = x + G y
lbspropd.v1 φ K X
lbspropd.v2 φ L Y
Assertion lbspropd φ LBasis K = LBasis L

Proof

Step Hyp Ref Expression
1 lbspropd.b1 φ B = Base K
2 lbspropd.b2 φ B = Base L
3 lbspropd.w φ B W
4 lbspropd.p φ x W y W x + K y = x + L y
5 lbspropd.s1 φ x P y B x K y W
6 lbspropd.s2 φ x P y B x K y = x L y
7 lbspropd.f F = Scalar K
8 lbspropd.g G = Scalar L
9 lbspropd.p1 φ P = Base F
10 lbspropd.p2 φ P = Base G
11 lbspropd.a φ x P y P x + F y = x + G y
12 lbspropd.v1 φ K X
13 lbspropd.v2 φ L Y
14 simplll φ z B u z v P 0 F φ
15 eldifi v P 0 F v P
16 15 adantl φ z B u z v P 0 F v P
17 simpr φ z B z B
18 17 sselda φ z B u z u B
19 18 adantr φ z B u z v P 0 F u B
20 6 oveqrspc2v φ v P u B v K u = v L u
21 14 16 19 20 syl12anc φ z B u z v P 0 F v K u = v L u
22 7 fveq2i Base F = Base Scalar K
23 9 22 eqtrdi φ P = Base Scalar K
24 8 fveq2i Base G = Base Scalar L
25 10 24 eqtrdi φ P = Base Scalar L
26 1 2 3 4 5 6 23 25 12 13 lsppropd φ LSpan K = LSpan L
27 14 26 syl φ z B u z v P 0 F LSpan K = LSpan L
28 27 fveq1d φ z B u z v P 0 F LSpan K z u = LSpan L z u
29 21 28 eleq12d φ z B u z v P 0 F v K u LSpan K z u v L u LSpan L z u
30 29 notbid φ z B u z v P 0 F ¬ v K u LSpan K z u ¬ v L u LSpan L z u
31 30 ralbidva φ z B u z v P 0 F ¬ v K u LSpan K z u v P 0 F ¬ v L u LSpan L z u
32 9 ad2antrr φ z B u z P = Base F
33 32 difeq1d φ z B u z P 0 F = Base F 0 F
34 33 raleqdv φ z B u z v P 0 F ¬ v K u LSpan K z u v Base F 0 F ¬ v K u LSpan K z u
35 10 ad2antrr φ z B u z P = Base G
36 9 10 11 grpidpropd φ 0 F = 0 G
37 36 ad2antrr φ z B u z 0 F = 0 G
38 37 sneqd φ z B u z 0 F = 0 G
39 35 38 difeq12d φ z B u z P 0 F = Base G 0 G
40 39 raleqdv φ z B u z v P 0 F ¬ v L u LSpan L z u v Base G 0 G ¬ v L u LSpan L z u
41 31 34 40 3bitr3d φ z B u z v Base F 0 F ¬ v K u LSpan K z u v Base G 0 G ¬ v L u LSpan L z u
42 41 ralbidva φ z B u z v Base F 0 F ¬ v K u LSpan K z u u z v Base G 0 G ¬ v L u LSpan L z u
43 42 anbi2d φ z B LSpan K z = Base K u z v Base F 0 F ¬ v K u LSpan K z u LSpan K z = Base K u z v Base G 0 G ¬ v L u LSpan L z u
44 43 pm5.32da φ z B LSpan K z = Base K u z v Base F 0 F ¬ v K u LSpan K z u z B LSpan K z = Base K u z v Base G 0 G ¬ v L u LSpan L z u
45 1 sseq2d φ z B z Base K
46 45 anbi1d φ z B LSpan K z = Base K u z v Base F 0 F ¬ v K u LSpan K z u z Base K LSpan K z = Base K u z v Base F 0 F ¬ v K u LSpan K z u
47 2 sseq2d φ z B z Base L
48 26 fveq1d φ LSpan K z = LSpan L z
49 1 2 eqtr3d φ Base K = Base L
50 48 49 eqeq12d φ LSpan K z = Base K LSpan L z = Base L
51 50 anbi1d φ LSpan K z = Base K u z v Base G 0 G ¬ v L u LSpan L z u LSpan L z = Base L u z v Base G 0 G ¬ v L u LSpan L z u
52 47 51 anbi12d φ z B LSpan K z = Base K u z v Base G 0 G ¬ v L u LSpan L z u z Base L LSpan L z = Base L u z v Base G 0 G ¬ v L u LSpan L z u
53 44 46 52 3bitr3d φ z Base K LSpan K z = Base K u z v Base F 0 F ¬ v K u LSpan K z u z Base L LSpan L z = Base L u z v Base G 0 G ¬ v L u LSpan L z u
54 3anass z Base K LSpan K z = Base K u z v Base F 0 F ¬ v K u LSpan K z u z Base K LSpan K z = Base K u z v Base F 0 F ¬ v K u LSpan K z u
55 3anass z Base L LSpan L z = Base L u z v Base G 0 G ¬ v L u LSpan L z u z Base L LSpan L z = Base L u z v Base G 0 G ¬ v L u LSpan L z u
56 53 54 55 3bitr4g φ z Base K LSpan K z = Base K u z v Base F 0 F ¬ v K u LSpan K z u z Base L LSpan L z = Base L u z v Base G 0 G ¬ v L u LSpan L z u
57 eqid Base K = Base K
58 eqid K = 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 X z LBasis K z Base K LSpan K z = Base K u z v Base F 0 F ¬ v K u LSpan K z u
64 12 63 syl φ z LBasis K z Base K LSpan K z = Base K u z v Base F 0 F ¬ v K u LSpan K z u
65 eqid Base L = Base L
66 eqid L = 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 Y z LBasis L z Base L LSpan L z = Base L u z v Base G 0 G ¬ v L u LSpan L z u
72 13 71 syl φ z LBasis L z Base L LSpan L z = Base L u z v Base G 0 G ¬ v L u LSpan L z u
73 56 64 72 3bitr4d φ z LBasis K z LBasis L
74 73 eqrdv φ LBasis K = LBasis L