Theorem lindsrng01

Description: Any subset of a module is always linearly independent if the underlying ring has at most one element. Since the underlying ring cannot be the empty set (see lmodsn0 ), this means that the underlying ring has only one element, so it is a zero ring. (Contributed by AV, 14-Apr-2019) (Revised by AV, 27-Apr-2019)

	Ref	Expression
Hypotheses	lindsrng01.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	lindsrng01.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
	lindsrng01.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
Assertion	lindsrng01	⊢ ( ( 𝑀 ∈ LMod ∧ ( ( ♯ ‘ 𝐸 ) = 0 ∨ ( ♯ ‘ 𝐸 ) = 1 ) ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑆 linIndS 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		lindsrng01.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		lindsrng01.r	⊢ 𝑅 = ( Scalar ‘ 𝑀 )
3		lindsrng01.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
4	2 3	lmodsn0	⊢ ( 𝑀 ∈ LMod → 𝐸 ≠ ∅ )
5	3	fvexi	⊢ 𝐸 ∈ V
6		hasheq0	⊢ ( 𝐸 ∈ V → ( ( ♯ ‘ 𝐸 ) = 0 ↔ 𝐸 = ∅ ) )
7	5 6	ax-mp	⊢ ( ( ♯ ‘ 𝐸 ) = 0 ↔ 𝐸 = ∅ )
8		eqneqall	⊢ ( 𝐸 = ∅ → ( 𝐸 ≠ ∅ → 𝑆 linIndS 𝑀 ) )
9	8	com12	⊢ ( 𝐸 ≠ ∅ → ( 𝐸 = ∅ → 𝑆 linIndS 𝑀 ) )
10	7 9	syl5bi	⊢ ( 𝐸 ≠ ∅ → ( ( ♯ ‘ 𝐸 ) = 0 → 𝑆 linIndS 𝑀 ) )
11	4 10	syl	⊢ ( 𝑀 ∈ LMod → ( ( ♯ ‘ 𝐸 ) = 0 → 𝑆 linIndS 𝑀 ) )
12	11	adantr	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( ( ♯ ‘ 𝐸 ) = 0 → 𝑆 linIndS 𝑀 ) )
13	12	com12	⊢ ( ( ♯ ‘ 𝐸 ) = 0 → ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑆 linIndS 𝑀 ) )
14	2	lmodring	⊢ ( 𝑀 ∈ LMod → 𝑅 ∈ Ring )
15	14	adantr	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑅 ∈ Ring )
16		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17	3 16	0ring	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐸 ) = 1 ) → 𝐸 = { ( 0g ‘ 𝑅 ) } )
18	15 17	sylan	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) → 𝐸 = { ( 0g ‘ 𝑅 ) } )
19		simpr	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑆 ∈ 𝒫 𝐵 )
20	19	adantr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) → 𝑆 ∈ 𝒫 𝐵 )
21	20	adantl	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → 𝑆 ∈ 𝒫 𝐵 )
22		snex	⊢ { ( 0g ‘ 𝑅 ) } ∈ V
23	20 22	jctil	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) → ( { ( 0g ‘ 𝑅 ) } ∈ V ∧ 𝑆 ∈ 𝒫 𝐵 ) )
24	23	adantl	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ( { ( 0g ‘ 𝑅 ) } ∈ V ∧ 𝑆 ∈ 𝒫 𝐵 ) )
25		elmapg	⊢ ( ( { ( 0g ‘ 𝑅 ) } ∈ V ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑓 ∈ ( { ( 0g ‘ 𝑅 ) } ↑m 𝑆 ) ↔ 𝑓 : 𝑆 ⟶ { ( 0g ‘ 𝑅 ) } ) )
26	24 25	syl	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ( 𝑓 ∈ ( { ( 0g ‘ 𝑅 ) } ↑m 𝑆 ) ↔ 𝑓 : 𝑆 ⟶ { ( 0g ‘ 𝑅 ) } ) )
27		fvex	⊢ ( 0g ‘ 𝑅 ) ∈ V
28	27	fconst2	⊢ ( 𝑓 : 𝑆 ⟶ { ( 0g ‘ 𝑅 ) } ↔ 𝑓 = ( 𝑆 × { ( 0g ‘ 𝑅 ) } ) )
29		fconstmpt	⊢ ( 𝑆 × { ( 0g ‘ 𝑅 ) } ) = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) )
30	29	eqeq2i	⊢ ( 𝑓 = ( 𝑆 × { ( 0g ‘ 𝑅 ) } ) ↔ 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) )
31	28 30	bitri	⊢ ( 𝑓 : 𝑆 ⟶ { ( 0g ‘ 𝑅 ) } ↔ 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) )
32		eqidd	⊢ ( ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) ∧ 𝑣 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) )
33		eqidd	⊢ ( ( ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) ∧ 𝑣 ∈ 𝑆 ) ∧ 𝑥 = 𝑣 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
34		simpr	⊢ ( ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) ∧ 𝑣 ∈ 𝑆 ) → 𝑣 ∈ 𝑆 )
35		fvexd	⊢ ( ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) ∧ 𝑣 ∈ 𝑆 ) → ( 0g ‘ 𝑅 ) ∈ V )
36	32 33 34 35	fvmptd	⊢ ( ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) ∧ 𝑣 ∈ 𝑆 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) )
37	36	ralrimiva	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ∀ 𝑣 ∈ 𝑆 ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) )
38	37	a1d	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ( ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) finSupp ( 0g ‘ 𝑅 ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) )
39		breq1	⊢ ( 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) → ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ↔ ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) finSupp ( 0g ‘ 𝑅 ) ) )
40		oveq1	⊢ ( 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) → ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ( linC ‘ 𝑀 ) 𝑆 ) )
41	40	eqeq1d	⊢ ( 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) )
42	39 41	anbi12d	⊢ ( 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) → ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) finSupp ( 0g ‘ 𝑅 ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) ) )
43		fveq1	⊢ ( 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) → ( 𝑓 ‘ 𝑣 ) = ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ‘ 𝑣 ) )
44	43	eqeq1d	⊢ ( 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) → ( ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) )
45	44	ralbidv	⊢ ( 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) → ( ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ↔ ∀ 𝑣 ∈ 𝑆 ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) )
46	42 45	imbi12d	⊢ ( 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) → ( ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ↔ ( ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) finSupp ( 0g ‘ 𝑅 ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ) )
47	38 46	syl5ibrcom	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ( 𝑓 = ( 𝑥 ∈ 𝑆 ↦ ( 0g ‘ 𝑅 ) ) → ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ) )
48	31 47	syl5bi	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ( 𝑓 : 𝑆 ⟶ { ( 0g ‘ 𝑅 ) } → ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ) )
49	26 48	sylbid	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ( 𝑓 ∈ ( { ( 0g ‘ 𝑅 ) } ↑m 𝑆 ) → ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ) )
50	49	ralrimiv	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ∀ 𝑓 ∈ ( { ( 0g ‘ 𝑅 ) } ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) )
51		oveq1	⊢ ( 𝐸 = { ( 0g ‘ 𝑅 ) } → ( 𝐸 ↑m 𝑆 ) = ( { ( 0g ‘ 𝑅 ) } ↑m 𝑆 ) )
52	51	raleqdv	⊢ ( 𝐸 = { ( 0g ‘ 𝑅 ) } → ( ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑓 ∈ ( { ( 0g ‘ 𝑅 ) } ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ) )
53	52	adantr	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ( ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑓 ∈ ( { ( 0g ‘ 𝑅 ) } ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ) )
54	50 53	mpbird	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) )
55		simpl	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) )
56	55	ancomd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) → ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ) )
57	56	adantl	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ) )
58		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
59	1 58 2 3 16	islininds	⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ) ) )
60	57 59	syl	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ 𝑅 ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑣 ∈ 𝑆 ( 𝑓 ‘ 𝑣 ) = ( 0g ‘ 𝑅 ) ) ) ) )
61	21 54 60	mpbir2and	⊢ ( ( 𝐸 = { ( 0g ‘ 𝑅 ) } ∧ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) ) → 𝑆 linIndS 𝑀 )
62	18 61	mpancom	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ ( ♯ ‘ 𝐸 ) = 1 ) → 𝑆 linIndS 𝑀 )
63	62	expcom	⊢ ( ( ♯ ‘ 𝐸 ) = 1 → ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑆 linIndS 𝑀 ) )
64	13 63	jaoi	⊢ ( ( ( ♯ ‘ 𝐸 ) = 0 ∨ ( ♯ ‘ 𝐸 ) = 1 ) → ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑆 linIndS 𝑀 ) )
65	64	expd	⊢ ( ( ( ♯ ‘ 𝐸 ) = 0 ∨ ( ♯ ‘ 𝐸 ) = 1 ) → ( 𝑀 ∈ LMod → ( 𝑆 ∈ 𝒫 𝐵 → 𝑆 linIndS 𝑀 ) ) )
66	65	com12	⊢ ( 𝑀 ∈ LMod → ( ( ( ♯ ‘ 𝐸 ) = 0 ∨ ( ♯ ‘ 𝐸 ) = 1 ) → ( 𝑆 ∈ 𝒫 𝐵 → 𝑆 linIndS 𝑀 ) ) )
67	66	3imp	⊢ ( ( 𝑀 ∈ LMod ∧ ( ( ♯ ‘ 𝐸 ) = 0 ∨ ( ♯ ‘ 𝐸 ) = 1 ) ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑆 linIndS 𝑀 )