# Metamath Proof Explorer

## 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 𝑈𝐽 )