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	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ) → 𝜑 )
15		eldifi	⊢ ( 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) → 𝑣 ∈ 𝑃 )
16	15	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ) → 𝑣 ∈ 𝑃 )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) → 𝑧 ⊆ 𝐵 )
18	17	sselda	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → 𝑢 ∈ 𝐵 )
19	18	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ) → 𝑢 ∈ 𝐵 )
20	6	oveqrspc2v	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝑃 ∧ 𝑢 ∈ 𝐵 ) ) → ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) = ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) )
21	14 16 19 20	syl12anc	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ) → ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) = ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) )
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	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ) → ( LSpan ‘ 𝐾 ) = ( LSpan ‘ 𝐿 ) )
28	27	fveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ) → ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) = ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) )
29	21 28	eleq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ) → ( ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
30	29	notbid	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) ∧ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ) → ( ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
31	30	ralbidva	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → ( ∀ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ∀ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
32	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → 𝑃 = ( Base ‘ 𝐹 ) )
33	32	difeq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) = ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) )
34	33	raleqdv	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → ( ∀ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
35	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → 𝑃 = ( Base ‘ 𝐺 ) )
36	9 10 11	grpidpropd	⊢ ( 𝜑 → ( 0_g ‘ 𝐹 ) = ( 0_g ‘ 𝐺 ) )
37	36	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → ( 0_g ‘ 𝐹 ) = ( 0_g ‘ 𝐺 ) )
38	37	sneqd	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → { ( 0_g ‘ 𝐹 ) } = { ( 0_g ‘ 𝐺 ) } )
39	35 38	difeq12d	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) = ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) )
40	39	raleqdv	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → ( ∀ 𝑣 ∈ ( 𝑃 ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
41	31 34 40	3bitr3d	⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑢 ∈ 𝑧 ) → ( ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
42	41	ralbidva	⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) → ( ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ↔ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) )
43	42	anbi2d	⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) → ( ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ↔ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
44	43	pm5.32da	⊢ ( 𝜑 → ( ( 𝑧 ⊆ 𝐵 ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ↔ ( 𝑧 ⊆ 𝐵 ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ) )
45	1	sseq2d	⊢ ( 𝜑 → ( 𝑧 ⊆ 𝐵 ↔ 𝑧 ⊆ ( Base ‘ 𝐾 ) ) )
46	45	anbi1d	⊢ ( 𝜑 → ( ( 𝑧 ⊆ 𝐵 ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( 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 ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ↔ ( ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
52	47 51	anbi12d	⊢ ( 𝜑 → ( ( 𝑧 ⊆ 𝐵 ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ) )
53	44 46 52	3bitr3d	⊢ ( 𝜑 → ( ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) ) )
54		3anass	⊢ ( ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
55		3anass	⊢ ( ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
56	53 54 55	3bitr4g	⊢ ( 𝜑 → ( ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
57		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
58		eqid	⊢ ( ·_𝑠 ‘ 𝐾 ) = ( ·_𝑠 ‘ 𝐾 )
59		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
60		eqid	⊢ ( LBasis ‘ 𝐾 ) = ( LBasis ‘ 𝐾 )
61		eqid	⊢ ( LSpan ‘ 𝐾 ) = ( LSpan ‘ 𝐾 )
62		eqid	⊢ ( 0_g ‘ 𝐹 ) = ( 0_g ‘ 𝐹 )
63	57 7 58 59 60 61 62	islbs	⊢ ( 𝐾 ∈ 𝑋 → ( 𝑧 ∈ ( LBasis ‘ 𝐾 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
64	12 63	syl	⊢ ( 𝜑 → ( 𝑧 ∈ ( LBasis ‘ 𝐾 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐾 ) ∧ ( ( LSpan ‘ 𝐾 ) ‘ 𝑧 ) = ( Base ‘ 𝐾 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐹 ) ∖ { ( 0_g ‘ 𝐹 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐾 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
65		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
66		eqid	⊢ ( ·_𝑠 ‘ 𝐿 ) = ( ·_𝑠 ‘ 𝐿 )
67		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
68		eqid	⊢ ( LBasis ‘ 𝐿 ) = ( LBasis ‘ 𝐿 )
69		eqid	⊢ ( LSpan ‘ 𝐿 ) = ( LSpan ‘ 𝐿 )
70		eqid	⊢ ( 0_g ‘ 𝐺 ) = ( 0_g ‘ 𝐺 )
71	65 8 66 67 68 69 70	islbs	⊢ ( 𝐿 ∈ 𝑌 → ( 𝑧 ∈ ( LBasis ‘ 𝐿 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
72	13 71	syl	⊢ ( 𝜑 → ( 𝑧 ∈ ( LBasis ‘ 𝐿 ) ↔ ( 𝑧 ⊆ ( Base ‘ 𝐿 ) ∧ ( ( LSpan ‘ 𝐿 ) ‘ 𝑧 ) = ( Base ‘ 𝐿 ) ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ ( ( Base ‘ 𝐺 ) ∖ { ( 0_g ‘ 𝐺 ) } ) ¬ ( 𝑣 ( ·_𝑠 ‘ 𝐿 ) 𝑢 ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑧 ∖ { 𝑢 } ) ) ) ) )
73	56 64 72	3bitr4d	⊢ ( 𝜑 → ( 𝑧 ∈ ( LBasis ‘ 𝐾 ) ↔ 𝑧 ∈ ( LBasis ‘ 𝐿 ) ) )
74	73	eqrdv	⊢ ( 𝜑 → ( LBasis ‘ 𝐾 ) = ( LBasis ‘ 𝐿 ) )

Metamath Proof Explorer

Theorem lbspropd

Proof