Theorem mavmul0g

Description: The result of the 0-dimensional multiplication of a matrix with a vector is always the empty set. (Contributed by AV, 1-Mar-2019)

	Ref	Expression
Hypothesis	mavmul0.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
Assertion	mavmul0g	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑋 · 𝑌 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		mavmul0.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
2		oveq12	⊢ ( ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) → ( 𝑋 · 𝑌 ) = ( ∅ · ∅ ) )
3	1	mavmul0	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ∅ · ∅ ) = ∅ )
4	2 3	sylan9eq	⊢ ( ( ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ∧ ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) ) → ( 𝑋 · 𝑌 ) = ∅ )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7		simpr	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
8		0fin	⊢ ∅ ∈ Fin
9		eleq1	⊢ ( 𝑁 = ∅ → ( 𝑁 ∈ Fin ↔ ∅ ∈ Fin ) )
10	8 9	mpbiri	⊢ ( 𝑁 = ∅ → 𝑁 ∈ Fin )
11	10	adantr	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ Fin )
12	1 5 6 7 11 11	mvmulfval	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → · = ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ) )
13	12	dmeqd	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → dom · = dom ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ) )
14		0ex	⊢ ∅ ∈ V
15		eleq1	⊢ ( 𝑁 = ∅ → ( 𝑁 ∈ V ↔ ∅ ∈ V ) )
16	14 15	mpbiri	⊢ ( 𝑁 = ∅ → 𝑁 ∈ V )
17	16	mptexd	⊢ ( 𝑁 = ∅ → ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ∈ V )
18	17	adantr	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ∈ V )
19	18	adantr	⊢ ( ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) ) → ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ∈ V )
20	19	ralrimivva	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ∀ 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∀ 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ∈ V )
21		eqid	⊢ ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ) = ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) )
22	21	dmmpoga	⊢ ( ∀ 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∀ 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ∈ V → dom ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ) = ( ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) × ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) )
23	20 22	syl	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑖 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) , 𝑗 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ↦ ( 𝑘 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑙 ∈ 𝑁 ↦ ( ( 𝑘 𝑖 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑗 ‘ 𝑙 ) ) ) ) ) ) = ( ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) × ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) )
24		id	⊢ ( 𝑁 = ∅ → 𝑁 = ∅ )
25	24 24	xpeq12d	⊢ ( 𝑁 = ∅ → ( 𝑁 × 𝑁 ) = ( ∅ × ∅ ) )
26		0xp	⊢ ( ∅ × ∅ ) = ∅
27	25 26	eqtrdi	⊢ ( 𝑁 = ∅ → ( 𝑁 × 𝑁 ) = ∅ )
28	27	oveq2d	⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( ( Base ‘ 𝑅 ) ↑m ∅ ) )
29		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
30		map0e	⊢ ( ( Base ‘ 𝑅 ) ∈ V → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
31	29 30	mp1i	⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
32	28 31	eqtrd	⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 1o )
33	32	adantr	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 1o )
34		df1o2	⊢ 1o = { ∅ }
35	33 34	eqtrdi	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = { ∅ } )
36		oveq2	⊢ ( 𝑁 = ∅ → ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = ( ( Base ‘ 𝑅 ) ↑m ∅ ) )
37	29 30	mp1i	⊢ ( 𝑅 ∈ 𝑉 → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = 1o )
38	37 34	eqtrdi	⊢ ( 𝑅 ∈ 𝑉 → ( ( Base ‘ 𝑅 ) ↑m ∅ ) = { ∅ } )
39	36 38	sylan9eq	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) = { ∅ } )
40	35 39	xpeq12d	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) × ( ( Base ‘ 𝑅 ) ↑m 𝑁 ) ) = ( { ∅ } × { ∅ } ) )
41	13 23 40	3eqtrd	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → dom · = ( { ∅ } × { ∅ } ) )
42		elsni	⊢ ( 𝑋 ∈ { ∅ } → 𝑋 = ∅ )
43		elsni	⊢ ( 𝑌 ∈ { ∅ } → 𝑌 = ∅ )
44	42 43	anim12i	⊢ ( ( 𝑋 ∈ { ∅ } ∧ 𝑌 ∈ { ∅ } ) → ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) )
45	44	con3i	⊢ ( ¬ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) → ¬ ( 𝑋 ∈ { ∅ } ∧ 𝑌 ∈ { ∅ } ) )
46		ndmovg	⊢ ( ( dom · = ( { ∅ } × { ∅ } ) ∧ ¬ ( 𝑋 ∈ { ∅ } ∧ 𝑌 ∈ { ∅ } ) ) → ( 𝑋 · 𝑌 ) = ∅ )
47	41 45 46	syl2anr	⊢ ( ( ¬ ( 𝑋 = ∅ ∧ 𝑌 = ∅ ) ∧ ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) ) → ( 𝑋 · 𝑌 ) = ∅ )
48	4 47	pm2.61ian	⊢ ( ( 𝑁 = ∅ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑋 · 𝑌 ) = ∅ )