mat1dimscm

Description: The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019)

	Ref	Expression
Hypotheses	mat1dim.a	$⊢ A = \{E\} Mat R$
	mat1dim.b	$⊢ B = {Base}_{R}$
	mat1dim.o	$⊢ O = ⟨E, E⟩$
Assertion	mat1dimscm	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to X \cdot_{A} \{⟨O, Y⟩\} = \{⟨O, X \cdot_{R} Y⟩\}$

Proof

Step	Hyp	Ref	Expression
1		mat1dim.a	$⊢ A = \{E\} Mat R$
2		mat1dim.b	$⊢ B = {Base}_{R}$
3		mat1dim.o	$⊢ O = ⟨E, E⟩$
4		opex	$⊢ ⟨E, E⟩ \in V$
5	3 4	eqeltri	$⊢ O \in V$
6	5	a1i	$⊢ Y \in B \to O \in V$
7	6	anim2i	$⊢ (X \in B \land Y \in B) \to (X \in B \land O \in V)$
8	7	ancomd	$⊢ (X \in B \land Y \in B) \to (O \in V \land X \in B)$
9		fnsng	$⊢ (O \in V \land X \in B) \to \{⟨O, X⟩\} Fn \{O\}$
10	8 9	syl	$⊢ (X \in B \land Y \in B) \to \{⟨O, X⟩\} Fn \{O\}$
11	10	adantl	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{⟨O, X⟩\} Fn \{O\}$
12		xpsng	$⊢ (O \in V \land X \in B) \to \{O\} \times \{X\} = \{⟨O, X⟩\}$
13	8 12	syl	$⊢ (X \in B \land Y \in B) \to \{O\} \times \{X\} = \{⟨O, X⟩\}$
14	13	adantl	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{O\} \times \{X\} = \{⟨O, X⟩\}$
15	14	fneq1d	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to ((\{O\} \times \{X\}) Fn \{O\} \leftrightarrow \{⟨O, X⟩\} Fn \{O\})$
16	11 15	mpbird	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to (\{O\} \times \{X\}) Fn \{O\}$
17		xpsng	$⊢ (E \in V \land E \in V) \to \{E\} \times \{E\} = \{⟨E, E⟩\}$
18	3	sneqi	$⊢ \{O\} = \{⟨E, E⟩\}$
19	17 18	eqtr4di	$⊢ (E \in V \land E \in V) \to \{E\} \times \{E\} = \{O\}$
20	19	anidms	$⊢ E \in V \to \{E\} \times \{E\} = \{O\}$
21	20	ad2antlr	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{E\} \times \{E\} = \{O\}$
22	21	xpeq1d	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to (\{E\} \times \{E\}) \times \{X\} = \{O\} \times \{X\}$
23	22	fneq1d	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to (((\{E\} \times \{E\}) \times \{X\}) Fn \{O\} \leftrightarrow (\{O\} \times \{X\}) Fn \{O\})$
24	16 23	mpbird	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to ((\{E\} \times \{E\}) \times \{X\}) Fn \{O\}$
25	5	a1i	$⊢ X \in B \to O \in V$
26		fnsng	$⊢ (O \in V \land Y \in B) \to \{⟨O, Y⟩\} Fn \{O\}$
27	25 26	sylan	$⊢ (X \in B \land Y \in B) \to \{⟨O, Y⟩\} Fn \{O\}$
28	27	adantl	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{⟨O, Y⟩\} Fn \{O\}$
29		snex	$⊢ \{O\} \in V$
30	29	a1i	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{O\} \in V$
31		inidm	$⊢ \{O\} \cap \{O\} = \{O\}$
32		elsni	$⊢ x \in \{O\} \to x = O$
33		fveq2	$⊢ x = O \to ((\{E\} \times \{E\}) \times \{X\}) (x) = ((\{E\} \times \{E\}) \times \{X\}) (O)$
34	17	anidms	$⊢ E \in V \to \{E\} \times \{E\} = \{⟨E, E⟩\}$
35	34	ad2antlr	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{E\} \times \{E\} = \{⟨E, E⟩\}$
36	35	xpeq1d	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to (\{E\} \times \{E\}) \times \{X\} = \{⟨E, E⟩\} \times \{X\}$
37	4	a1i	$⊢ Y \in B \to ⟨E, E⟩ \in V$
38	37	anim2i	$⊢ (X \in B \land Y \in B) \to (X \in B \land ⟨E, E⟩ \in V)$
39	38	ancomd	$⊢ (X \in B \land Y \in B) \to (⟨E, E⟩ \in V \land X \in B)$
40		xpsng	$⊢ (⟨E, E⟩ \in V \land X \in B) \to \{⟨E, E⟩\} \times \{X\} = \{⟨⟨E, E⟩, X⟩\}$
41	3	eqcomi	$⊢ ⟨E, E⟩ = O$
42	41	opeq1i	$⊢ ⟨⟨E, E⟩, X⟩ = ⟨O, X⟩$
43	42	sneqi	$⊢ \{⟨⟨E, E⟩, X⟩\} = \{⟨O, X⟩\}$
44	40 43	eqtrdi	$⊢ (⟨E, E⟩ \in V \land X \in B) \to \{⟨E, E⟩\} \times \{X\} = \{⟨O, X⟩\}$
45	39 44	syl	$⊢ (X \in B \land Y \in B) \to \{⟨E, E⟩\} \times \{X\} = \{⟨O, X⟩\}$
46	45	adantl	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{⟨E, E⟩\} \times \{X\} = \{⟨O, X⟩\}$
47	36 46	eqtrd	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to (\{E\} \times \{E\}) \times \{X\} = \{⟨O, X⟩\}$
48	47	fveq1d	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to ((\{E\} \times \{E\}) \times \{X\}) (O) = \{⟨O, X⟩\} (O)$
49		fvsng	$⊢ (O \in V \land X \in B) \to \{⟨O, X⟩\} (O) = X$
50	8 49	syl	$⊢ (X \in B \land Y \in B) \to \{⟨O, X⟩\} (O) = X$
51	50	adantl	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{⟨O, X⟩\} (O) = X$
52	48 51	eqtrd	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to ((\{E\} \times \{E\}) \times \{X\}) (O) = X$
53	33 52	sylan9eq	$⊢ (x = O \land ((R \in Ring \land E \in V) \land (X \in B \land Y \in B))) \to ((\{E\} \times \{E\}) \times \{X\}) (x) = X$
54	53	ex	$⊢ x = O \to (((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to ((\{E\} \times \{E\}) \times \{X\}) (x) = X)$
55	32 54	syl	$⊢ x \in \{O\} \to (((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to ((\{E\} \times \{E\}) \times \{X\}) (x) = X)$
56	55	impcom	$⊢ (((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \land x \in \{O\}) \to ((\{E\} \times \{E\}) \times \{X\}) (x) = X$
57		fveq2	$⊢ x = O \to \{⟨O, Y⟩\} (x) = \{⟨O, Y⟩\} (O)$
58		fvsng	$⊢ (O \in V \land Y \in B) \to \{⟨O, Y⟩\} (O) = Y$
59	25 58	sylan	$⊢ (X \in B \land Y \in B) \to \{⟨O, Y⟩\} (O) = Y$
60	59	adantl	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{⟨O, Y⟩\} (O) = Y$
61	57 60	sylan9eq	$⊢ (x = O \land ((R \in Ring \land E \in V) \land (X \in B \land Y \in B))) \to \{⟨O, Y⟩\} (x) = Y$
62	61	ex	$⊢ x = O \to (((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{⟨O, Y⟩\} (x) = Y)$
63	32 62	syl	$⊢ x \in \{O\} \to (((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{⟨O, Y⟩\} (x) = Y)$
64	63	impcom	$⊢ (((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \land x \in \{O\}) \to \{⟨O, Y⟩\} (x) = Y$
65	24 28 30 30 31 56 64	offval	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to ((\{E\} \times \{E\}) \times \{X\}) {\cdot_{R}}_{f} \{⟨O, Y⟩\} = (x \in \{O\} ⟼ X \cdot_{R} Y)$
66		simprl	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to X \in B$
67		simpr	$⊢ (X \in B \land Y \in B) \to Y \in B$
68	67	anim2i	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to ((R \in Ring \land E \in V) \land Y \in B)$
69		df-3an	$⊢ (R \in Ring \land E \in V \land Y \in B) \leftrightarrow ((R \in Ring \land E \in V) \land Y \in B)$
70	68 69	sylibr	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to (R \in Ring \land E \in V \land Y \in B)$
71	1 2 3	mat1dimbas	$⊢ (R \in Ring \land E \in V \land Y \in B) \to \{⟨O, Y⟩\} \in {Base}_{A}$
72	70 71	syl	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{⟨O, Y⟩\} \in {Base}_{A}$
73		eqid	$⊢ {Base}_{A} = {Base}_{A}$
74		eqid	$⊢ \cdot_{A} = \cdot_{A}$
75		eqid	$⊢ \cdot_{R} = \cdot_{R}$
76		eqid	$⊢ \{E\} \times \{E\} = \{E\} \times \{E\}$
77	1 73 2 74 75 76	matvsca2	$⊢ (X \in B \land \{⟨O, Y⟩\} \in {Base}_{A}) \to X \cdot_{A} \{⟨O, Y⟩\} = ((\{E\} \times \{E\}) \times \{X\}) {\cdot_{R}}_{f} \{⟨O, Y⟩\}$
78	66 72 77	syl2anc	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to X \cdot_{A} \{⟨O, Y⟩\} = ((\{E\} \times \{E\}) \times \{X\}) {\cdot_{R}}_{f} \{⟨O, Y⟩\}$
79		3anass	$⊢ (R \in Ring \land X \in B \land Y \in B) \leftrightarrow (R \in Ring \land (X \in B \land Y \in B))$
80	79	biimpri	$⊢ (R \in Ring \land (X \in B \land Y \in B)) \to (R \in Ring \land X \in B \land Y \in B)$
81	80	adantlr	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to (R \in Ring \land X \in B \land Y \in B)$
82	2 75	ringcl	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \cdot_{R} Y \in B$
83	81 82	syl	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to X \cdot_{R} Y \in B$
84		fmptsn	$⊢ (O \in V \land X \cdot_{R} Y \in B) \to \{⟨O, X \cdot_{R} Y⟩\} = (x \in \{O\} ⟼ X \cdot_{R} Y)$
85	5 83 84	sylancr	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to \{⟨O, X \cdot_{R} Y⟩\} = (x \in \{O\} ⟼ X \cdot_{R} Y)$
86	65 78 85	3eqtr4d	$⊢ ((R \in Ring \land E \in V) \land (X \in B \land Y \in B)) \to X \cdot_{A} \{⟨O, Y⟩\} = \{⟨O, X \cdot_{R} Y⟩\}$

Metamath Proof Explorer

Theorem mat1dimscm

Proof