Theorem frlmlbs

Description: The unit vectors comprise a basis for a free module. (Contributed by Stefan O'Rear, 6-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Hypotheses	frlmlbs.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmlbs.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
	frlmlbs.j	⊢ 𝐽 = ( LBasis ‘ 𝐹 )
Assertion	frlmlbs	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ran 𝑈 ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		frlmlbs.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmlbs.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
3		frlmlbs.j	⊢ 𝐽 = ( LBasis ‘ 𝐹 )
4		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
5	2 1 4	uvcff	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐹 ) )
6	5	frnd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ran 𝑈 ⊆ ( Base ‘ 𝐹 ) )
7		suppssdm	⊢ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ dom 𝑎
8		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9	1 8 4	frlmbasf	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑎 ∈ ( Base ‘ 𝐹 ) ) → 𝑎 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
10	9	adantll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑎 ∈ ( Base ‘ 𝐹 ) ) → 𝑎 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
11	7 10	fssdm	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑎 ∈ ( Base ‘ 𝐹 ) ) → ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 )
12	11	ralrimiva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ∀ 𝑎 ∈ ( Base ‘ 𝐹 ) ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 )
13		rabid2	⊢ ( ( Base ‘ 𝐹 ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 } ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐹 ) ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 )
14	12 13	sylibr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( Base ‘ 𝐹 ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 } )
15		ssid	⊢ 𝐼 ⊆ 𝐼
16		eqid	⊢ ( LSpan ‘ 𝐹 ) = ( LSpan ‘ 𝐹 )
17		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18		eqid	⊢ { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 } = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 }
19	1 2 16 4 17 18	frlmsslsp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐼 ⊆ 𝐼 ) → ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ 𝐼 ) ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 } )
20	15 19	mp3an3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ 𝐼 ) ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ 𝐼 } )
21		ffn	⊢ ( 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐹 ) → 𝑈 Fn 𝐼 )
22		fnima	⊢ ( 𝑈 Fn 𝐼 → ( 𝑈 “ 𝐼 ) = ran 𝑈 )
23	5 21 22	3syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 𝑈 “ 𝐼 ) = ran 𝑈 )
24	23	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ 𝐼 ) ) = ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) )
25	14 20 24	3eqtr2rd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) = ( Base ‘ 𝐹 ) )
26		eqid	⊢ ( ·𝑠 ‘ 𝐹 ) = ( ·𝑠 ‘ 𝐹 )
27		eqid	⊢ { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) } = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) }
28		simpll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑅 ∈ Ring )
29		simplr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝐼 ∈ 𝑉 )
30		difssd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( 𝐼 ∖ { 𝑐 } ) ⊆ 𝐼 )
31		vsnid	⊢ 𝑐 ∈ { 𝑐 }
32		snssi	⊢ ( 𝑐 ∈ 𝐼 → { 𝑐 } ⊆ 𝐼 )
33	32	ad2antrl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → { 𝑐 } ⊆ 𝐼 )
34		dfss4	⊢ ( { 𝑐 } ⊆ 𝐼 ↔ ( 𝐼 ∖ ( 𝐼 ∖ { 𝑐 } ) ) = { 𝑐 } )
35	33 34	sylib	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( 𝐼 ∖ ( 𝐼 ∖ { 𝑐 } ) ) = { 𝑐 } )
36	31 35	eleqtrrid	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑐 ∈ ( 𝐼 ∖ ( 𝐼 ∖ { 𝑐 } ) ) )
37	1	frlmsca	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
38	37	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
39	37	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝐹 ) ) )
40	39	sneqd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → { ( 0g ‘ 𝑅 ) } = { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } )
41	38 40	difeq12d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) = ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) )
42	41	eleq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( 𝑏 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ↔ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) )
43	42	biimpar	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) → 𝑏 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
44	43	adantrl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑏 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
45	1 2 4 8 26 17 27 28 29 30 36 44	frlmssuvc2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) } )
46	17 8	ringelnzr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑏 ∈ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) → 𝑅 ∈ NzRing )
47	28 44 46	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑅 ∈ NzRing )
48	2 1 4	uvcf1	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑉 ) → 𝑈 : 𝐼 –1-1→ ( Base ‘ 𝐹 ) )
49	47 29 48	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑈 : 𝐼 –1-1→ ( Base ‘ 𝐹 ) )
50		df-f1	⊢ ( 𝑈 : 𝐼 –1-1→ ( Base ‘ 𝐹 ) ↔ ( 𝑈 : 𝐼 ⟶ ( Base ‘ 𝐹 ) ∧ Fun ◡ 𝑈 ) )
51	50	simprbi	⊢ ( 𝑈 : 𝐼 –1-1→ ( Base ‘ 𝐹 ) → Fun ◡ 𝑈 )
52		imadif	⊢ ( Fun ◡ 𝑈 → ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) = ( ( 𝑈 “ 𝐼 ) ∖ ( 𝑈 “ { 𝑐 } ) ) )
53	49 51 52	3syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) = ( ( 𝑈 “ 𝐼 ) ∖ ( 𝑈 “ { 𝑐 } ) ) )
54		f1fn	⊢ ( 𝑈 : 𝐼 –1-1→ ( Base ‘ 𝐹 ) → 𝑈 Fn 𝐼 )
55	49 54 22	3syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( 𝑈 “ 𝐼 ) = ran 𝑈 )
56	49 54	syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑈 Fn 𝐼 )
57		simprl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → 𝑐 ∈ 𝐼 )
58		fnsnfv	⊢ ( ( 𝑈 Fn 𝐼 ∧ 𝑐 ∈ 𝐼 ) → { ( 𝑈 ‘ 𝑐 ) } = ( 𝑈 “ { 𝑐 } ) )
59	56 57 58	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → { ( 𝑈 ‘ 𝑐 ) } = ( 𝑈 “ { 𝑐 } ) )
60	59	eqcomd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( 𝑈 “ { 𝑐 } ) = { ( 𝑈 ‘ 𝑐 ) } )
61	55 60	difeq12d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( ( 𝑈 “ 𝐼 ) ∖ ( 𝑈 “ { 𝑐 } ) ) = ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) )
62	53 61	eqtr2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) = ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) )
63	62	fveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) = ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) ) )
64	1 2 16 4 17 27	frlmsslsp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ ( 𝐼 ∖ { 𝑐 } ) ⊆ 𝐼 ) → ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) } )
65	28 29 30 64	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( ( LSpan ‘ 𝐹 ) ‘ ( 𝑈 “ ( 𝐼 ∖ { 𝑐 } ) ) ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) } )
66	63 65	eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) = { 𝑎 ∈ ( Base ‘ 𝐹 ) ∣ ( 𝑎 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐼 ∖ { 𝑐 } ) } )
67	45 66	neleqtrrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐼 ∧ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ) ) → ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) )
68	67	ralrimivva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ∀ 𝑐 ∈ 𝐼 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) )
69		oveq2	⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) = ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) )
70		sneq	⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → { 𝑎 } = { ( 𝑈 ‘ 𝑐 ) } )
71	70	difeq2d	⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( ran 𝑈 ∖ { 𝑎 } ) = ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) )
72	71	fveq2d	⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) = ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) )
73	69 72	eleq12d	⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ↔ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) ) )
74	73	notbid	⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ↔ ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) ) )
75	74	ralbidv	⊢ ( 𝑎 = ( 𝑈 ‘ 𝑐 ) → ( ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ↔ ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) ) )
76	75	ralrn	⊢ ( 𝑈 Fn 𝐼 → ( ∀ 𝑎 ∈ ran 𝑈 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ↔ ∀ 𝑐 ∈ 𝐼 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) ) )
77	5 21 76	3syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ( ∀ 𝑎 ∈ ran 𝑈 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ↔ ∀ 𝑐 ∈ 𝐼 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) ( 𝑈 ‘ 𝑐 ) ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { ( 𝑈 ‘ 𝑐 ) } ) ) ) )
78	68 77	mpbird	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ∀ 𝑎 ∈ ran 𝑈 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) )
79	1	ovexi	⊢ 𝐹 ∈ V
80		eqid	⊢ ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
81		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐹 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) )
82		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝐹 ) ) = ( 0g ‘ ( Scalar ‘ 𝐹 ) )
83	4 80 26 81 3 16 82	islbs	⊢ ( 𝐹 ∈ V → ( ran 𝑈 ∈ 𝐽 ↔ ( ran 𝑈 ⊆ ( Base ‘ 𝐹 ) ∧ ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) = ( Base ‘ 𝐹 ) ∧ ∀ 𝑎 ∈ ran 𝑈 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ) ) )
84	79 83	ax-mp	⊢ ( ran 𝑈 ∈ 𝐽 ↔ ( ran 𝑈 ⊆ ( Base ‘ 𝐹 ) ∧ ( ( LSpan ‘ 𝐹 ) ‘ ran 𝑈 ) = ( Base ‘ 𝐹 ) ∧ ∀ 𝑎 ∈ ran 𝑈 ∀ 𝑏 ∈ ( ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐹 ) ) } ) ¬ ( 𝑏 ( ·𝑠 ‘ 𝐹 ) 𝑎 ) ∈ ( ( LSpan ‘ 𝐹 ) ‘ ( ran 𝑈 ∖ { 𝑎 } ) ) ) )
85	6 25 78 84	syl3anbrc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → ran 𝑈 ∈ 𝐽 )