Theorem ldepsnlinclem2

Description: Lemma 2 for ldepsnlinc . (Contributed by AV, 25-May-2019) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypotheses	zlmodzxzldep.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
	zlmodzxzldep.a	⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
	zlmodzxzldep.b	⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
Assertion	ldepsnlinclem2	⊢ ( 𝐹 ∈ ( ( Base ‘ ℤring ) ↑m { 𝐴 } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		zlmodzxzldep.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2		zlmodzxzldep.a	⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
3		zlmodzxzldep.b	⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
4		elmapi	⊢ ( 𝐹 ∈ ( ( Base ‘ ℤring ) ↑m { 𝐴 } ) → 𝐹 : { 𝐴 } ⟶ ( Base ‘ ℤring ) )
5		prex	⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ V
6	2 5	eqeltri	⊢ 𝐴 ∈ V
7	6	fsn2	⊢ ( 𝐹 : { 𝐴 } ⟶ ( Base ‘ ℤring ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )
8		oveq1	⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑍 ) { 𝐴 } ) )
9	8	adantl	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑍 ) { 𝐴 } ) )
10	1	zlmodzxzlmod	⊢ ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) )
11	10	simpli	⊢ 𝑍 ∈ LMod
12	11	a1i	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → 𝑍 ∈ LMod )
13		3z	⊢ 3 ∈ ℤ
14		6nn	⊢ 6 ∈ ℕ
15	14	nnzi	⊢ 6 ∈ ℤ
16	1	zlmodzxzel	⊢ ( ( 3 ∈ ℤ ∧ 6 ∈ ℤ ) → { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ 𝑍 ) )
17	13 15 16	mp2an	⊢ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ∈ ( Base ‘ 𝑍 )
18	2 17	eqeltri	⊢ 𝐴 ∈ ( Base ‘ 𝑍 )
19	18	a1i	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → 𝐴 ∈ ( Base ‘ 𝑍 ) )
20		simpl	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) )
21		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
22	10	simpri	⊢ ℤring = ( Scalar ‘ 𝑍 )
23		eqid	⊢ ( Base ‘ ℤring ) = ( Base ‘ ℤring )
24		eqid	⊢ ( ·𝑠 ‘ 𝑍 ) = ( ·𝑠 ‘ 𝑍 )
25	21 22 23 24	lincvalsng	⊢ ( ( 𝑍 ∈ LMod ∧ 𝐴 ∈ ( Base ‘ 𝑍 ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑍 ) { 𝐴 } ) = ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) )
26	12 19 20 25	syl3anc	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ( linC ‘ 𝑍 ) { 𝐴 } ) = ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) )
27	9 26	eqtrd	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) = ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) )
28		eqid	⊢ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
29		eqid	⊢ ( -g ‘ 𝑍 ) = ( -g ‘ 𝑍 )
30	1 28 24 29 2 3	zlmodzxznm	⊢ ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 )
31		r19.26	⊢ ( ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) ↔ ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) )
32		oveq1	⊢ ( 𝑖 = ( 𝐹 ‘ 𝐴 ) → ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) = ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) )
33	32	neeq1d	⊢ ( 𝑖 = ( 𝐹 ‘ 𝐴 ) → ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ↔ ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) )
34	33	rspcv	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℤ → ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) )
35		zringbas	⊢ ℤ = ( Base ‘ ℤring )
36	35	eqcomi	⊢ ( Base ‘ ℤring ) = ℤ
37	36	eleq2i	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ↔ ( 𝐹 ‘ 𝐴 ) ∈ ℤ )
38	37	birani	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → ( 𝐹 ‘ 𝐴 ) ∈ ℤ )
39	34 38	syl11	⊢ ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 → ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) )
40	39	adantr	⊢ ( ( ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ∀ 𝑖 ∈ ℤ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) )
41	31 40	sylbi	⊢ ( ∀ 𝑖 ∈ ℤ ( ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ∧ ( 𝑖 ( ·𝑠 ‘ 𝑍 ) 𝐵 ) ≠ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 ) )
42	30 41	ax-mp	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → ( ( 𝐹 ‘ 𝐴 ) ( ·𝑠 ‘ 𝑍 ) 𝐴 ) ≠ 𝐵 )
43	27 42	eqnetrd	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ ℤring ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 )
44	7 43	sylbi	⊢ ( 𝐹 : { 𝐴 } ⟶ ( Base ‘ ℤring ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 )
45	4 44	syl	⊢ ( 𝐹 ∈ ( ( Base ‘ ℤring ) ↑m { 𝐴 } ) → ( 𝐹 ( linC ‘ 𝑍 ) { 𝐴 } ) ≠ 𝐵 )