mamufacex

Description: Every solution of the equation A * X = B for matrices A and B is a matrix. (Contributed by AV, 10-Feb-2019)

	Ref	Expression
Hypotheses	mamudm.e	⊢ 𝐸 = ( 𝑅 freeLMod ( 𝑀 × 𝑁 ) )
	mamudm.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	mamudm.f	⊢ 𝐹 = ( 𝑅 freeLMod ( 𝑁 × 𝑃 ) )
	mamudm.c	⊢ 𝐶 = ( Base ‘ 𝐹 )
	mamudm.m	⊢ × = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
	mamufacex.g	⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑀 × 𝑃 ) )
	mamufacex.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
Assertion	mamufacex	⊢ ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		mamudm.e	⊢ 𝐸 = ( 𝑅 freeLMod ( 𝑀 × 𝑁 ) )
2		mamudm.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
3		mamudm.f	⊢ 𝐹 = ( 𝑅 freeLMod ( 𝑁 × 𝑃 ) )
4		mamudm.c	⊢ 𝐶 = ( Base ‘ 𝐹 )
5		mamudm.m	⊢ × = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
6		mamufacex.g	⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑀 × 𝑃 ) )
7		mamufacex.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
8		2a1	⊢ ( 𝑍 ∈ 𝐶 → ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) ) )
9	1 2 3 4 5	mamudm	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → dom × = ( 𝐵 × 𝐶 ) )
10	9	adantlr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → dom × = ( 𝐵 × 𝐶 ) )
11	10	3adant1	⊢ ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → dom × = ( 𝐵 × 𝐶 ) )
12		simpl	⊢ ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ¬ 𝑍 ∈ 𝐶 )
13	12	intnand	⊢ ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ¬ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) )
14		ndmovg	⊢ ( ( dom × = ( 𝐵 × 𝐶 ) ∧ ¬ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝑋 × 𝑍 ) = ∅ )
15	11 13 14	syl2an2	⊢ ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ( 𝑋 × 𝑍 ) = ∅ )
16		eqeq1	⊢ ( ( 𝑋 × 𝑍 ) = ∅ → ( ( 𝑋 × 𝑍 ) = 𝑌 ↔ ∅ = 𝑌 ) )
17		xpfi	⊢ ( ( 𝑀 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑀 × 𝑃 ) ∈ Fin )
18	17	3adant2	⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑀 × 𝑃 ) ∈ Fin )
19		xpnz	⊢ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ↔ ( 𝑀 × 𝑃 ) ≠ ∅ )
20	19	biimpi	⊢ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) → ( 𝑀 × 𝑃 ) ≠ ∅ )
21		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
22	6 21 7	elfrlmbasn0	⊢ ( ( ( 𝑀 × 𝑃 ) ∈ Fin ∧ ( 𝑀 × 𝑃 ) ≠ ∅ ) → ( 𝑌 ∈ 𝐷 → 𝑌 ≠ ∅ ) )
23	18 20 22	syl2an	⊢ ( ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ∧ ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ) → ( 𝑌 ∈ 𝐷 → 𝑌 ≠ ∅ ) )
24	23	ex	⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) → ( 𝑌 ∈ 𝐷 → 𝑌 ≠ ∅ ) ) )
25	24	com13	⊢ ( 𝑌 ∈ 𝐷 → ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → 𝑌 ≠ ∅ ) ) )
26	25	adantl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) → ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) → ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → 𝑌 ≠ ∅ ) ) )
27	26	3imp21	⊢ ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → 𝑌 ≠ ∅ )
28		eqneqall	⊢ ( 𝑌 = ∅ → ( 𝑌 ≠ ∅ → 𝑍 ∈ 𝐶 ) )
29	27 28	syl5com	⊢ ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( 𝑌 = ∅ → 𝑍 ∈ 𝐶 ) )
30	29	adantl	⊢ ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ( 𝑌 = ∅ → 𝑍 ∈ 𝐶 ) )
31	30	com12	⊢ ( 𝑌 = ∅ → ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → 𝑍 ∈ 𝐶 ) )
32	31	eqcoms	⊢ ( ∅ = 𝑌 → ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → 𝑍 ∈ 𝐶 ) )
33	16 32	biimtrdi	⊢ ( ( 𝑋 × 𝑍 ) = ∅ → ( ( 𝑋 × 𝑍 ) = 𝑌 → ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → 𝑍 ∈ 𝐶 ) ) )
34	33	com23	⊢ ( ( 𝑋 × 𝑍 ) = ∅ → ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) ) )
35	15 34	mpcom	⊢ ( ( ¬ 𝑍 ∈ 𝐶 ∧ ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) )
36	35	ex	⊢ ( ¬ 𝑍 ∈ 𝐶 → ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) ) )
37	8 36	pm2.61i	⊢ ( ( ( 𝑀 ≠ ∅ ∧ 𝑃 ≠ ∅ ) ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( 𝑋 × 𝑍 ) = 𝑌 → 𝑍 ∈ 𝐶 ) )

Metamath Proof Explorer

Theorem mamufacex

Proof