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 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
lbspropd.b2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
lbspropd.w ( 𝜑𝐵𝑊 )
lbspropd.p ( ( 𝜑 ∧ ( 𝑥𝑊𝑦𝑊 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
lbspropd.s1 ( ( 𝜑 ∧ ( 𝑥𝑃𝑦𝐵 ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) ∈ 𝑊 )
lbspropd.s2 ( ( 𝜑 ∧ ( 𝑥𝑃𝑦𝐵 ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠𝐿 ) 𝑦 ) )
lbspropd.f 𝐹 = ( Scalar ‘ 𝐾 )
lbspropd.g 𝐺 = ( Scalar ‘ 𝐿 )
lbspropd.p1 ( 𝜑𝑃 = ( Base ‘ 𝐹 ) )
lbspropd.p2 ( 𝜑𝑃 = ( Base ‘ 𝐺 ) )
lbspropd.a ( ( 𝜑 ∧ ( 𝑥𝑃𝑦𝑃 ) ) → ( 𝑥 ( +g𝐹 ) 𝑦 ) = ( 𝑥 ( +g𝐺 ) 𝑦 ) )
lbspropd.v1 ( 𝜑𝐾𝑋 )
lbspropd.v2 ( 𝜑𝐿𝑌 )
Assertion lbspropd ( 𝜑 → ( LBasis ‘ 𝐾 ) = ( LBasis ‘ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 lbspropd.b1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
2 lbspropd.b2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
3 lbspropd.w ( 𝜑𝐵𝑊 )
4 lbspropd.p ( ( 𝜑 ∧ ( 𝑥𝑊𝑦𝑊 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
5 lbspropd.s1 ( ( 𝜑 ∧ ( 𝑥𝑃𝑦𝐵 ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) ∈ 𝑊 )
6 lbspropd.s2 ( ( 𝜑 ∧ ( 𝑥𝑃𝑦𝐵 ) ) → ( 𝑥 ( ·𝑠𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠𝐿 ) 𝑦 ) )
7 lbspropd.f 𝐹 = ( Scalar ‘ 𝐾 )
8 lbspropd.g 𝐺 = ( Scalar ‘ 𝐿 )
9 lbspropd.p1 ( 𝜑𝑃 = ( Base ‘ 𝐹 ) )
10 lbspropd.p2 ( 𝜑𝑃 = ( Base ‘ 𝐺 ) )
11 lbspropd.a ( ( 𝜑 ∧ ( 𝑥𝑃𝑦𝑃 ) ) → ( 𝑥 ( +g𝐹 ) 𝑦 ) = ( 𝑥 ( +g𝐺 ) 𝑦 ) )
12 lbspropd.v1 ( 𝜑𝐾𝑋 )
13 lbspropd.v2 ( 𝜑𝐿𝑌 )
14 simplll ( ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ) → 𝜑 )
15 eldifi ( 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) → 𝑣𝑃 )
16 15 adantl ( ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ) → 𝑣𝑃 )
17 simpr ( ( 𝜑𝑧𝐵 ) → 𝑧𝐵 )
18 17 sselda ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → 𝑢𝐵 )
19 18 adantr ( ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ) → 𝑢𝐵 )
20 6 oveqrspc2v ( ( 𝜑 ∧ ( 𝑣𝑃𝑢𝐵 ) ) → ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) = ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) )
21 14 16 19 20 syl12anc ( ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ) → ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) = ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) )
22 7 fveq2i ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐾 ) )
23 9 22 eqtrdi ( 𝜑𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
24 8 fveq2i ( Base ‘ 𝐺 ) = ( Base ‘ ( Scalar ‘ 𝐿 ) )
25 10 24 eqtrdi ( 𝜑𝑃 = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
26 1 2 3 4 5 6 23 25 12 13 lsppropd ( 𝜑 → ( LSpan ‘ 𝐾 ) = ( LSpan ‘ 𝐿 ) )
27 14 26 syl ( ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ) → ( LSpan ‘ 𝐾 ) = ( LSpan ‘ 𝐿 ) )
28 27 fveq1d ( ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ) → ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) = ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) )
29 21 28 eleq12d ( ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ) → ( ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
30 29 notbid ( ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ) → ( ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
31 30 ralbidva ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → ( ∀ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ∀ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
32 9 ad2antrr ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → 𝑃 = ( Base ‘ 𝐹 ) )
33 32 difeq1d ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → ( 𝑃 ∖ { ( 0g𝐹 ) } ) = ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) )
34 33 raleqdv ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → ( ∀ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
35 10 ad2antrr ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → 𝑃 = ( Base ‘ 𝐺 ) )
36 9 10 11 grpidpropd ( 𝜑 → ( 0g𝐹 ) = ( 0g𝐺 ) )
37 36 ad2antrr ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → ( 0g𝐹 ) = ( 0g𝐺 ) )
38 37 sneqd ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → { ( 0g𝐹 ) } = { ( 0g𝐺 ) } )
39 35 38 difeq12d ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → ( 𝑃 ∖ { ( 0g𝐹 ) } ) = ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) )
40 39 raleqdv ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → ( ∀ 𝑣 ∈ ( 𝑃 ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
41 31 34 40 3bitr3d ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑢𝑧 ) → ( ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
42 41 ralbidva ( ( 𝜑𝑧𝐵 ) → ( ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
43 42 anbi2d ( ( 𝜑𝑧𝐵 ) → ( ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ↔ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
44 43 pm5.32da ( 𝜑 → ( ( 𝑧𝐵 ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ↔ ( 𝑧𝐵 ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ) )
45 1 sseq2d ( 𝜑 → ( 𝑧𝐵𝑧 ⊆ ( Base ‘ 𝐾 ) ) )
46 45 anbi1d ( 𝜑 → ( ( 𝑧𝐵 ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ) )
47 2 sseq2d ( 𝜑 → ( 𝑧𝐵𝑧 ⊆ ( Base ‘ 𝐿 ) ) )
48 26 fveq1d ( 𝜑 → ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) )
49 1 2 eqtr3d ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
50 48 49 eqeq12d ( 𝜑 → ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ↔ ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ) )
51 50 anbi1d ( 𝜑 → ( ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ↔ ( ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
52 47 51 anbi12d ( 𝜑 → ( ( 𝑧𝐵 ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ) )
53 44 46 52 3bitr3d ( 𝜑 → ( ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ) )
54 3anass ( ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
55 3anass ( ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
56 53 54 55 3bitr4g ( 𝜑 → ( ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
57 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
58 eqid ( ·𝑠𝐾 ) = ( ·𝑠𝐾 )
59 eqid ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
60 eqid ( LBasis ‘ 𝐾 ) = ( LBasis ‘ 𝐾 )
61 eqid ( LSpan ‘ 𝐾 ) = ( LSpan ‘ 𝐾 )
62 eqid ( 0g𝐹 ) = ( 0g𝐹 )
63 57 7 58 59 60 61 62 islbs ( 𝐾𝑋 → ( 𝑧 ∈ ( LBasis ‘ 𝐾 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
64 12 63 syl ( 𝜑 → ( 𝑧 ∈ ( LBasis ‘ 𝐾 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0g𝐹 ) } ) ¬ ( 𝑣 ( ·𝑠𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
65 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
66 eqid ( ·𝑠𝐿 ) = ( ·𝑠𝐿 )
67 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
68 eqid ( LBasis ‘ 𝐿 ) = ( LBasis ‘ 𝐿 )
69 eqid ( LSpan ‘ 𝐿 ) = ( LSpan ‘ 𝐿 )
70 eqid ( 0g𝐺 ) = ( 0g𝐺 )
71 65 8 66 67 68 69 70 islbs ( 𝐿𝑌 → ( 𝑧 ∈ ( LBasis ‘ 𝐿 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
72 13 71 syl ( 𝜑 → ( 𝑧 ∈ ( LBasis ‘ 𝐿 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢𝑧𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0g𝐺 ) } ) ¬ ( 𝑣 ( ·𝑠𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
73 56 64 72 3bitr4d ( 𝜑 → ( 𝑧 ∈ ( LBasis ‘ 𝐾 ) ↔ 𝑧 ∈ ( LBasis ‘ 𝐿 ) ) )
74 73 eqrdv ( 𝜑 → ( LBasis ‘ 𝐾 ) = ( LBasis ‘ 𝐿 ) )