mat1dimelbas

Description: A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019)

	Ref	Expression
Hypotheses	mat1dim.a	$⊢ A = \{E\} Mat R$
	mat1dim.b	$⊢ B = {Base}_{R}$
	mat1dim.o	$⊢ O = ⟨E, E⟩$
Assertion	mat1dimelbas	$⊢ (R \in Ring \land E \in V) \to (M \in {Base}_{A} \leftrightarrow \exists r \in B M = \{⟨O, r⟩\})$

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		snfi	$⊢ \{E\} \in Fin$
5		simpl	$⊢ (R \in Ring \land E \in V) \to R \in Ring$
6	1 2	matbas2	$⊢ (\{E\} \in Fin \land R \in Ring) \to B^{(\{E\} \times \{E\})} = {Base}_{A}$
7	6	eqcomd	$⊢ (\{E\} \in Fin \land R \in Ring) \to {Base}_{A} = B^{(\{E\} \times \{E\})}$
8	7	eleq2d	$⊢ (\{E\} \in Fin \land R \in Ring) \to (M \in {Base}_{A} \leftrightarrow M \in (B^{(\{E\} \times \{E\})}))$
9	4 5 8	sylancr	$⊢ (R \in Ring \land E \in V) \to (M \in {Base}_{A} \leftrightarrow M \in (B^{(\{E\} \times \{E\})}))$
10	2	fvexi	$⊢ B \in V$
11		snex	$⊢ \{E\} \in V$
12	11 11	pm3.2i	$⊢ (\{E\} \in V \land \{E\} \in V)$
13		xpexg	$⊢ (\{E\} \in V \land \{E\} \in V) \to \{E\} \times \{E\} \in V$
14	12 13	mp1i	$⊢ (R \in Ring \land E \in V) \to \{E\} \times \{E\} \in V$
15		elmapg	$⊢ (B \in V \land \{E\} \times \{E\} \in V) \to (M \in (B^{(\{E\} \times \{E\})}) \leftrightarrow M : \{E\} \times \{E\} ⟶ B)$
16	10 14 15	sylancr	$⊢ (R \in Ring \land E \in V) \to (M \in (B^{(\{E\} \times \{E\})}) \leftrightarrow M : \{E\} \times \{E\} ⟶ B)$
17	9 16	bitrd	$⊢ (R \in Ring \land E \in V) \to (M \in {Base}_{A} \leftrightarrow M : \{E\} \times \{E\} ⟶ B)$
18		xpsng	$⊢ (E \in V \land E \in V) \to \{E\} \times \{E\} = \{⟨E, E⟩\}$
19	18	anidms	$⊢ E \in V \to \{E\} \times \{E\} = \{⟨E, E⟩\}$
20	19	adantl	$⊢ (R \in Ring \land E \in V) \to \{E\} \times \{E\} = \{⟨E, E⟩\}$
21	20	feq2d	$⊢ (R \in Ring \land E \in V) \to (M : \{E\} \times \{E\} ⟶ B \leftrightarrow M : \{⟨E, E⟩\} ⟶ B)$
22		opex	$⊢ ⟨E, E⟩ \in V$
23	22	fsn2	$⊢ M : \{⟨E, E⟩\} ⟶ B \leftrightarrow (M (⟨E, E⟩) \in B \land M = \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\})$
24		risset	$⊢ M (⟨E, E⟩) \in B \leftrightarrow \exists r \in B r = M (⟨E, E⟩)$
25		eqcom	$⊢ r = M (⟨E, E⟩) \leftrightarrow M (⟨E, E⟩) = r$
26	25	rexbii	$⊢ \exists r \in B r = M (⟨E, E⟩) \leftrightarrow \exists r \in B M (⟨E, E⟩) = r$
27	24 26	sylbb	$⊢ M (⟨E, E⟩) \in B \to \exists r \in B M (⟨E, E⟩) = r$
28	27	ad2antrl	$⊢ ((R \in Ring \land E \in V) \land (M (⟨E, E⟩) \in B \land M = \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\})) \to \exists r \in B M (⟨E, E⟩) = r$
29		eqeq1	$⊢ M = \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\} \to (M = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\} = \{⟨⟨E, E⟩, r⟩\})$
30		opex	$⊢ ⟨⟨E, E⟩, M (⟨E, E⟩)⟩ \in V$
31		sneqbg	$⊢ ⟨⟨E, E⟩, M (⟨E, E⟩)⟩ \in V \to (\{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\} = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow ⟨⟨E, E⟩, M (⟨E, E⟩)⟩ = ⟨⟨E, E⟩, r⟩)$
32	30 31	ax-mp	$⊢ \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\} = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow ⟨⟨E, E⟩, M (⟨E, E⟩)⟩ = ⟨⟨E, E⟩, r⟩$
33		eqid	$⊢ ⟨E, E⟩ = ⟨E, E⟩$
34		vex	$⊢ r \in V$
35	22 34	opth2	$⊢ ⟨⟨E, E⟩, M (⟨E, E⟩)⟩ = ⟨⟨E, E⟩, r⟩ \leftrightarrow (⟨E, E⟩ = ⟨E, E⟩ \land M (⟨E, E⟩) = r)$
36	33 35	mpbiran	$⊢ ⟨⟨E, E⟩, M (⟨E, E⟩)⟩ = ⟨⟨E, E⟩, r⟩ \leftrightarrow M (⟨E, E⟩) = r$
37	32 36	bitri	$⊢ \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\} = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow M (⟨E, E⟩) = r$
38	29 37	bitrdi	$⊢ M = \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\} \to (M = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow M (⟨E, E⟩) = r)$
39	38	adantl	$⊢ (M (⟨E, E⟩) \in B \land M = \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\}) \to (M = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow M (⟨E, E⟩) = r)$
40	39	adantl	$⊢ ((R \in Ring \land E \in V) \land (M (⟨E, E⟩) \in B \land M = \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\})) \to (M = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow M (⟨E, E⟩) = r)$
41	40	rexbidv	$⊢ ((R \in Ring \land E \in V) \land (M (⟨E, E⟩) \in B \land M = \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\})) \to (\exists r \in B M = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow \exists r \in B M (⟨E, E⟩) = r)$
42	28 41	mpbird	$⊢ ((R \in Ring \land E \in V) \land (M (⟨E, E⟩) \in B \land M = \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\})) \to \exists r \in B M = \{⟨⟨E, E⟩, r⟩\}$
43	42	ex	$⊢ (R \in Ring \land E \in V) \to ((M (⟨E, E⟩) \in B \land M = \{⟨⟨E, E⟩, M (⟨E, E⟩)⟩\}) \to \exists r \in B M = \{⟨⟨E, E⟩, r⟩\})$
44	23 43	biimtrid	$⊢ (R \in Ring \land E \in V) \to (M : \{⟨E, E⟩\} ⟶ B \to \exists r \in B M = \{⟨⟨E, E⟩, r⟩\})$
45	21 44	sylbid	$⊢ (R \in Ring \land E \in V) \to (M : \{E\} \times \{E\} ⟶ B \to \exists r \in B M = \{⟨⟨E, E⟩, r⟩\})$
46		f1o2sn	$⊢ (E \in V \land r \in B) \to \{⟨⟨E, E⟩, r⟩\} : \{E\} \times \{E\} \underset{1-1 onto}{⟶} \{r\}$
47		f1of	$⊢ \{⟨⟨E, E⟩, r⟩\} : \{E\} \times \{E\} \underset{1-1 onto}{⟶} \{r\} \to \{⟨⟨E, E⟩, r⟩\} : \{E\} \times \{E\} ⟶ \{r\}$
48	46 47	syl	$⊢ (E \in V \land r \in B) \to \{⟨⟨E, E⟩, r⟩\} : \{E\} \times \{E\} ⟶ \{r\}$
49	48	adantll	$⊢ ((R \in Ring \land E \in V) \land r \in B) \to \{⟨⟨E, E⟩, r⟩\} : \{E\} \times \{E\} ⟶ \{r\}$
50		snssi	$⊢ r \in B \to \{r\} \subseteq B$
51	50	adantl	$⊢ ((R \in Ring \land E \in V) \land r \in B) \to \{r\} \subseteq B$
52	49 51	fssd	$⊢ ((R \in Ring \land E \in V) \land r \in B) \to \{⟨⟨E, E⟩, r⟩\} : \{E\} \times \{E\} ⟶ B$
53		feq1	$⊢ M = \{⟨⟨E, E⟩, r⟩\} \to (M : \{E\} \times \{E\} ⟶ B \leftrightarrow \{⟨⟨E, E⟩, r⟩\} : \{E\} \times \{E\} ⟶ B)$
54	52 53	syl5ibrcom	$⊢ ((R \in Ring \land E \in V) \land r \in B) \to (M = \{⟨⟨E, E⟩, r⟩\} \to M : \{E\} \times \{E\} ⟶ B)$
55	54	rexlimdva	$⊢ (R \in Ring \land E \in V) \to (\exists r \in B M = \{⟨⟨E, E⟩, r⟩\} \to M : \{E\} \times \{E\} ⟶ B)$
56	45 55	impbid	$⊢ (R \in Ring \land E \in V) \to (M : \{E\} \times \{E\} ⟶ B \leftrightarrow \exists r \in B M = \{⟨⟨E, E⟩, r⟩\})$
57	3	eqcomi	$⊢ ⟨E, E⟩ = O$
58	57	opeq1i	$⊢ ⟨⟨E, E⟩, r⟩ = ⟨O, r⟩$
59	58	sneqi	$⊢ \{⟨⟨E, E⟩, r⟩\} = \{⟨O, r⟩\}$
60	59	eqeq2i	$⊢ M = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow M = \{⟨O, r⟩\}$
61	60	a1i	$⊢ (R \in Ring \land E \in V) \to (M = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow M = \{⟨O, r⟩\})$
62	61	rexbidv	$⊢ (R \in Ring \land E \in V) \to (\exists r \in B M = \{⟨⟨E, E⟩, r⟩\} \leftrightarrow \exists r \in B M = \{⟨O, r⟩\})$
63	56 62	bitrd	$⊢ (R \in Ring \land E \in V) \to (M : \{E\} \times \{E\} ⟶ B \leftrightarrow \exists r \in B M = \{⟨O, r⟩\})$
64	17 63	bitrd	$⊢ (R \in Ring \land E \in V) \to (M \in {Base}_{A} \leftrightarrow \exists r \in B M = \{⟨O, r⟩\})$

Metamath Proof Explorer

Theorem mat1dimelbas

Proof