This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
Assertion mat1dimelbas ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
2 mat1dim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 mat1dim.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
4 snfi ⊢ { 𝐸 } ∈ Fin
5 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Ring )
6 1 2 matbas2 ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) = ( Base ‘ 𝐴 ) )
7 6 eqcomd ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝐴 ) = ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) )
8 7 eleq2d ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ 𝑀 ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) ) )
9 4 5 8 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ 𝑀 ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) ) )
10 2 fvexi ⊢ 𝐵 ∈ V
11 snex ⊢ { 𝐸 } ∈ V
12 11 11 pm3.2i ⊢ ( { 𝐸 } ∈ V ∧ { 𝐸 } ∈ V )
13 xpexg ⊢ ( ( { 𝐸 } ∈ V ∧ { 𝐸 } ∈ V ) → ( { 𝐸 } × { 𝐸 } ) ∈ V )
14 12 13 mp1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) ∈ V )
15 elmapg ⊢ ( ( 𝐵 ∈ V ∧ ( { 𝐸 } × { 𝐸 } ) ∈ V ) → ( 𝑀 ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) ↔ 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
16 10 14 15 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 ∈ ( 𝐵 ↑m ( { 𝐸 } × { 𝐸 } ) ) ↔ 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
17 9 16 bitrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
18 xpsng ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
19 18 anidms ⊢ ( 𝐸 ∈ 𝑉 → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
20 19 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
21 20 feq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ 𝑀 : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 ) )
22 opex ⊢ ⟨ 𝐸 , 𝐸 ⟩ ∈ V
23 22 fsn2 ⊢ ( 𝑀 : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 ↔ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) )
24 risset ⊢ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ↔ ∃ 𝑟 ∈ 𝐵 𝑟 = ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) )
25 eqcom ⊢ ( 𝑟 = ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
26 25 rexbii ⊢ ( ∃ 𝑟 ∈ 𝐵 𝑟 = ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
27 24 26 sylbb ⊢ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 → ∃ 𝑟 ∈ 𝐵 ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
28 27 ad2antrl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
29 eqeq1 ⊢ ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ) )
30 opex ⊢ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ ∈ V
31 sneqbg ⊢ ( ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ ∈ V → ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ ) )
32 30 31 ax-mp ⊢ ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ )
33 eqid ⊢ ⟨ 𝐸 , 𝐸 ⟩ = ⟨ 𝐸 , 𝐸 ⟩
34 vex ⊢ 𝑟 ∈ V
35 22 34 opth2 ⊢ ( ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ ↔ ( ⟨ 𝐸 , 𝐸 ⟩ = ⟨ 𝐸 , 𝐸 ⟩ ∧ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 ) )
36 33 35 mpbiran ⊢ ( ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
37 32 36 bitri ⊢ ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 )
38 29 37 bitrdi ⊢ ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 ) )
39 38 adantl ⊢ ( ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 ) )
40 39 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) ) → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 ) )
41 40 rexbidv ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) ) → ( ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ∃ 𝑟 ∈ 𝐵 ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) = 𝑟 ) )
42 28 41 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) ) → ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } )
43 42 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( ( ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ∈ 𝐵 ∧ 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , ( 𝑀 ‘ ⟨ 𝐸 , 𝐸 ⟩ ) ⟩ } ) → ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ) )
44 23 43 biimtrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 : { ⟨ 𝐸 , 𝐸 ⟩ } ⟶ 𝐵 → ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ) )
45 21 44 sylbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 → ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ) )
46 f1o2sn ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝑟 ∈ 𝐵 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) –1-1-onto→ { 𝑟 } )
47 f1of ⊢ ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) –1-1-onto→ { 𝑟 } → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ { 𝑟 } )
48 46 47 syl ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝑟 ∈ 𝐵 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ { 𝑟 } )
49 48 adantll ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝐵 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ { 𝑟 } )
50 snssi ⊢ ( 𝑟 ∈ 𝐵 → { 𝑟 } ⊆ 𝐵 )
51 50 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝐵 ) → { 𝑟 } ⊆ 𝐵 )
52 49 51 fssd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝐵 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 )
53 feq1 ⊢ ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } → ( 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
54 52 53 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ 𝑟 ∈ 𝐵 ) → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } → 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
55 54 rexlimdva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } → 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ) )
56 45 55 impbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ) )
57 3 eqcomi ⊢ ⟨ 𝐸 , 𝐸 ⟩ = 𝑂
58 57 opeq1i ⊢ ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ = ⟨ 𝑂 , 𝑟 ⟩
59 58 sneqi ⊢ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } = { ⟨ 𝑂 , 𝑟 ⟩ }
60 59 eqeq2i ⊢ ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } )
61 60 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } ) )
62 61 rexbidv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑟 ⟩ } ↔ ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } ) )
63 56 62 bitrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 : ( { 𝐸 } × { 𝐸 } ) ⟶ 𝐵 ↔ ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } ) )
64 17 63 bitrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ ∃ 𝑟 ∈ 𝐵 𝑀 = { ⟨ 𝑂 , 𝑟 ⟩ } ) )