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 ‘ 𝐿 ) )